kernel/Documentation/trace/rv, branch master

Merge tag 'trace-rv-v7.0' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace

2026-02-12T22:08:49Z

Pull runtime verifier updates from Steven Rostedt: - Refactor da_monitor to minimize macros Complete refactor of da_monitor.h to reduce reliance on macros generating functions. Use generic static functions and uses the preprocessor only when strictly necessary (e.g. for tracepoint handlers). The change essentially relies on functions with generic names (e.g. da_handle) instead of monitor-specific as well adding the need to define constant (e.g. MONITOR_NAME, MONITOR_TYPE) before including the header rather than calling macros that would define functions. Also adapt monitors and documentation accordingly. - Cleanup DA code generation scripts Clean up functions in dot2c removing reimplementations of trivial library functions (__buff_to_string) and removing some other unused intermediate steps. - Annotate functions with types in the rvgen python scripts - Remove superfluous assignments and cleanup generated code The rvgen scripts generate a superfluous assignment to 0 for enum variables and don't add commas to the last elements, which is against the kernel coding standards. Change the generation process for a better compliance and slightly simpler logic. - Remove superfluous declarations from generated code The monitor container source files contained a declaration and a definition for the rv_monitor variable. The former is superfluous and was removed. - Fix reference to outdated documentation s/da_monitor_synthesis.rst/monitor_synthesis.rst in comment in da_monitor.h * tag 'trace-rv-v7.0' of git://git.kernel.org/pub/scm/linux/kernel/git/trace/linux-trace: rv: Fix documentation reference in da_monitor.h verification/rvgen: Remove unused variable declaration from containers verification/dot2c: Remove superfluous enum assignment and add last comma verification/dot2c: Remove __buff_to_string() and cleanup verification/rvgen: Annotate DA functions with types verification/rvgen: Adapt dot2k and templates after refactoring da_monitor.h Documentation/rv: Adapt documentation after da_monitor refactoring rv: Cleanup da_monitor after refactor rv: Refactor da_monitor to minimise macros

Documentation/rv: Adapt documentation after da_monitor refactoring

2026-01-12T06:43:50Z

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_(name, type) is substituted by #define RV_MON_TYPE RV_MON_ da_handle_event_() is substituted by da_handle_event() Update the documentation to reflect the changes. Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20251126104241.291258-4-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

Documentation/rv: Fix dead link to monitor_synthesis.rst

2025-12-22T22:30:26Z

The file 'da_monitor_synthesis.rst' was renamed to 'monitor_synthesis.rst' in commit f40a7c06020709 ("Documentation/rv: Prepare monitor synthesis document for LTL inclusion"). Signed-off-by: Soham Metha Fixes: f40a7c06020709 ("Documentation/rv: Prepare monitor synthesis document for LTL inclusion") Acked-by: Gabriele Monaco Signed-off-by: Jonathan Corbet Message-ID: <20251204032452.9523-1-sohammetha01@gmail.com>

Documentation/rv: Fix minor typo in monitor_synthesis page

2025-08-12T18:41:20Z

Specifically, fix spelling of "practice" Signed-off-by: Gopi Krishna Menon Signed-off-by: Jonathan Corbet Link: https://lore.kernel.org/r/20250810111249.93181-1-krishnagopi487@gmail.com

rv: Add opid per-cpu monitor

2025-07-28T20:47:35Z

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:34Z

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:34Z

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)

verification/rvgen: Support the 'next' operator

2025-07-24T14:43:23Z

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

Documentation/rv: Add documentation for linear temporal logic monitors

2025-07-24T14:42:47Z

Add documents describing linear temporal logic runtime verification monitors and how to generate them using rvgen. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Cc: Gabriele Monaco Link: https://lore.kernel.org/be13719e66fd8da147d7c69d5365aa23c52b743f.1751634289.git.namcao@linutronix.de Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

Documentation/rv: Prepare monitor synthesis document for LTL inclusion

2025-07-24T14:42:46Z

Monitor synthesis from deterministic automaton and linear temporal logic have a lot in common. Therefore a single document should describe both. Change da_monitor_synthesis.rst to monitor_synthesis.rst. LTL monitor synthesis will be added to this file by a follow-up commit. This makes the diff far easier to read. If renaming and adding LTL info is done in a single commit, git wouldn't recognize it as a rename, but a file removal and a file addition. While at it, correct the old dot2k commands to the new rvgen commands. Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/d91c6e4600287f4732d68a014219e576a75ce6dc.1751634289.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)