linux-toradex.git/tools/verification/models/sched, branch master

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