| 5b4b6ef9 | 23-Jul-2026 |
Gabriele Monaco <gmonaco@redhat.com> |
verification/rvgen: Add the rvgen kunit subcommand
Add the rvgen kunit subcommand to patch an already generated monitor for
kunit support. It parses the handlers and create the necessary structs
and
verification/rvgen: Add the rvgen kunit subcommand
Add the rvgen kunit subcommand to patch an already generated monitor for
kunit support. It parses the handlers and create the necessary structs
and initialisations.
The only remaining manual steps are importing the test in the runner
and writing the test itself.
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-10-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 36c1af42 | 23-Jul-2026 |
Gabriele Monaco <gmonaco@redhat.com> |
verification/rvgen: Add selftests
The rvgen code generator needs validation to ensure it produces correct
monitor implementations from input specifications.
Add selftests with golden reference outp
verification/rvgen: Add selftests
The rvgen code generator needs validation to ensure it produces correct
monitor implementations from input specifications.
Add selftests with golden reference outputs covering all monitor classes
(DA, HA, LTL) and types (global, per_cpu, per_task, per_obj), including
optional features like descriptions and parent monitors. Container
generation and error handling (missing files, invalid specifications,
missing arguments) are also validated against expected output.
Acked-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Wen Yang <wen.yang@linux.dev>
Link: https://lore.kernel.org/r/20260723074534.43521-9-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 0ab69fdd | 23-Jul-2026 |
Gabriele Monaco <gmonaco@redhat.com> |
verification/rvgen: Improve consistency in template files
Template files for rvgen had minor inconsistencies in their
placeholders for default author and default tracepoint examples. The
user needs
verification/rvgen: Improve consistency in template files
Template files for rvgen had minor inconsistencies in their
placeholders for default author and default tracepoint examples. The
user needs to modify those anyway but keeping consistency may help in
bulk editing or checking.
Change default author from "dot2k: auto-generated" (for DA/containers)
or /* TODO */ (for LTL) to the general "rvgen: auto-generated".
Align the sample tracepoint handler name in LTL template to
handle_example_event, consistently with the rest of the file.
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-6-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 85b43f84 | 23-Jul-2026 |
Gabriele Monaco <gmonaco@redhat.com> |
verification/rvgen: Use pathlib instead of os.path
Migrate to the newer patlib library, bundled with python since 3.4 to
increase readability over using os.path.
Reviewed-by: Nam Cao <namcao@linutr
verification/rvgen: Use pathlib instead of os.path
Migrate to the newer patlib library, bundled with python since 3.4 to
increase readability over using os.path.
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-5-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| c737b725 | 23-Jul-2026 |
Gabriele Monaco <gmonaco@redhat.com> |
verification/rvgen: Improve rv_dir discovery in RVGenerator
The RVGenerator class can find the RV directory (kernel/trace/rv) in the
kernel tree to do some auto patching. This works by assuming PWD
verification/rvgen: Improve rv_dir discovery in RVGenerator
The RVGenerator class can find the RV directory (kernel/trace/rv) in the
kernel tree to do some auto patching. This works by assuming PWD is
either the kernel tree or tools/verification, which isn't always the
case (e.g. when running from selftests).
Make discovery more robust by relying on the absolute path of the
current script and traversing backwards the right number of times.
This should work from any location if rvgen is in the kernel tree.
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-4-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 2a8cd68c | 01-Jun-2026 |
Gabriele Monaco <gmonaco@redhat.com> |
verification/rvgen: Generate cleanup hook for per-obj monitor
Per-object monitors can allocate memory dynamically and such memory is
required for the lifetime of the object, then it should be freed
verification/rvgen: Generate cleanup hook for per-obj monitor
Per-object monitors can allocate memory dynamically and such memory is
required for the lifetime of the object, then it should be freed with
the appropriate call.
Force the generation scripts to add a cleanup function the user will
need to wire to the appropriate event (e.g. sched_process_exit for
tasks). This can be safely removed if the object will never cease to
exist before disabling the monitor (e.g. if following only static
variables).
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260601153840.124372-14-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| da245fae | 18-Jun-2026 |
Yu Chuanyu <lucayu.alight@gmail.com> |
rv: Update rvgen monitor synthesis documentation path
The rvgen source comments still refer to da_monitor_synthesis.rst, which
no longer exists. The documentation is now available in
monitor_synthes
rv: Update rvgen monitor synthesis documentation path
The rvgen source comments still refer to da_monitor_synthesis.rst, which
no longer exists. The documentation is now available in
monitor_synthesis.rst. Update both references to point to the current
file.
Signed-off-by: Yu Chuanyu <lucayu.alight@gmail.com>
Acked-by: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/r/20260618-rvgen-doc-path-v1-1-9bcf0148417a@gmail.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| fc0663ec | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Remove dead code
The conversion to use Lark left some dead code behind. Remove them.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.
verification/rvgen: Remove dead code
The conversion to use Lark left some dead code behind. Remove them.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/98115605a49c819adae9329823d4010bf181c3b7.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 7edaba05 | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Remove the old state variables
The state variables (states, initial_state, final_states) only capture the
states' names and have less information than their Lark-based counterpar
verification/rvgen: Remove the old state variables
The state variables (states, initial_state, final_states) only capture the
states' names and have less information than their Lark-based counterparts.
Switch to use the new state variables and delete these old ones.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/c1e214623f83a6d8a97b6ffa54ce8ec106b11c65.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| cad252db | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Switch __create_matrix() to Lark
Switch __create_matrix() to use the transitions parsed by Lark to avoid all
the raw text parsing.
Also stop parsing constraints in __create_matr
verification/rvgen: Switch __create_matrix() to Lark
Switch __create_matrix() to use the transitions parsed by Lark to avoid all
the raw text parsing.
Also stop parsing constraints in __create_matrix(), that is not used
anymore.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/36e76b64049b7fef1cf5c2855fea310c0452ee38.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 8aa51cb4 | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Switch __get_event_variables() to Lark
Switch __get_event_variables() to use the parsed results from Lark, instead
of raw text processing.
Reviewed-by: Gabriele Monaco <gmonaco@
verification/rvgen: Switch __get_event_variables() to Lark
Switch __get_event_variables() to use the parsed results from Lark, instead
of raw text processing.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/03f6457b4fcaa64199ffe73edb2a9fc48e76a839.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 35266cc3 | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Delete __parse_constraint()
All previous users of self.invariants and self.guards have been converted
to the Lark parser, delete __parse_constraints() and its associates.
Signed
verification/rvgen: Delete __parse_constraint()
All previous users of self.invariants and self.guards have been converted
to the Lark parser, delete __parse_constraints() and its associates.
Signed-off-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/r/b22a5a3822fe53afb8e2cf1df623a0e4c9ed5f49.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 62247351 | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Simplify the generation for clock variables
Hybrid automata monitors's clock variables have been changed to have
only a single representation. Now there is no need to generate co
verification/rvgen: Simplify the generation for clock variables
Hybrid automata monitors's clock variables have been changed to have
only a single representation. Now there is no need to generate code to
convert between the two representations.
Delete __fill_convert_inv_guard_func() and its associates. Update
__start_to_invariant_check() to how invariants now work.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/0d2a8e4bf90a9ed959289ddd2190b1152e4bbadf.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| e0235729 | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Convert __fill_verify_guards_func() to Lark
Prepare to remove self.guards and self.__parse_constraints(), convert
__fill_verify_guards_func() to use the parsed transitions from L
verification/rvgen: Convert __fill_verify_guards_func() to Lark
Prepare to remove self.guards and self.__parse_constraints(), convert
__fill_verify_guards_func() to use the parsed transitions from Lark.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/4f18c30b60d7c7138c0016cd6985d14a898b1eec.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| beb3a26e | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Convert __fill_setup_invariants_func() to Lark
Prepare for self.invariants and __parse_constraints() to be removed.
convert __fill_setup_invariants_func() to use the new parsed s
verification/rvgen: Convert __fill_setup_invariants_func() to Lark
Prepare for self.invariants and __parse_constraints() to be removed.
convert __fill_setup_invariants_func() to use the new parsed states from
Lark.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/1e6e95ae085b21155f9ba97359659fa231d1b803.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 75092d5a | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Convert __fill_verify_invariants_func() to Lark
Convert __fill_verify_invariants_func() to use the parsed states
information from Lark, prepare to remove the old raw text parsing
verification/rvgen: Convert __fill_verify_invariants_func() to Lark
Convert __fill_verify_invariants_func() to use the parsed states
information from Lark, prepare to remove the old raw text parsing code.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/dce2a7dd9e9644e1c4c7ddf696c1b695b14157eb.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| a9fb612d | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Implement state and transition parser based on Lark
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly c
verification/rvgen: Implement state and transition parser based on Lark
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly changed (for
instance, by breaking long some lines which is allowed by the DOT
language), the scripts would fail.
Prepare to move away from the raw text processing, implement parsers based
on Lark which parse states, transitions and constraints.
The parse results are not used yet. The existing scripts will be converted
one by one to them, and the raw text processing will eventually be removed.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/3ef60fdb03154abb9d9718ea106484213e1a4598.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| eb46aecc | 19-Jun-2026 |
Nam Cao <namcao@linutronix.de> |
verification/rvgen: Introduce a parse tree for automata using Lark
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly change
verification/rvgen: Introduce a parse tree for automata using Lark
The DOT parsing scripts directly parse the raw text and they are quite
fragile. If the input dot files' formats are slightly changed (for
instance, by breaking long some lines which is allowed by the DOT language
defined by graphviz), the scripts would fail.
To make the scripts robust, the parser should be implemented based on the
dot language specification, not based on how the existing dot files look.
As a first step, use Lark to implement a Parser based on the graphviz dot
language specification. The resulting parse tree is not used yet, but the
existing scripts will be converted one by one to use this new parse tree in
the follow-up commits.
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Signed-off-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/f816bce4cc7c48d0b6b6a28a7029459df69d6a71.1781847583.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| df996599 | 14-May-2026 |
Gabriele Monaco <gmonaco@redhat.com> |
verification/rvgen: Fix ltl2k writing True as a literal
The rvgen parser for LTL stores literal true values in the python
representation (capitalised True), this doesn't build in C.
The Literal clas
verification/rvgen: Fix ltl2k writing True as a literal
The rvgen parser for LTL stores literal true values in the python
representation (capitalised True), this doesn't build in C.
The Literal class should already handle this case but ASTNode skips its
strigification method and converts the value (true/false) directly.
Fix by delegating ASTNode stringification to the Literal and Variable
classes instead of bypassing them.
Fixes: 97ffa4ce6ab32 ("verification/rvgen: Add support for linear temporal logic")
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260514152055.229162-8-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|
| 5f845ad7 | 14-May-2026 |
Gabriele Monaco <gmonaco@redhat.com> |
verification/rvgen: Fix options shared among commands
After rvgen was refactored to use subparsers, the common options (-a and
-D) were left in the main parser. This meant that they needed to be
cal
verification/rvgen: Fix options shared among commands
After rvgen was refactored to use subparsers, the common options (-a and
-D) were left in the main parser. This meant that they needed to be
called /before/ the subcommand and using them without subcommand was
allowed. This is not the original intent.
rvgen -D "some description" container -n name
Define the options as parent in the subparsers to allow them to be used
from both subcommands together with other options.
rvgen container -n name -D "some description"
Fixes: 5270a0e3041c ("verification/dot2k: Replace is_container() hack with subparsers")
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260514152055.229162-7-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
show more ...
|