linux/tools/verification/models/sched/sssw.dot
Gabriele Monaco e8440a88e5 rv: Add nrp and sssw per-task monitors
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 <mingo@redhat.com>
Cc: Jonathan Corbet <corbet@lwn.net>
Cc: Masami Hiramatsu <mhiramat@kernel.org>
Cc: Tomas Glozar <tglozar@redhat.com>
Cc: Juri Lelli <jlelli@redhat.com>
Cc: Clark Williams <williams@redhat.com>
Cc: John Kacur <jkacur@redhat.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Link: https://lore.kernel.org/20250728135022.255578-9-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Acked-by: Nam Cao <namcao@linutronix.de>
Tested-by: Nam Cao <namcao@linutronix.de>
Signed-off-by: Steven Rostedt (Google) <rostedt@goodmis.org>
2025-07-28 16:47:34 -04:00

30 lines
1.5 KiB
Text

digraph state_automaton {
center = true;
size = "7,11";
{node [shape = plaintext, style=invis, label=""] "__init_runnable"};
{node [shape = doublecircle] "runnable"};
{node [shape = circle] "runnable"};
{node [shape = circle] "signal_wakeup"};
{node [shape = circle] "sleepable"};
{node [shape = circle] "sleeping"};
"__init_runnable" -> "runnable";
"runnable" [label = "runnable", color = green3];
"runnable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup\nsched_switch_in\nsched_switch_yield\nsched_switch_preempt\nsignal_deliver" ];
"runnable" -> "sleepable" [ label = "sched_set_state_sleepable" ];
"runnable" -> "sleeping" [ label = "sched_switch_blocking" ];
"signal_wakeup" [label = "signal_wakeup"];
"signal_wakeup" -> "runnable" [ label = "signal_deliver" ];
"signal_wakeup" -> "signal_wakeup" [ label = "sched_switch_in\nsched_switch_preempt\nsched_switch_yield\nsched_wakeup" ];
"signal_wakeup" -> "sleepable" [ label = "sched_set_state_sleepable" ];
"sleepable" [label = "sleepable"];
"sleepable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup" ];
"sleepable" -> "signal_wakeup" [ label = "sched_switch_yield" ];
"sleepable" -> "sleepable" [ label = "sched_set_state_sleepable\nsched_switch_in\nsched_switch_preempt\nsignal_deliver" ];
"sleepable" -> "sleeping" [ label = "sched_switch_suspend\nsched_switch_blocking" ];
"sleeping" [label = "sleeping"];
"sleeping" -> "runnable" [ label = "sched_wakeup" ];
{ rank = min ;
"__init_runnable";
"runnable";
}
}