linux.git/tools/verification/models, branch v6.18.21

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)

rv: Add snroc per-task monitor

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

Add a per-task monitor as part of the sched model:

* snroc: set non runnable on its own context
    Monitor to ensure set_state happens only in the respective task's context

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-5-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco 
Signed-off-by: Steven Rostedt (Google)

rv: Add sco and tss per-cpu monitors

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

Add 2 per-cpu monitors as part of the sched model:

* sco: scheduling context operations
    Monitor to ensure sched_set_state happens only in thread context
* tss: task switch while scheduling
    Monitor to ensure sched_switch happens only in scheduling context

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-4-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco 
Signed-off-by: Steven Rostedt (Google)

rv/monitor: Add the wwnr monitor

2022-07-30T18:01:30+00:00

Per task wakeup while not running (wwnr) monitor.

This model is broken, the reason is that a task can be running in the
processor without being set as RUNNABLE. Think about a task about to
sleep:

1:      set_current_state(TASK_UNINTERRUPTIBLE);
2:      schedule();

And then imagine an IRQ happening in between the lines one and two,
waking the task up. BOOM, the wakeup will happen while the task is
running.

Q: Why do we need this model, so?
A: To test the reactors.

Link: https://lkml.kernel.org/r/473c0fc39967250fdebcff8b620311c11dccad30.1659052063.git.bristot@kernel.org

Cc: Wim Van Sebroeck 
Cc: Guenter Roeck 
Cc: Jonathan Corbet 
Cc: Ingo Molnar 
Cc: Thomas Gleixner 
Cc: Peter Zijlstra 
Cc: Will Deacon 
Cc: Catalin Marinas 
Cc: Marco Elver 
Cc: Dmitry Vyukov 
Cc: "Paul E. McKenney" 
Cc: Shuah Khan 
Cc: Gabriele Paoloni 
Cc: Juri Lelli 
Cc: Clark Williams 
Cc: Tao Zhou 
Cc: Randy Dunlap 
Cc: linux-doc@vger.kernel.org
Cc: linux-kernel@vger.kernel.org
Cc: linux-trace-devel@vger.kernel.org
Signed-off-by: Daniel Bristot de Oliveira 
Signed-off-by: Steven Rostedt (Google)

rv/monitor: Add the wip monitor

2022-07-30T18:01:30+00:00

The wakeup in preemptive (wip) monitor verifies if the
wakeup events always take place with preemption disabled:

                     |
                     |
                     v
                   #==================#
                   H    preemptive    H <+
                   #==================#  |
                     |                   |
                     | preempt_disable   | preempt_enable
                     v                   |
    sched_waking   +------------------+  |
  +--------------- |                  |  |
  |                |  non_preemptive  |  |
  +--------------> |                  | -+
                   +------------------+

The wakeup event always takes place with preemption disabled because
of the scheduler synchronization. However, because the preempt_count
and its trace event are not atomic with regard to interrupts, some
inconsistencies might happen.

The documentation illustrates one of these cases.

Link: https://lkml.kernel.org/r/c98ca678df81115fddc04921b3c79720c836b18f.1659052063.git.bristot@kernel.org

Cc: Wim Van Sebroeck 
Cc: Guenter Roeck 
Cc: Jonathan Corbet 
Cc: Ingo Molnar 
Cc: Thomas Gleixner 
Cc: Peter Zijlstra 
Cc: Will Deacon 
Cc: Catalin Marinas 
Cc: Marco Elver 
Cc: Dmitry Vyukov 
Cc: "Paul E. McKenney" 
Cc: Shuah Khan 
Cc: Gabriele Paoloni 
Cc: Juri Lelli 
Cc: Clark Williams 
Cc: Tao Zhou 
Cc: Randy Dunlap 
Cc: linux-doc@vger.kernel.org
Cc: linux-kernel@vger.kernel.org
Cc: linux-trace-devel@vger.kernel.org
Signed-off-by: Daniel Bristot de Oliveira 
Signed-off-by: Steven Rostedt (Google)