kernel/linux.git/Documentation/trace/rv, branch v6.18.41

Documentation/rv: Replace stale website link

2026-07-24T14:15:45+00:00

[ Upstream commit 49cbd359e4a7501e9d6694c072031d9ae6b2d1a5 ] The sched monitor page was linking to Daniel's website which is now down. The main purpose of the link was to point to a source for the models from the original author and that can be found also in his published paper. Replace the link with a reference to Daniel's "A thread synchronization model for the PREEMPT_RT Linux kernel" which can be found online and includes the models definitions as well as the work behind them (not the original patches but since they're based on a 5.0 kernel and are mostly included upstream, there's little value in keeping them in the docs). Fixes: 03abeaa63c08 ("Documentation/rv: Add docs for the sched monitors") Signed-off-by: Gabriele Monaco Acked-by: Matteo Martelli Tested-by: Matteo Martelli Tested-by: Randy Dunlap Acked-by: Randy Dunlap Signed-off-by: Jonathan Corbet Message-ID: <20260427131709.170505-2-gmonaco@redhat.com> Signed-off-by: Sasha Levin

Documentation/rv: Fix minor typo in monitor_synthesis page

2025-08-12T18:41:20+00:00

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: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)

verification/rvgen: Support the 'next' operator

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

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:47+00:00

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:46+00:00

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)

rv: Add documentation for rtapp monitor

2025-07-09T19:27:02+00:00

Add documentation describing the rtapp monitor. Cc: John Ogness Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/df0242d74c12511e82cc9d73c082def91a160c74.1752088709.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

Documentation/rv: Add sched pages to the indices

2025-03-27T16:02:38+00:00

The pages Documentation/tools/rv/rv-mon-sched.rst and Documentation/trace/rv/monitor_sched.rst were introduced but not included in any index. Add them to the respective indices. Cc: Jonathan Corbet Link: https://lore.kernel.org/20250327081240.46422-1-gmonaco@redhat.com Reported-by: Stephen Rothwell Fixes: 03abeaa63c08 ("Documentation/rv: Add docs for the sched monitors") Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)