verification/rvgen: Add selftests for rvgen kunit

The rvgen kunit command patches monitor files and adds necessary
definitions for kunit tests.

Add a test case validating its behaviour on dummy gen

verification/rvgen: Add selftests for rvgen kunit

The rvgen kunit command patches monitor files and adds necessary
definitions for kunit tests.

Add a test case validating its behaviour on dummy generated files and
comparing it against reference files, like it's done for rvgen monitor.

Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-11-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

show more ...

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 ...

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 ...

verification/rvgen: Add golden and spec folders for tests

Create reference models specifications and generated files in the golded
folder. Those can be used as reference to validate rvgen still gene

verification/rvgen: Add golden and spec folders for tests

Create reference models specifications and generated files in the golded
folder. Those can be used as reference to validate rvgen still generates
files as expected in automated tests.

Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-8-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

show more ...

tools/rv: Add selftests

The rv tool needs automated testing to catch regressions and verify
correct functionality across different usage scenarios.

Add selftests that validate monitor listing (incl

tools/rv: Add selftests

The rv tool needs automated testing to catch regressions and verify
correct functionality across different usage scenarios.

Add selftests that validate monitor listing (including containers and
nested monitors), monitor execution with different configurations
(reactors, verbose output, tracing), and trace output format for both
per-task and per-cpu monitors. Error handling paths are also tested.
Tests use a shared engine for common patterns.

Acked-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-7-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

show more ...

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 ...

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 ...

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 ...

tools/rv: Fix exit status when monitor execution fails

When running "rv mon" on a monitor that is already enabled, the tool
fails to start but incorrectly exits with a success status (0).

Fix the e

tools/rv: Fix exit status when monitor execution fails

When running "rv mon" on a monitor that is already enabled, the tool
fails to start but incorrectly exits with a success status (0).

Fix the exit condition to ensure it returns a failure code on any
execution error. Also use the standard EXIT_SUCCESS/EXIT_FAILURE macros
throughout the file.

Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-3-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

show more ...

rv: Use generic rv_this for the rv_monitor variable in LTL

Align the rv_monitor variable name in LTL to the generic rv_this as it
is already done for DA/HA monitors. This improves consistency and ea

rv: Use generic rv_this for the rv_monitor variable in LTL

Align the rv_monitor variable name in LTL to the generic rv_this as it
is already done for DA/HA monitors. This improves consistency and eases
assumptions across model classes.

Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260723074534.43521-2-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

show more ...

rv/rtapp: Add wakeup monitor

Add a wakeup monitor to detect a lower-priority task waking up a
higher-priority task.

The rtapp/sleep monitor already detects this. However, that monitor
triggers an e

rv/rtapp: Add wakeup monitor

Add a wakeup monitor to detect a lower-priority task waking up a
higher-priority task.

The rtapp/sleep monitor already detects this. However, that monitor
triggers an error in the context of the wakee task and user only gets
the stacktrace of that task. It is also extremely useful to get the
stacktrace of the waker task, which this monitor offers. In other
words, this monitor complements the rtapp/sleep monitor.

Signed-off-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/r/ba5658fa13e49ada466b84a2c211f233037180b5.1781852967.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

show more ...

rv/rtapp/sleep: Stop monitoring kernel threads

The rtapp/sleep monitor's primary purpose is detecting common mistakes
with user-space real-time design. Monitoring real-time issues with
kernel thread

rv/rtapp/sleep: Stop monitoring kernel threads

The rtapp/sleep monitor's primary purpose is detecting common mistakes
with user-space real-time design. Monitoring real-time issues with
kernel threads is a bonus.

However, accomodating kernel threads complicates the monitor due to
the edge cases which is seen by the monitor as lower-priority task
waking higher-priority task:

- kthread_stop() wakes up the task in order to stop it.

- The rcu thread and migration thread can be woken by any task.

- The ktimerd thread is woken near the end of irq_exit_rcu(), where
the preempt counter is "broken" and falsely says this is task
context. This requires the monitor to use the hardirq_context flag
instead of the preempt counter.

Beside complicating the monitor, the final case also requires enabling
CONFIG_TRACE_IRQFLAGS (so that "hardirq_context" can be used). This
adds overhead to the kernel even when the monitor is not active. This
may be an obstacle to enabling this monitor in distros' kernels.

Furthermore, kernel threads usually are started before the monitor is
enabled. Consequently, the threads' states (i.o.w. the monitor's
atomic propositions for the threads) are not fully known to the
monitor. As a result, the kernel threads mostly cannot be monitored.

Overall, the downsides of accomodating kernel threads outweights the
benefits. Thus, exclude kernel threads to simplify the monitor.

Signed-off-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/r/eec2ca5224bcdacc45b8e1eb2f0e68109e1cae7a.1781852967.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

show more ...

rv/rtapp/sleep: Update nanosleep rule

CLOCK_REALTIME is the only clock that often is misused in real-time
applications. The other clocks either are safe for real-time uses
(CLOCK_TAI, CLOCK_MONOTONI

rv/rtapp/sleep: Update nanosleep rule

CLOCK_REALTIME is the only clock that often is misused in real-time
applications. The other clocks either are safe for real-time uses
(CLOCK_TAI, CLOCK_MONOTONIC, CLOCK_BOOTTIME) or are unlikely to be misused
(CLOCK_AUX, CLOCK_PROCESS_CPUTIME_ID).

Update the monitor to only warn about CLOCK_REALTIME.

While at it, update the out-of-sync documentation.

Signed-off-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/r/c7ceb5c6263ee8f43a2676acae669cf486b0d903.1781852967.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

show more ...

rv/rtapp/sleep: Make the error more informative for user

The rtapp/sleep monitor detects real-time tasks which go to sleep in an
real-time-unsafe manner. If this happen, the monitor triggers a trace

rv/rtapp/sleep: Make the error more informative for user

The rtapp/sleep monitor detects real-time tasks which go to sleep in an
real-time-unsafe manner. If this happen, the monitor triggers a trace event
in the sched_wakeup tracepoint's handler.

However, the invoking context of that trace event is not the most
informative, because of the stack trace of that event is the wakeup's code
path which is not very helpful:

74.669317: rv:error_sleep: condvar[254]: violation detected
ltl_validate+0x345 ([kernel.kallsyms])
handle_sched_wakeup+0x34 ([kernel.kallsyms])
ttwu_do_activate+0xff ([kernel.kallsyms])
sched_ttwu_pending+0x104 ([kernel.kallsyms])
__flush_smp_call_function_queue+0x15b ([kernel.kallsyms])
__sysvec_call_function_single+0x18 ([kernel.kallsyms])
sysvec_call_function_single+0x66 ([kernel.kallsyms])
asm_sysvec_call_function_single+0x1a ([kernel.kallsyms])
pv_native_safe_halt+0xf ([kernel.kallsyms])
default_idle+0x9 ([kernel.kallsyms])
default_idle_call+0x33 ([kernel.kallsyms])
do_idle+0x234 ([kernel.kallsyms])
cpu_startup_entry+0x24 ([kernel.kallsyms])
start_secondary+0xf8 ([kernel.kallsyms])
common_startup_64+0x13e ([kernel.kallsyms])

What would be much more valuable is the stack trace of the task itself.

Instead of using the sched_wakeup tracepoint, use the sched_exit
tracepoint. This makes the event happen in the task's context, making
the stack trace far more informative for user:

rv:error_sleep: condvar[254]: violation detected
ltl_validate+0x345 ([kernel.kallsyms])
handle_sched_exit+0x39 ([kernel.kallsyms])
__schedule+0x80f ([kernel.kallsyms])
schedule+0x22 ([kernel.kallsyms])
futex_do_wait+0x33 ([kernel.kallsyms])
__futex_wait+0x8c ([kernel.kallsyms])
futex_wait+0x73 ([kernel.kallsyms])
do_futex+0xc6 ([kernel.kallsyms])
__x64_sys_futex+0x121 ([kernel.kallsyms])
do_syscall_64+0xf3 ([kernel.kallsyms])
entry_SYSCALL_64_after_hwframe+0x77 ([kernel.kallsyms])
__futex_abstimed_wait_common64+0xc6 (inlined)
__futex_abstimed_wait_common+0xc6 (/usr/lib/x86_64-linux-gnu/libc.so.6)

Signed-off-by: Nam Cao <namcao@linutronix.de>
Reviewed-by: Gabriele Monaco <gmonaco@redhat.com>
Link: https://lore.kernel.org/r/d97b4b5c476e5792b6875ec9bbf8dc214f999516.1781852967.git.namcao@linutronix.de
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>

show more ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...

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 ...