kernel/linux.git/tools/verification/models, branch master

rv: Allow epoll in rtapp-sleep monitor

2026-04-01T13:18:30+00:00

Since commit 0c43094f8cc9 ("eventpoll: Replace rwlock with spinlock"), epoll_wait is real-time-safe syscall for sleeping. Add epoll_wait to the list of rt-safe sleeping APIs. Signed-off-by: Nam Cao Reviewed-by: Gabriele Monaco Link: https://lore.kernel.org/r/20260401130828.3115428-1-namcao@linutronix.de Signed-off-by: Gabriele Monaco

rv: Add nomiss deadline monitor

2026-03-31T14:47:18+00:00

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

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

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

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: Add rtapp_sleep monitor

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

Add a monitor for checking that real-time tasks do not go to sleep in a manner that may cause undesirable latency. Also change RV depends on TRACING to RV select TRACING to avoid the following recursive dependency: error: recursive dependency detected! symbol TRACING is selected by PREEMPTIRQ_TRACEPOINTS symbol PREEMPTIRQ_TRACEPOINTS depends on TRACE_IRQFLAGS symbol TRACE_IRQFLAGS is selected by RV_MON_SLEEP symbol RV_MON_SLEEP depends on RV symbol RV depends on TRACING Cc: John Ogness Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/75bc5bcc741d153aa279c95faf778dff35c5c8ad.1752088709.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

rv: Add rtapp_pagefault monitor

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

Userspace real-time applications may have design flaws that they raise page faults in real-time threads, and thus have unexpected latencies. Add an linear temporal logic monitor to detect this scenario. Cc: John Ogness Cc: Masami Hiramatsu Cc: Mathieu Desnoyers Link: https://lore.kernel.org/78fea8a2de6d058241d3c6502c1a92910772b0ed.1752088709.git.namcao@linutronix.de Reviewed-by: Gabriele Monaco Signed-off-by: Nam Cao Signed-off-by: Steven Rostedt (Google)

rv: Add scpd, snep and sncid per-cpu monitors

2025-03-24T21:27:39+00:00

Add 3 per-cpu monitors as part of the sched model: * scpd: schedule called with preemption disabled Monitor to ensure schedule is called with preemption disabled * snep: schedule does not enable preempt Monitor to ensure schedule does not enable preempt * sncid: schedule not called with interrupt disabled Monitor to ensure schedule is not called with interrupt disabled To: Ingo Molnar To: Peter Zijlstra Cc: Juri Lelli Cc: Ingo Molnar Cc: Peter Zijlstra Cc: John Kacur Cc: Clark Williams Link: https://lore.kernel.org/20250305140406.350227-6-gmonaco@redhat.com Signed-off-by: Gabriele Monaco Signed-off-by: Steven Rostedt (Google)