diff options
| author | Gabriele Monaco <gmonaco@redhat.com> | 2026-03-30 13:10:04 +0200 |
|---|---|---|
| committer | Gabriele Monaco <gmonaco@redhat.com> | 2026-03-31 16:47:17 +0200 |
| commit | 13578a087152b85e53b1fa11639c814cb427808a (patch) | |
| tree | c566d3bdf4fba965c2a4bba0e42119241518d3b0 /Documentation/trace | |
| parent | 708340c2714c4770f1cfac09f20fe7fc8a3acd09 (diff) | |
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 'Documentation/trace')
| -rw-r--r-- | Documentation/trace/rv/index.rst | 1 | ||||
| -rw-r--r-- | Documentation/trace/rv/monitor_stall.rst | 43 |
2 files changed, 44 insertions, 0 deletions
diff --git a/Documentation/trace/rv/index.rst b/Documentation/trace/rv/index.rst index ad298784bda2..bf9962f49959 100644 --- a/Documentation/trace/rv/index.rst +++ b/Documentation/trace/rv/index.rst @@ -16,3 +16,4 @@ Runtime Verification monitor_wwnr.rst monitor_sched.rst monitor_rtapp.rst + monitor_stall.rst diff --git a/Documentation/trace/rv/monitor_stall.rst b/Documentation/trace/rv/monitor_stall.rst new file mode 100644 index 000000000000..d29e820b2433 --- /dev/null +++ b/Documentation/trace/rv/monitor_stall.rst @@ -0,0 +1,43 @@ +Monitor stall +============= + +- Name: stall - stalled task monitor +- Type: per-task hybrid automaton +- Author: Gabriele Monaco <gmonaco@redhat.com> + +Description +----------- + +The stalled task (stall) monitor is a sample per-task timed monitor that checks +if tasks are scheduled within a defined threshold after they are ready:: + + | + | + v + #==========================# + +-----------------> H dequeued H + | #==========================# + | | + sched_switch_wait | sched_wakeup;reset(clk) + | v + | +--------------------------+ <+ + | | enqueued | | sched_wakeup + | | clk < threshold_jiffies | -+ + | +--------------------------+ + | | ^ + | sched_switch_in sched_switch_preempt;reset(clk) + | v | + | +--------------------------+ + +------------------ | running | + +--------------------------+ + ^ sched_switch_in | + | sched_wakeup | + +----------------------+ + +The threshold can be configured as a parameter by either booting with the +``stall.threshold_jiffies=<new value>`` argument or writing a new value to +``/sys/module/stall/parameters/threshold_jiffies``. + +Specification +------------- +Graphviz Dot file in tools/verification/models/stall.dot |