[PATCH v7 10/14] rv: Add tlob model DOT file
flat view
WARM3d
From: <hidden>
Date: 2026-10-11 19:40:45
Also in:
lkml
Subsystem:
runtime verification (rv), the rest · Maintainers:
Steven Rostedt, Gabriele Monaco, Linus Torvalds
From: Wen Yang <redacted> Add the Graphviz DOT specification of the tlob hybrid automaton to tools/verification/models/. The model has four states (stopped, running, waiting, sleeping) and six events (start, stop, sleep, preempt, wakeup, switch_in). A single clock invariant, clk_elapsed < BUDGET_NS(), holds in running, waiting and sleeping; stopped has no invariant, hence no timer. wakeup is a self-loop on running and waiting: a task that is already queued can still be the target of a traced wakeup, either by waking itself or through ttwu_runnable() while preempted, and neither case ends the budget window. stopped takes every scheduler event as a self-loop, so a task keeps going through the scheduler between windows. Suggested-by: Gabriele Monaco <gmonaco@redhat.com> Signed-off-by: Wen Yang <redacted> --- tools/verification/models/tlob.dot | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 tools/verification/models/tlob.dot
diff --git a/tools/verification/models/tlob.dot b/tools/verification/models/tlob.dot
new file mode 100644
index 000000000000..021a4d823548
--- /dev/null
+++ b/tools/verification/models/tlob.dot@@ -0,0 +1,27 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_stopped"}; + {node [shape = plaintext] "running"}; + {node [shape = plaintext] "waiting"}; + {node [shape = plaintext] "sleeping"}; + {node [shape = ellipse] "stopped"}; + "__init_stopped" -> "stopped"; + "running" [label = "running\nclk_elapsed <= BUDGET_NS()"]; + "waiting" [label = "waiting\nclk_elapsed <= BUDGET_NS()"]; + "sleeping" [label = "sleeping\nclk_elapsed <= BUDGET_NS()"]; + "stopped" [label = "stopped", color = green3]; + "running" -> "sleeping" [ label = "sleep" ]; + "running" -> "waiting" [ label = "preempt" ]; + "running" -> "running" [ label = "wakeup" ]; + "waiting" -> "running" [ label = "switch_in" ]; + "waiting" -> "waiting" [ label = "wakeup" ]; + "sleeping" -> "waiting" [ label = "wakeup" ]; + "running" -> "stopped" [ label = "stop" ]; + "stopped" -> "running" [ label = "start;reset(clk_elapsed)" ]; + "stopped" -> "stopped" [ label = "preempt\nsleep\nswitch_in\nwakeup" ]; + { rank = min ; + "__init_stopped"; + "stopped"; + } +}
--
2.25.1