summaryrefslogtreecommitdiff
path: root/tools/verification/models
diff options
context:
space:
mode:
Diffstat (limited to 'tools/verification/models')
-rw-r--r--tools/verification/models/deadline/nomiss.dot41
-rw-r--r--tools/verification/models/rtapp/sleep.ltl12
-rw-r--r--tools/verification/models/rtapp/wakeup.ltl5
-rw-r--r--tools/verification/models/sched/opid.dot36
-rw-r--r--tools/verification/models/stall.dot22
5 files changed, 80 insertions, 36 deletions
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";
+ }
+}
diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl
index 6379bbeb6212..4d78fdd204c0 100644
--- a/tools/verification/models/rtapp/sleep.ltl
+++ b/tools/verification/models/rtapp/sleep.ltl
@@ -1,22 +1,20 @@
-RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
+RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST))
-RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD)
- and ((not WAKE) until RT_FRIENDLY_WAKE)
+RT_FRIENDLY_SLEEP = RT_VALID_SLEEP_REASON
+ and ((not SCHEDULE_IN) until RT_FRIENDLY_WAKE)
RT_VALID_SLEEP_REASON = FUTEX_WAIT
or RT_FRIENDLY_NANOSLEEP
+ or EPOLL_WAIT
RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP
and NANOSLEEP_TIMER_ABSTIME
- and (NANOSLEEP_CLOCK_MONOTONIC or NANOSLEEP_CLOCK_TAI)
+ and not NANOSLEEP_CLOCK_REALTIME
RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO
or WOKEN_BY_HARDIRQ
or WOKEN_BY_NMI
or ABORT_SLEEP
- or KTHREAD_SHOULD_STOP
ALLOWLIST = BLOCK_ON_RT_MUTEX
or FUTEX_LOCK_PI
- or TASK_IS_RCU
- or TASK_IS_MIGRATION
diff --git a/tools/verification/models/rtapp/wakeup.ltl b/tools/verification/models/rtapp/wakeup.ltl
new file mode 100644
index 000000000000..a5d63ca0811a
--- /dev/null
+++ b/tools/verification/models/rtapp/wakeup.ltl
@@ -0,0 +1,5 @@
+RULE = always (((RT and USER_THREAD) imply
+ (not (WOKEN_BY_LOWER_PRIO or WOKEN_BY_SOFTIRQ)) or ALLOWLIST))
+
+ALLOWLIST = BLOCK_ON_RT_MUTEX
+ or FUTEX_LOCK_PI
diff --git a/tools/verification/models/sched/opid.dot b/tools/verification/models/sched/opid.dot
index 840052f6952b..511051fce430 100644
--- a/tools/verification/models/sched/opid.dot
+++ b/tools/verification/models/sched/opid.dot
@@ -1,35 +1,13 @@
digraph state_automaton {
center = true;
size = "7,11";
- {node [shape = plaintext, style=invis, label=""] "__init_disabled"};
- {node [shape = circle] "disabled"};
- {node [shape = doublecircle] "enabled"};
- {node [shape = circle] "enabled"};
- {node [shape = circle] "in_irq"};
- {node [shape = circle] "irq_disabled"};
- {node [shape = circle] "preempt_disabled"};
- "__init_disabled" -> "disabled";
- "disabled" [label = "disabled"];
- "disabled" -> "disabled" [ label = "sched_need_resched\nsched_waking\nirq_entry" ];
- "disabled" -> "irq_disabled" [ label = "preempt_enable" ];
- "disabled" -> "preempt_disabled" [ label = "irq_enable" ];
- "enabled" [label = "enabled", color = green3];
- "enabled" -> "enabled" [ label = "preempt_enable" ];
- "enabled" -> "irq_disabled" [ label = "irq_disable" ];
- "enabled" -> "preempt_disabled" [ label = "preempt_disable" ];
- "in_irq" [label = "in_irq"];
- "in_irq" -> "enabled" [ label = "irq_enable" ];
- "in_irq" -> "in_irq" [ label = "sched_need_resched\nsched_waking\nirq_entry" ];
- "irq_disabled" [label = "irq_disabled"];
- "irq_disabled" -> "disabled" [ label = "preempt_disable" ];
- "irq_disabled" -> "enabled" [ label = "irq_enable" ];
- "irq_disabled" -> "in_irq" [ label = "irq_entry" ];
- "irq_disabled" -> "irq_disabled" [ label = "sched_need_resched" ];
- "preempt_disabled" [label = "preempt_disabled"];
- "preempt_disabled" -> "disabled" [ label = "irq_disable" ];
- "preempt_disabled" -> "enabled" [ label = "preempt_enable" ];
+ {node [shape = plaintext, style=invis, label=""] "__init_any"};
+ {node [shape = doublecircle] "any"};
+ "__init_any" -> "any";
+ "any" [label = "any", color = green3];
+ "any" -> "any" [ label = "sched_need_resched;irq_off == 1\nsched_waking;irq_off == 1 && preempt_off == 1" ];
{ rank = min ;
- "__init_disabled";
- "disabled";
+ "__init_any";
+ "any";
}
}
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";
+ }
+}
generated by cgit v1.2.3 (git 2.0.4) at 2026-09-24 23:08:06 +0000