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