summaryrefslogtreecommitdiff
path: root/tools/verification
AgeCommit message (Collapse)Author
2026-04-01rv/rvgen: fix typos in automata and generator docstring and commentsWander Lairson Costa
Fix two typos in the Automata class documentation that have been present since the initial implementation. Fix the class docstring: "part it" instead of "parses it". Additionally, a comment describing transition labels contained the misspelling "lables" instead of "labels". Fix a typo in the comment describing the insertion of the initial state into the states list: "bein og" should be "beginning of". Fix typo in the module docstring: "Abtract" should be "Abstract". Fix several occurrences of "automata" where it should be the singular form "automaton". Signed-off-by: Wander Lairson Costa <wander@redhat.com> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Link: https://lore.kernel.org/r/20260223162407.147003-8-wander@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31rv/rvgen: use context managers for file operationsWander Lairson Costa
Replace manual file open and close operations with context managers throughout the rvgen codebase. The previous implementation used explicit open() and close() calls, which could lead to resource leaks if exceptions occurred between opening and closing the file handles. This change affects three file operations: reading DOT specification files in the automata parser, reading template files in the generator base class, and writing generated monitor files. All now use the with statement to ensure proper resource cleanup even in error conditions. Context managers provide automatic cleanup through the with statement, which guarantees that file handles are closed when the with block exits regardless of whether an exception occurred. This follows PEP 343 recommendations and is the standard Python idiom for resource management. The change also reduces code verbosity while improving safety and maintainability. Signed-off-by: Wander Lairson Costa <wander@redhat.com> Reviewed-by: Nam Cao <namcao@linutronix.de> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Link: https://lore.kernel.org/r/20260223162407.147003-7-wander@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31rv/rvgen: remove unnecessary semicolonsWander Lairson Costa
Remove unnecessary semicolons from Python code in the rvgen tool. Python does not require semicolons to terminate statements, and their presence goes against PEP 8 style guidelines. These semicolons were likely added out of habit from C-style languages. This cleanup improves consistency with Python coding standards and aligns with the recent improvements to remove other Python anti-patterns from the codebase. Signed-off-by: Wander Lairson Costa <wander@redhat.com> Reviewed-by: Nam Cao <namcao@linutronix.de> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Link: https://lore.kernel.org/r/20260223162407.147003-6-wander@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31rv/rvgen: replace __len__() calls with len()Wander Lairson Costa
Replace all direct calls to the __len__() dunder method with the idiomatic len() built-in function across the rvgen codebase. This change eliminates a Python anti-pattern where dunder methods are called directly instead of using their corresponding built-in functions. The changes affect nine instances across two files. In automata.py, the empty string check is further improved by using truthiness testing instead of explicit length comparison. In dot2c.py, all length checks in the get_minimun_type, __get_max_strlen_of_states, and get_aut_init_function methods now use the standard len() function. Additionally, spacing around keyword arguments has been corrected to follow PEP 8 guidelines. Direct calls to dunder methods like __len__() are discouraged in Python because they bypass the language's abstraction layer and reduce code readability. Using len() provides the same functionality while adhering to Python community standards and making the code more familiar to Python developers. Signed-off-by: Wander Lairson Costa <wander@redhat.com> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20260223162407.147003-5-wander@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31rv/rvgen: replace % string formatting with f-stringsWander Lairson Costa
Replace all instances of percent-style string formatting with f-strings across the rvgen codebase. This modernizes the string formatting to use Python 3.6+ features, providing clearer and more maintainable code while improving runtime performance. The conversion handles all formatting cases including simple variable substitution, multi-variable formatting, and complex format specifiers. Dynamic width formatting is converted from "%*s" to "{var:>{width}}" using proper alignment syntax. Template strings for generated C code properly escape braces using double-brace syntax to produce literal braces in the output. F-strings provide approximately 2x performance improvement over percent formatting and are the recommended approach in modern Python. Signed-off-by: Wander Lairson Costa <wander@redhat.com> Reviewed-by: Nam Cao <namcao@linutronix.de> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Link: https://lore.kernel.org/r/20260223162407.147003-4-wander@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31rv/rvgen: remove bare except clauses in generatorWander Lairson Costa
Remove bare except clauses from the generator module that were catching all exceptions including KeyboardInterrupt and SystemExit. This follows the same exception handling improvements made in the previous AutomataError commit and addresses PEP 8 violations. The bare except clause in __create_directory was silently catching and ignoring all errors after printing a message, which could mask serious issues. For __write_file, the bare except created a critical bug where the file variable could remain undefined if open() failed, causing a NameError when attempting to write to or close the file. These methods now let OSError propagate naturally, allowing callers to handle file system errors appropriately. This provides clearer error reporting and allows Python's exception handling to show complete stack traces with proper error types and locations. Signed-off-by: Wander Lairson Costa <wander@redhat.com> Reviewed-by: Nam Cao <namcao@linutronix.de> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Link: https://lore.kernel.org/r/20260223162407.147003-3-wander@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31rv/rvgen: introduce AutomataError exception classWander Lairson Costa
Replace the generic except Exception block with a custom AutomataError class that inherits from Exception. This provides more precise exception handling for automata parsing and validation errors while avoiding overly broad exception catches that could mask programming errors like SyntaxError or TypeError. The AutomataError class is raised when DOT file processing fails due to invalid format, I/O errors, or malformed automaton definitions. The main entry point catches this specific exception and provides a user-friendly error message to stderr before exiting. Also, replace generic exceptions raising in HA and LTL with AutomataError. Co-authored-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Wander Lairson Costa <wander@redhat.com> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Link: https://lore.kernel.org/r/20260223162407.147003-2-wander@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31rv: Add nomiss deadline monitorGabriele Monaco
Add the deadline monitors collection to validate the deadline scheduler, both for deadline tasks and servers. The currently implemented monitors are: * nomiss: validate dl entities run to completion before their deadiline Reviewed-by: Nam Cao <namcao@linutronix.de> Reviewed-by: Juri Lelli <juri.lelli@redhat.com> Link: https://lore.kernel.org/r/20260330111010.153663-13-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31verification/rvgen: Add support for per-obj monitorsGabriele Monaco
The special per-object monitor type was just introduced in RV, this requires the user to define some functions and type specific to the object. Adapt rvgen to add stub definitions for the monitor_target type and other modifications required to create per-object monitors. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20260330111010.153663-10-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31rv: Convert the opid monitor to a hybrid automatonGabriele Monaco
The opid monitor validates that wakeup and need_resched events only occur with interrupts and preemption disabled by following the preemptirq tracepoints. As reported in [1], those tracepoints might be inaccurate in some situations (e.g. NMIs). Since the monitor doesn't validate other ordering properties, remove the dependency on preemptirq tracepoints and convert the monitor to a hybrid automaton to validate the constraint during event handling. This makes the monitor more robust by also removing the workaround for interrupts missing the preemption tracepoints, which was working on PREEMPT_RT only and allows the monitor to be built on kernels without the preemptirqs tracepoints. [1] - https://lore.kernel.org/lkml/20250625120823.60600-1-gmonaco@redhat.com Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20260330111010.153663-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31rv: Add sample hybrid monitor stallGabriele Monaco
Add a sample monitor to showcase hybrid/timed automata. The stall monitor identifies tasks stalled for longer than a threshold and reacts when that happens. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20260330111010.153663-7-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31verification/rvgen: Add support for Hybrid AutomataGabriele Monaco
Add the possibility to parse dot files as hybrid automata and generate the necessary code from rvgen. Hybrid automata are very similar to deterministic ones and most functionality is shared, the dot files include also constraints together with event names (separated by ;) and state names (separated by \n). The tool can now generate the appropriate code to validate constraints at runtime according to the dot specification. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20260330111010.153663-5-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-03-31verification/rvgen: Allow spaces in and events stringsGabriele Monaco
Currently the automata parser assumes event strings don't have any space, this stands true for event names, but can be a wrong assumption if we want to store other information in the event strings (e.g. constraints for hybrid automata). Adapt the parser logic to allow spaces in the event strings. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20260330111010.153663-4-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-01-12verification/rvgen: Remove unused variable declaration from containersGabriele Monaco
The monitor container source files contained a declaration and a definition for the rv_monitor variable. The former is superfluous and can be removed. Remove the variable declaration from the template as well as the existing monitor containers. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20251126104241.291258-9-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-01-12verification/dot2c: Remove superfluous enum assignment and add last commaGabriele Monaco
The header files generated by dot2c currently create enums for states and events assigning the first element to 0. This is superfluous as it happens automatically if no value is specified. Also it doesn't add a comma to the last enum elements, which slightly complicates the diff if states or events are added. Remove the assignment to 0 and add a comma to last elements, this simplifies the logic for the code generator. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20251126104241.291258-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-01-12verification/dot2c: Remove __buff_to_string() and cleanupGabriele Monaco
str.join() can do what __buff_to_string() does. Therefore replace __buff_to_string() to make the scripts more pythonic. Also clean and remove some intermediate functions. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20251126104241.291258-7-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-01-12verification/rvgen: Annotate DA functions with typesGabriele Monaco
Functions in automata.py, dot2c.py and dot2k.py don't have type annotations and it can get complicated to remember how to use them. Add minimal type annotations. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20251126104241.291258-6-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2026-01-12verification/rvgen: Adapt dot2k and templates after refactoring da_monitor.hGabriele Monaco
Previous changes refactored the da_monitor header file to avoid using macros. This implies a few changes in how to import and use da_monitor helpers: DECLARE_DA_MON_<TYPE>(name, type) is substituted by #define RV_MON_TYPE RV_MON_<TYPE> Update the rvgen templates to reflect the changes. Reviewed-by: Nam Cao <namcao@linutronix.de> Link: https://lore.kernel.org/r/20251126104241.291258-5-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
2025-07-28rv: Add opid per-cpu monitorGabriele Monaco
Add a per-cpu monitor as part of the sched model: * opid: operations with preemption and irq disabled Monitor to ensure wakeup and need_resched occur with irq and preemption disabled or in irq handlers. Cc: Jonathan Corbet <corbet@lwn.net> Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Ingo Molnar <mingo@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Tomas Glozar <tglozar@redhat.com> Cc: Juri Lelli <jlelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: John Kacur <jkacur@redhat.com> Link: https://lore.kernel.org/20250728135022.255578-10-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Acked-by: Nam Cao <namcao@linutronix.de> Tested-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-28rv: Add nrp and sssw per-task monitorsGabriele Monaco
Add 2 per-task monitors as part of the sched model: * nrp: need-resched preempts Monitor to ensure preemption requires need resched. * sssw: set state sleep and wakeup Monitor to ensure sched_set_state to sleepable leads to sleeping and sleeping tasks require wakeup. Cc: Ingo Molnar <mingo@redhat.com> Cc: Jonathan Corbet <corbet@lwn.net> Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Tomas Glozar <tglozar@redhat.com> Cc: Juri Lelli <jlelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: John Kacur <jkacur@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Link: https://lore.kernel.org/20250728135022.255578-9-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Acked-by: Nam Cao <namcao@linutronix.de> Tested-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-28rv: Replace tss and sncid monitors with more complete stsGabriele Monaco
The tss monitor currently guarantees task switches can happen only while scheduling, whereas the sncid monitor enforces scheduling occurs with interrupt disabled. Replace the monitors with a more comprehensive specification which implies both but also ensures that: * each scheduler call disable interrupts to switch * each task switch happens with interrupts disabled Cc: Ingo Molnar <mingo@redhat.com> Cc: Jonathan Corbet <corbet@lwn.net> Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Nam Cao <namcao@linutronix.de> Cc: Tomas Glozar <tglozar@redhat.com> Cc: Juri Lelli <jlelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: John Kacur <jkacur@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Link: https://lore.kernel.org/20250728135022.255578-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24rv: Return init error when registering monitorsGabriele Monaco
Monitors generated with dot2k have their registration function (the one called during monitor initialisation) return always 0, even if the registration failed on RV side. This can hide potential errors. Return the value returned by the RV register function. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Tomas Glozar <tglozar@redhat.com> Cc: Juri Lelli <jlelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: John Kacur <jkacur@redhat.com> Link: https://lore.kernel.org/20250723161240.194860-6-gmonaco@redhat.com Reviewed-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/rvgen: Organise Kconfig entries for nested monitorsGabriele Monaco
The current behaviour of rvgen when running with the -a option is to append the necessary lines at the end of the configuration for Kconfig, Makefile and tracepoints. This is not always the desired behaviour in case of nested monitors: while tracepoints are not affected by nesting and the Makefile's only requirement is that the parent monitor is built before its children, in the Kconfig it is better to have children defined right after their parent, otherwise the result has wrong indentation: [*] foo_parent monitor [*] foo_child1 monitor [*] foo_child2 monitor [*] bar_parent monitor [*] bar_child1 monitor [*] bar_child2 monitor [*] foo_child3 monitor [*] foo_child4 monitor Adapt rvgen to look for a different marker for nested monitors in the Kconfig file and append the line right after the last sibling, instead of the last monitor. Also add the marker when creating a new parent monitor. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Tomas Glozar <tglozar@redhat.com> Cc: Juri Lelli <jlelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: John Kacur <jkacur@redhat.com> Link: https://lore.kernel.org/20250723161240.194860-5-gmonaco@redhat.com Reviewed-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24tools/dot2c: Fix generated files going over 100 column limitGabriele Monaco
The dot2c.py script generates all states in a single line. This breaks the 100 column limit when the state machines are non-trivial. Change dot2c.py to generate the states in separate lines in case the generated line is going to be too long. Also adapt existing monitors with line length over the limit. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Tomas Glozar <tglozar@redhat.com> Cc: Juri Lelli <jlelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: John Kacur <jkacur@redhat.com> Link: https://lore.kernel.org/20250723161240.194860-4-gmonaco@redhat.com Suggested-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24tools/rv: Stop gracefully also on SIGTERMGabriele Monaco
Currently the userspace RV tool starts a monitor and waits for the user to press Ctrl-C (SIGINT) to terminate and stop the monitor. This doesn't account for a scenario where a user starts RV in background and simply kills it (SIGTERM unless the user specifies differently). E.g.: # rv mon wip & # kill % Would terminate RV without stopping the monitor and next RV executions won't start correctly. Register the signal handler used for SIGINT also to SIGTERM. Cc: Nam Cao <namcao@linutronix.de> Cc: Tomas Glozar <tglozar@redhat.com> Cc: Juri Lelli <jlelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: John Kacur <jkacur@redhat.com> Link: https://lore.kernel.org/20250723161240.194860-3-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24tools/rv: Do not skip idle in traceGabriele Monaco
Currently, the userspace RV tool skips trace events triggered by the RV tool itself, this can be changed by passing the parameter -s, which sets the variable config_my_pid to 0 (instead of the tool's PID). This has the side effect of skipping events generated by idle (PID 0). Set config_my_pid to -1 (an invalid pid) to avoid skipping idle. Cc: Nam Cao <namcao@linutronix.de> Cc: Tomas Glozar <tglozar@redhat.com> Cc: Juri Lelli <jlelli@redhat.com> Cc: Clark Williams <williams@redhat.com> Cc: John Kacur <jkacur@redhat.com> Link: https://lore.kernel.org/20250723161240.194860-2-gmonaco@redhat.com Fixes: 6d60f89691fc ("tools/rv: Add in-kernel monitor interface") Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/rvgen: Do not generate unused variablesNam Cao
ltl2k generates all variable definition in both ltl_start() and ltl_possible_next_states(). However, these two functions may not use all the variables, causing "unused variable" compiler warning. Change the script to only generate used variables. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/636b2b2d99a9bd46a9f77a078d44ebd7ffc7508c.1752850449.git.namcao@linutronix.de Signed-off-by: Nam Cao <namcao@linutronix.de> Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/rvgen: Generate each variable definition only onceNam Cao
If a variable appears multiple times in the specification, ltl2k generates multiple variable definitions. This fails the build. Make sure each variable is only defined once. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Cc: Gabriele Monaco <gmonaco@redhat.com> Link: https://lore.kernel.org/107dcf0d0aa8482d5fbe0314c3138f61cd284e91.1752850449.git.namcao@linutronix.de Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/rvgen: Support the 'next' operatorNam Cao
The 'next' operator is a unary operator. It is defined as: "next time, the operand must be true". Support this operator. For RV monitors, "next time" means the next invocation of ltl_validate(). Cc: John Ogness <john.ogness@linutronix.de> Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/9c32cec04dd18d2e956fddd84b0e0a2503daa75a.1752239482.git.namcao@linutronix.de Signed-off-by: Nam Cao <namcao@linutronix.de> Tested-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/rvgen: Add support for linear temporal logicNam Cao
Add support for generating RV monitors from linear temporal logic, similar to the generation of deterministic automaton monitors. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Cc: Gabriele Monaco <gmonaco@redhat.com> Link: https://lore.kernel.org/f3c63b363ff9c5af3302ba2b5d92a26a98700eaf.1751634289.git.namcao@linutronix.de Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/rvgen: Restructure the classes to prepare for LTL inclusionNam Cao
Both container generation and DA monitor generation is implemented in the class dot2k. That requires some ugly "if is_container ... else ...". If linear temporal logic support is added at the current state, the "if else" chain is longer and uglier. Furthermore, container generation is irrevelant to .dot files. It is therefore illogical to be implemented in class "dot2k". Clean it up, restructure the dot2k class into the following class hierarchy: (RVGenerator) /\ / \ / \ / \ / \ (Container) (Monitor) /\ / \ / \ / \ (dot2k) [ltl2k] <- intended This allows a simple and clean integration of LTL. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/692137a581ba6bee7a64d37fb7173ae137c47bbd.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/rvgen: Restructure the templates filesNam Cao
To simply the scripts and to allow easy integration of new monitor types, restructure the template files as followed: 1. Move the template files to be in the same directory as the rvgen package. Furthermore, the installation will now only install the templates to the package directory, not /usr/share/. This simplify templates reading, as the scripts do not need to find the templates at multiple places. 2. Move dot2k_templates/* to: - templates/dot2k/ - templates/container/ This allows sharing templates reading code between DA monitor generation and container generation (and any future generation type). For template files which can be shared between different generation types, support putting them in templates/ This restructure aligns with the recommendation from: https://python-packaging.readthedocs.io/en/latest/non-code-files.html Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/462d90273f96804d3ba850474877d5f727031258.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/dot2k: Prepare the frontend for LTL inclusionNam Cao
The dot2k tool has some code that can be reused for linear temporal logic monitor. Prepare its frontend for LTL inclusion: 1. Rename to be generic: rvgen 2. Replace the parameter --dot with 2 parameters: --class: to specific the monitor class, can be 'da' or 'ltl' --spec: the monitor specification file, .dot file for DA, and .ltl file for LTL The old command: python3 dot2/dot2k monitor -d wip.dot -t per_cpu is equivalent to the new commands: python3 rvgen monitor -c da -s wip.dot -t per_cpu Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/dea18f7a44374e4db8df5c7e785604bc3062ffc9.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/dot2k: Replace is_container() hack with subparsersNam Cao
dot2k is used for both generating deterministic automaton (DA) monitor and generating container monitor. Generating DA monitor and generating container requires different parameters. This is implemented by peeking at sys.argv and check whether "--container" is specified, and use that information to make some parameters optional or required. This works, but is quite hacky and ugly. Replace this hack with Python's built-in subparsers. The old commands: python3 dot2/dot2k -d wip.dot -t per_cpu python3 dot2/dot2k -n sched --container are equivalent to the new commands: python3 dot2/dot2k monitor -d wip.dot -t per_cpu python3 dot2/dot2k container -n sched Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/23c4e3c6e10c39e86d8e6a289208dde407efc4a8.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/dot2k: Remove __buff_to_string()Nam Cao
str.join() can do what __buff_to_string() does. Therefore replace __buff_to_string() to make the scripts more pythonic. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/860d6002659f604c743e0f23d5cf3c99ea6a82d8.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-24verification/dot2k: Make a separate dot2k_templates/Kconfig_containerNam Cao
A generated container's Kconfig has an incorrect line: select DA_MON_EVENTS_IMPLICIT This is due to container generation uses the same template Kconfig file as deterministic automaton monitor. Therefore, make a separate Kconfig template for container which has only the necessaries for container. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/d54fd7ee120785bec5695220e837dbbd6efb30e5.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-09rv: Add rtapp_sleep monitorNam Cao
Add a monitor for checking that real-time tasks do not go to sleep in a manner that may cause undesirable latency. Also change RV depends on TRACING to RV select TRACING to avoid the following recursive dependency: error: recursive dependency detected! symbol TRACING is selected by PREEMPTIRQ_TRACEPOINTS symbol PREEMPTIRQ_TRACEPOINTS depends on TRACE_IRQFLAGS symbol TRACE_IRQFLAGS is selected by RV_MON_SLEEP symbol RV_MON_SLEEP depends on RV symbol RV depends on TRACING Cc: John Ogness <john.ogness@linutronix.de> Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/75bc5bcc741d153aa279c95faf778dff35c5c8ad.1752088709.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-09rv: Add rtapp_pagefault monitorNam Cao
Userspace real-time applications may have design flaws that they raise page faults in real-time threads, and thus have unexpected latencies. Add an linear temporal logic monitor to detect this scenario. Cc: John Ogness <john.ogness@linutronix.de> Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Mathieu Desnoyers <mathieu.desnoyers@efficios.com> Link: https://lore.kernel.org/78fea8a2de6d058241d3c6502c1a92910772b0ed.1752088709.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Nam Cao <namcao@linutronix.de> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-03-27Merge tag 'trace-tools-v6.15' of ↵Linus Torvalds
git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace Pull tracing tooling updates from Steven Rostedt: - Allow RTLA to collect data via BPF The current implementation of rtla uses libtracefs and libtraceevent to pull sample events generated by the timerlat tracer from the trace buffer. rtla then processes the sample by updating the histogram and summary (current, maximum, minimum, and sum values) as well as checks if tracing has been stopped due to threshold overflow. In use cases where a large number of samples is being generated, that is, with measurements running on many CPUs and with a low interval, this sample processing design causes a significant CPU load on the rtla side. Furthermore, with >100 CPUs and 100us interval, rtla was reported as not being able to keep up with the samples and dropping most of them, leading to it being unusable. Change the way the timerlat trace processes samples by attaching a BPF program to the trace event using the BPF skeleton feature of bpftool. Unlike the current implementation, the BPF implementation does not check whether tracing is stopped (in BPF mode, tracing is always off to improve performance), but waits for a write to a BPF ringbuffer instead. This allows rtla to exit immediately when a threshold is violated, without waiting for the next iteration of the while loop. If the requirements for the BPF implementation are not met, either at build time or at run time, the current implementation is used as fallback. Which implementation is being used can be seen when running rtla timerlat with "-D" option. rtla can be forced to run in non-BPF mode by setting the RTLA_NO_BPF option to 1, for debugging purposes. - Fix LD_FLAGS from being dropped in build - Refactor code to remove duplication of save_trace_to_file - Always set options and do not rely on default settings Do not rely on the default kernel settings of the tracers when starting. They could have been changed by the user which gives inconsistent results. Always set the options that rtla expects. - Add creation of ctags and TAGS for traversing code * tag 'trace-tools-v6.15' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace: rtla: Add the ability to create ctags and etags rtla/tests: Test setting default options rtla/tests: Reset osnoise options before check rtla: Always set all tracer options rtla/osnoise: Set OSNOISE_WORKLOAD to true rtla: Unify apply_config between top and hist rtla/osnoise: Unify params struct rtla: Fix segfault in save_trace_to_file call tools/build: Use SYSTEM_BPFTOOL for system bpftool rtla: Refactor save_trace_to_file tools/rv: Keep user LDFLAGS in build rtla/timerlat: Test BPF mode rtla/timerlat_top: Use BPF to collect samples rtla/timerlat_top: Move divisor to update rtla/timerlat_hist: Use BPF to collect samples rtla/timerlat: Add BPF skeleton to collect samples rtla: Add optional dependency on BPF tooling tools/build: Add bpftool-skeletons feature test rtla/timerlat: Unify params struct
2025-03-27Merge tag 'trace-latency-v6.15' of ↵Linus Torvalds
git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace Pull latency tracing updates from Steven Rostedt: - Add some trace events to osnoise and timerlat sample generation This adds more information to the osnoise and timerlat tracers as well as allows BPF programs to be attached to these locations to extract even more data. - Fix to DECLARE_TRACE_CONDITION() macro It wasn't used but now will be and it happened to be broken causing the build to fail. - Add scheduler specification monitors to runtime verifier (RV) This is a continuation of Daniel Bristot's work. RV allows monitors to run and react concurrently. Running the cumulative model is equivalent to running single components using the same reactors, with the advantage that it's easier to point out which specification failed in case of error. This update introduces nested monitors to RV, in short, the sysfs monitor folder will contain a monitor named sched, which is nothing but an empty container for other monitors. Controlling the sched monitor (enable, disable, set reactors) controls all nested monitors. The following scheduling monitors are added: - sco: scheduling context operations Monitor to ensure sched_set_state happens only in thread context - tss: task switch while scheduling Monitor to ensure sched_switch happens only in scheduling context - snroc: set non runnable on its own context Monitor to ensure set_state happens only in the respective task's context - scpd: schedule called with preemption disabled Monitor to ensure schedule is called with preemption disabled - snep: schedule does not enable preempt Monitor to ensure schedule does not enable preempt - sncid: schedule not called with interrupt disabled Monitor to ensure schedule is not called with interrupt disabled * tag 'trace-latency-v6.15' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace: tools/rv: Allow rv list to filter for container Documentation/rv: Add docs for the sched monitors verification/dot2k: Add support for nested monitors tools/rv: Add support for nested monitors rv: Add scpd, snep and sncid per-cpu monitors rv: Add snroc per-task monitor rv: Add sco and tss per-cpu monitors rv: Add option for nested monitors and include sched sched: Add sched tracepoints for RV task model rv: Add license identifiers to monitor files tracing: Fix DECLARE_TRACE_CONDITION trace/osnoise: Add trace events for samples
2025-03-24tools/rv: Allow rv list to filter for containerGabriele Monaco
Add possibility to supply the container name to rv list: # rv list sched mon1 mon2 mon3 This lists only monitors in sched, without indentation. Supplying -h, any option (string starting with -) or more than 1 argument will still print the usage. Passing a non-existent container prints nothing and passing no container continues to print all monitors, showing indentation for nested monitors, reported after their container. Cc: Ingo Molnar <mingo@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Juri Lelli <juri.lelli@redhat.com> Link: https://lore.kernel.org/20250305140406.350227-10-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-03-24verification/dot2k: Add support for nested monitorsGabriele Monaco
RV now supports nested monitors, this functionality requires a container monitor, which has virtually no functionality besides holding other monitors, and nested monitors, that have a container as parent. Add the -p flag to pass a parent to a monitor, this sets it up while registering the monitor and adds necessary includes and configurations. Add the -c flag to create a container, since containers are empty, we don't allow supplying a dot model or a monitor type, the template is also different since functions to enable and disable the monitor are not defined, nor any tracepoint. The generated header file only allows to include the rv_monitor structure in children monitors. Cc: Ingo Molnar <mingo@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Juri Lelli <juri.lelli@redhat.com> Link: https://lore.kernel.org/20250305140406.350227-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-03-24tools/rv: Add support for nested monitorsGabriele Monaco
RV now supports nested monitors, this functionality requires a container monitor, which has virtually no functionality besides holding other monitors, and nested monitors, that have a container as parent. Nested monitors' sysfs folders are physically nested in the container's folder, and they are listed in the available_monitors file with the notation container:monitor. These changes go against the assumption that each line in the available_monitors file correspond to a folder in the rv directory, breaking the functionality of the rv tool. Add support for nested containers in the rv userspace tool, indenting nested monitors while listed and allowing both the notation with and without container name, which are equivalent: # rv list mon1 mon2 container: - nested1 - nested2 ## notation with container name # rv mon container:nested1 ## notation without container name # rv mon nested1 Either way, enabling a nested monitor is the same as enabling any other non-nested monitor. Selecting the container with rv mon enables all the nested monitors, if -t is passed, the trace also includes the monitor name next to the event: # rv mon nested1 -t <idle>-0 [004] event state1 x event -> state2 <idle>-0 [004] error event not expected in state2 # rv mon sched -t <idle>-0 [004] event_nested1 state1 x event -> state2 <idle>-0 [004] error_nested1 event not expected in state2 Cc: Ingo Molnar <mingo@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Juri Lelli <juri.lelli@redhat.com> Link: https://lore.kernel.org/20250305140406.350227-7-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-03-24rv: Add scpd, snep and sncid per-cpu monitorsGabriele Monaco
Add 3 per-cpu monitors as part of the sched model: * scpd: schedule called with preemption disabled Monitor to ensure schedule is called with preemption disabled * snep: schedule does not enable preempt Monitor to ensure schedule does not enable preempt * sncid: schedule not called with interrupt disabled Monitor to ensure schedule is not called with interrupt disabled To: Ingo Molnar <mingo@redhat.com> To: Peter Zijlstra <peterz@infradead.org> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Ingo Molnar <mingo@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: John Kacur <jkacur@redhat.com> Cc: Clark Williams <williams@redhat.com> Link: https://lore.kernel.org/20250305140406.350227-6-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-03-24rv: Add snroc per-task monitorGabriele Monaco
Add a per-task monitor as part of the sched model: * snroc: set non runnable on its own context Monitor to ensure set_state happens only in the respective task's context To: Ingo Molnar <mingo@redhat.com> To: Peter Zijlstra <peterz@infradead.org> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Ingo Molnar <mingo@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: John Kacur <jkacur@redhat.com> Cc: Clark Williams <williams@redhat.com> Link: https://lore.kernel.org/20250305140406.350227-5-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-03-24rv: Add sco and tss per-cpu monitorsGabriele Monaco
Add 2 per-cpu monitors as part of the sched model: * sco: scheduling context operations Monitor to ensure sched_set_state happens only in thread context * tss: task switch while scheduling Monitor to ensure sched_switch happens only in scheduling context To: Ingo Molnar <mingo@redhat.com> To: Peter Zijlstra <peterz@infradead.org> Cc: Juri Lelli <juri.lelli@redhat.com> Cc: Ingo Molnar <mingo@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: John Kacur <jkacur@redhat.com> Cc: Clark Williams <williams@redhat.com> Link: https://lore.kernel.org/20250305140406.350227-4-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-03-24sched: Add sched tracepoints for RV task modelGabriele Monaco
Add the following tracepoints: * sched_entry(bool preempt, ip) Called while entering __schedule * sched_exit(bool is_switch, ip) Called while exiting __schedule * sched_set_state(task, curr_state, state) Called when a task changes its state (to and from running) These tracepoints are useful to describe the Linux task model and are adapted from the patches by Daniel Bristot de Oliveira (https://bristot.me/linux-task-model/). Cc: Ingo Molnar <mingo@redhat.com> Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Juri Lelli <juri.lelli@redhat.com> Link: https://lore.kernel.org/20250305140406.350227-2-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Acked-by: Peter Zijlstra (Intel) <peterz@infradead.org> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-03-04tools/rv: Keep user LDFLAGS in buildTomas Glozar
rv, unlike rtla and perf, drops LDFLAGS supplied by the user and honors only EXTRA_LDFLAGS. This is inconsistent with both perf and rtla and can lead to all kinds of unexpected behavior. For example, on Fedora and RHEL, it causes rv to be build without PIE, unlike the aforementioned perf and rtla: $ file /usr/bin/{rv,rtla,perf} /usr/bin/rv: ELF 64-bit LSB executable, ... /usr/bin/rtla: ELF 64-bit LSB pie executable, ... /usr/bin/perf: ELF 64-bit LSB pie executable, ... Keep both LDFLAGS and EXTRA_LDFLAGS for the build. Cc: John Kacur <jkacur@redhat.com> Cc: Luis Goncalves <lgoncalv@redhat.com> Cc: Gabriele Monaco <gmonaco@redhat.com> Link: https://lore.kernel.org/20250304142228.767658-1-tglozar@redhat.com Fixes: 012e4e77df73 ("tools/verification: Use tools/build makefiles on rv") Signed-off-by: Tomas Glozar <tglozar@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-03-04rv: Add license identifiers to monitor filesGabriele Monaco
Some monitor files like the main header and the Kconfig are missing the license identifier. Add it to those and make sure the automatic generation script includes the line in newly created monitors. Cc: Masami Hiramatsu <mhiramat@kernel.org> Cc: Ingo Molnar <mingo@redhat.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Juri Lelli <juri.lelli@redhat.com> Link: https://lore.kernel.org/20250218123121.253551-3-gmonaco@redhat.com Signed-off-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-02-25Merge tag 'perf-tools-fixes-for-v6.14-2-2025-02-25' of ↵Linus Torvalds
git://git.kernel.org/pub/scm/linux/kernel/git/perf/perf-tools Pull perf tools fixes from Arnaldo Carvalho de Melo: - Fix tools/ quiet build Makefile infrastructure that was broken when working on tools/perf/ without testing on other tools/ living utilities. * tag 'perf-tools-fixes-for-v6.14-2-2025-02-25' of git://git.kernel.org/pub/scm/linux/kernel/git/perf/perf-tools: tools: Remove redundant quiet setup tools: Unify top-level quiet infrastructure