linux/Documentation/trace/rv, branch master

rv: Add nomiss deadline monitor

2026-03-31T14:47:18Z

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 Reviewed-by: Juri Lelli Link: https://lore.kernel.org/r/20260330111010.153663-13-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

rv: Convert the opid monitor to a hybrid automaton

2026-03-31T14:47:17Z

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 Link: https://lore.kernel.org/r/20260330111010.153663-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

rv: Add sample hybrid monitor stall

2026-03-31T14:47:17Z

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 Link: https://lore.kernel.org/r/20260330111010.153663-7-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

Documentation/rv: Add documentation about hybrid automata

2026-03-31T14:47:17Z

Describe theory and implementation of hybrid automata in the dedicated page hybrid_automata.rst Include a section on how to integrate a hybrid automaton in monitor_synthesis.rst Also remove a hanging $ in deterministic_automata.rst Reviewed-by: Nam Cao Reviewed-by: Juri Lelli Link: https://lore.kernel.org/r/20260330111010.153663-6-gmonaco@redhat.com Signed-off-by: Gabriele Monaco

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)