From b133207deb72609ad4da40c4d50128a5e150677b Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 30 Mar 2026 13:10:10 +0200 Subject: rv: Add nomiss deadline monitor Add the deadline monitors collection to validate the deadline scheduler, both for deadline tasks and servers. The currently implemented monitors are: * nomiss: validate dl entities run to completion before their deadiline Reviewed-by: Nam Cao Reviewed-by: Juri Lelli Link: https://lore.kernel.org/r/20260330111010.153663-13-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- tools/verification/models/deadline/nomiss.dot | 41 +++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 tools/verification/models/deadline/nomiss.dot (limited to 'tools') diff --git a/tools/verification/models/deadline/nomiss.dot b/tools/verification/models/deadline/nomiss.dot new file mode 100644 index 000000000000..fd1ea6bf2509 --- /dev/null +++ b/tools/verification/models/deadline/nomiss.dot @@ -0,0 +1,41 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = circle] "idle"}; + {node [shape = plaintext, style=invis, label=""] "__init_ready"}; + {node [shape = doublecircle] "ready"}; + {node [shape = circle] "ready"}; + {node [shape = circle] "running"}; + {node [shape = circle] "sleeping"}; + {node [shape = circle] "throttled"}; + "__init_ready" -> "ready"; + "idle" [label = "idle"]; + "idle" -> "idle" [ label = "dl_server_idle" ]; + "idle" -> "ready" [ label = "dl_replenish;reset(clk)" ]; + "idle" -> "running" [ label = "sched_switch_in" ]; + "idle" -> "sleeping" [ label = "dl_server_stop" ]; + "idle" -> "throttled" [ label = "dl_throttle" ]; + "ready" [label = "ready\nclk < DEADLINE_NS()", color = green3]; + "ready" -> "idle" [ label = "dl_server_idle" ]; + "ready" -> "ready" [ label = "sched_wakeup\ndl_replenish;reset(clk)" ]; + "ready" -> "running" [ label = "sched_switch_in" ]; + "ready" -> "sleeping" [ label = "dl_server_stop" ]; + "ready" -> "throttled" [ label = "dl_throttle;is_defer == 1" ]; + "running" [label = "running\nclk < DEADLINE_NS()"]; + "running" -> "idle" [ label = "dl_server_idle" ]; + "running" -> "running" [ label = "dl_replenish;reset(clk)\nsched_switch_in\nsched_wakeup" ]; + "running" -> "sleeping" [ label = "sched_switch_suspend\ndl_server_stop" ]; + "running" -> "throttled" [ label = "dl_throttle" ]; + "sleeping" [label = "sleeping"]; + "sleeping" -> "ready" [ label = "sched_wakeup\ndl_replenish;reset(clk)" ]; + "sleeping" -> "running" [ label = "sched_switch_in" ]; + "sleeping" -> "sleeping" [ label = "dl_server_stop\ndl_server_idle" ]; + "sleeping" -> "throttled" [ label = "dl_throttle;is_constr_dl == 1 || is_defer == 1" ]; + "throttled" [label = "throttled"]; + "throttled" -> "ready" [ label = "dl_replenish;reset(clk)" ]; + "throttled" -> "throttled" [ label = "sched_switch_suspend\nsched_wakeup\ndl_server_idle\ndl_throttle" ]; + { rank = min ; + "__init_ready"; + "ready"; + } +} -- cgit v1.2.3