diff options
| author | Gabriele Monaco <gmonaco@redhat.com> | 2026-03-30 14:10:04 +0300 |
|---|---|---|
| committer | Gabriele Monaco <gmonaco@redhat.com> | 2026-03-31 17:47:17 +0300 |
| commit | 13578a087152b85e53b1fa11639c814cb427808a (patch) | |
| tree | c566d3bdf4fba965c2a4bba0e42119241518d3b0 /tools | |
| parent | 708340c2714c4770f1cfac09f20fe7fc8a3acd09 (diff) | |
| download | linux-13578a087152b85e53b1fa11639c814cb427808a.tar.xz | |
rv: Add sample hybrid monitor stall
Add a sample monitor to showcase hybrid/timed automata.
The stall monitor identifies tasks stalled for longer than a threshold
and reacts when that happens.
Reviewed-by: Nam Cao <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260330111010.153663-7-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/verification/models/stall.dot | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/tools/verification/models/stall.dot b/tools/verification/models/stall.dot new file mode 100644 index 000000000000..50077d1dff74 --- /dev/null +++ b/tools/verification/models/stall.dot @@ -0,0 +1,22 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = circle] "enqueued"}; + {node [shape = plaintext, style=invis, label=""] "__init_dequeued"}; + {node [shape = doublecircle] "dequeued"}; + {node [shape = circle] "running"}; + "__init_dequeued" -> "dequeued"; + "enqueued" [label = "enqueued\nclk < threshold_jiffies"]; + "running" [label = "running"]; + "dequeued" [label = "dequeued", color = green3]; + "running" -> "running" [ label = "sched_switch_in\nsched_wakeup" ]; + "enqueued" -> "enqueued" [ label = "sched_wakeup" ]; + "enqueued" -> "running" [ label = "sched_switch_in" ]; + "running" -> "dequeued" [ label = "sched_switch_wait" ]; + "dequeued" -> "enqueued" [ label = "sched_wakeup;reset(clk)" ]; + "running" -> "enqueued" [ label = "sched_switch_preempt;reset(clk)" ]; + { rank = min ; + "__init_dequeued"; + "dequeued"; + } +} |