kernel/linux.git/tools/verification, branch v6.19.11

rv: Add opid per-cpu monitor

2025-07-28T20:47:35+00:00

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 Cc: Masami Hiramatsu Cc: Ingo Molnar Cc: Peter Zijlstra Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250728135022.255578-10-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Acked-by: Nam Cao Tested-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

rv: Add nrp and sssw per-task monitors

2025-07-28T20:47:34+00:00

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 Cc: Jonathan Corbet Cc: Masami Hiramatsu Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Cc: Peter Zijlstra Link: https://lore.kernel.org/20250728135022.255578-9-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Acked-by: Nam Cao Tested-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

rv: Replace tss and sncid monitors with more complete sts

2025-07-28T20:47:34+00:00

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 Cc: Jonathan Corbet Cc: Masami Hiramatsu Cc: Nam Cao Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Cc: Peter Zijlstra Link: https://lore.kernel.org/20250728135022.255578-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)

rv: Return init error when registering monitors

2025-07-24T14:43:46+00:00

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 Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250723161240.194860-6-gmonaco@redhat.com Reviewed-by: Nam Cao Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)

verification/rvgen: Organise Kconfig entries for nested monitors

2025-07-24T14:43:46+00:00

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 Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250723161240.194860-5-gmonaco@redhat.com Reviewed-by: Nam Cao Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)

tools/dot2c: Fix generated files going over 100 column limit

2025-07-24T14:43:46+00:00

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 Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250723161240.194860-4-gmonaco@redhat.com Suggested-by: Nam Cao Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)

tools/rv: Stop gracefully also on SIGTERM

2025-07-24T14:43:46+00:00

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 Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur Link: https://lore.kernel.org/20250723161240.194860-3-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)

tools/rv: Do not skip idle in trace

2025-07-24T14:43:46+00:00

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 Cc: Tomas Glozar Cc: Juri Lelli Cc: Clark Williams Cc: John Kacur 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 Signed-off-by: Steven Rostedt (Google)

verification/rvgen: Do not generate unused variables

2025-07-24T14:43:23+00:00

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 Cc: Mathieu Desnoyers Link: https://lore.kernel.org/636b2b2d99a9bd46a9f77a078d44ebd7ffc7508c.1752850449.git.namcao@linutronix.de Signed-off-by: Nam Cao Reviewed-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)

verification/rvgen: Generate each variable definition only once

2025-07-24T14:43:23+00:00

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 Cc: Mathieu Desnoyers Cc: Gabriele Monaco Link: https://lore.kernel.org/107dcf0d0aa8482d5fbe0314c3138f61cd284e91.1752850449.git.namcao@linutronix.de Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)