From 2bd30b8dc75b823dd7bbef9d7bc68e1fd7ecee5c Mon Sep 17 00:00:00 2001 From: Sang-Heon Jeon Date: Mon, 24 Aug 2026 01:18:14 +0900 Subject: coccinelle: alloc_cast: drop removed allocators - pci_alloc_consistent() and pci_zalloc_consistent() were removed by commit 7968778914e5 ("PCI: Remove the deprecated "pci-dma-compat.h" API") - kmem_alloc() was removed by commit f078d4ea8276 ("xfs: convert kmem_alloc() to kmalloc()") - kmem_zalloc() was removed by commit 10634530f7ba ("xfs: convert kmem_zalloc() to kzalloc()") - kmem_zone_alloc() and kmem_zone_zalloc() were removed by commit bae633a4a283 ("xfs: remove xfs_zone_{alloc,zalloc} helpers") So drop them from the rules. No functional change. Signed-off-by: Sang-Heon Jeon Signed-off-by: Julia Lawall --- tools/verification/models/deadline/nomiss.dot | 41 +++++++++++++++++++++++++++ tools/verification/models/rtapp/pagefault.ltl | 1 + tools/verification/models/rtapp/sleep.ltl | 20 +++++++++++++ tools/verification/models/rtapp/wakeup.ltl | 5 ++++ tools/verification/models/sched/nrp.dot | 29 +++++++++++++++++++ tools/verification/models/sched/opid.dot | 13 +++++++++ tools/verification/models/sched/sco.dot | 18 ++++++++++++ tools/verification/models/sched/scpd.dot | 18 ++++++++++++ tools/verification/models/sched/snep.dot | 18 ++++++++++++ tools/verification/models/sched/snroc.dot | 18 ++++++++++++ tools/verification/models/sched/sssw.dot | 30 ++++++++++++++++++++ tools/verification/models/sched/sts.dot | 38 +++++++++++++++++++++++++ tools/verification/models/stall.dot | 22 ++++++++++++++ tools/verification/models/wip.dot | 16 +++++++++++ tools/verification/models/wwnr.dot | 16 +++++++++++ 15 files changed, 303 insertions(+) create mode 100644 tools/verification/models/deadline/nomiss.dot create mode 100644 tools/verification/models/rtapp/pagefault.ltl create mode 100644 tools/verification/models/rtapp/sleep.ltl create mode 100644 tools/verification/models/rtapp/wakeup.ltl create mode 100644 tools/verification/models/sched/nrp.dot create mode 100644 tools/verification/models/sched/opid.dot create mode 100644 tools/verification/models/sched/sco.dot create mode 100644 tools/verification/models/sched/scpd.dot create mode 100644 tools/verification/models/sched/snep.dot create mode 100644 tools/verification/models/sched/snroc.dot create mode 100644 tools/verification/models/sched/sssw.dot create mode 100644 tools/verification/models/sched/sts.dot create mode 100644 tools/verification/models/stall.dot create mode 100644 tools/verification/models/wip.dot create mode 100644 tools/verification/models/wwnr.dot (limited to 'tools/verification/models') diff --git a/tools/verification/models/deadline/nomiss.dot b/tools/verification/models/deadline/nomiss.dot new file mode 100644 index 000000000..fd1ea6bf2 --- /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/pagefault.ltl b/tools/verification/models/rtapp/pagefault.ltl new file mode 100644 index 000000000..d7ce62102 --- /dev/null +++ b/tools/verification/models/rtapp/pagefault.ltl @@ -0,0 +1 @@ +RULE = always (RT imply not PAGEFAULT) diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl new file mode 100644 index 000000000..4d78fdd20 --- /dev/null +++ b/tools/verification/models/rtapp/sleep.ltl @@ -0,0 +1,20 @@ +RULE = always ((RT and SLEEP and USER_THREAD) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) + +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 not NANOSLEEP_CLOCK_REALTIME + +RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO + or WOKEN_BY_HARDIRQ + or WOKEN_BY_NMI + or ABORT_SLEEP + +ALLOWLIST = BLOCK_ON_RT_MUTEX + or FUTEX_LOCK_PI diff --git a/tools/verification/models/rtapp/wakeup.ltl b/tools/verification/models/rtapp/wakeup.ltl new file mode 100644 index 000000000..a5d63ca08 --- /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/nrp.dot b/tools/verification/models/sched/nrp.dot new file mode 100644 index 000000000..77bb64669 --- /dev/null +++ b/tools/verification/models/sched/nrp.dot @@ -0,0 +1,29 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = doublecircle] "any_thread_running"}; + {node [shape = circle] "any_thread_running"}; + {node [shape = circle] "nested_preempt"}; + {node [shape = plaintext, style=invis, label=""] "__init_preempt_irq"}; + {node [shape = circle] "preempt_irq"}; + {node [shape = circle] "rescheduling"}; + "__init_preempt_irq" -> "preempt_irq"; + "any_thread_running" [label = "any_thread_running", color = green3]; + "any_thread_running" -> "any_thread_running" [ label = "schedule_entry\nirq_entry" ]; + "any_thread_running" -> "rescheduling" [ label = "sched_need_resched" ]; + "nested_preempt" [label = "nested_preempt"]; + "nested_preempt" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "nested_preempt" -> "nested_preempt" [ label = "irq_entry" ]; + "nested_preempt" -> "preempt_irq" [ label = "sched_need_resched" ]; + "preempt_irq" [label = "preempt_irq"]; + "preempt_irq" -> "nested_preempt" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "preempt_irq" -> "preempt_irq" [ label = "irq_entry\nsched_need_resched" ]; + "rescheduling" [label = "rescheduling"]; + "rescheduling" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "rescheduling" -> "preempt_irq" [ label = "irq_entry" ]; + "rescheduling" -> "rescheduling" [ label = "sched_need_resched" ]; + { rank = min ; + "__init_preempt_irq"; + "preempt_irq"; + } +} diff --git a/tools/verification/models/sched/opid.dot b/tools/verification/models/sched/opid.dot new file mode 100644 index 000000000..511051fce --- /dev/null +++ b/tools/verification/models/sched/opid.dot @@ -0,0 +1,13 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {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_any"; + "any"; + } +} diff --git a/tools/verification/models/sched/sco.dot b/tools/verification/models/sched/sco.dot new file mode 100644 index 000000000..20b0e3b44 --- /dev/null +++ b/tools/verification/models/sched/sco.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext] "scheduling_context"}; + {node [shape = plaintext, style=invis, label=""] "__init_thread_context"}; + {node [shape = ellipse] "thread_context"}; + {node [shape = plaintext] "thread_context"}; + "__init_thread_context" -> "thread_context"; + "scheduling_context" [label = "scheduling_context"]; + "scheduling_context" -> "thread_context" [ label = "schedule_exit" ]; + "thread_context" [label = "thread_context", color = green3]; + "thread_context" -> "scheduling_context" [ label = "schedule_entry" ]; + "thread_context" -> "thread_context" [ label = "sched_set_state" ]; + { rank = min ; + "__init_thread_context"; + "thread_context"; + } +} diff --git a/tools/verification/models/sched/scpd.dot b/tools/verification/models/sched/scpd.dot new file mode 100644 index 000000000..340413896 --- /dev/null +++ b/tools/verification/models/sched/scpd.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext] "can_sched"}; + {node [shape = plaintext, style=invis, label=""] "__init_cant_sched"}; + {node [shape = ellipse] "cant_sched"}; + {node [shape = plaintext] "cant_sched"}; + "__init_cant_sched" -> "cant_sched"; + "can_sched" [label = "can_sched"]; + "can_sched" -> "can_sched" [ label = "schedule_entry\nschedule_exit" ]; + "can_sched" -> "cant_sched" [ label = "preempt_enable" ]; + "cant_sched" [label = "cant_sched", color = green3]; + "cant_sched" -> "can_sched" [ label = "preempt_disable" ]; + { rank = min ; + "__init_cant_sched"; + "cant_sched"; + } +} diff --git a/tools/verification/models/sched/snep.dot b/tools/verification/models/sched/snep.dot new file mode 100644 index 000000000..fe1300e93 --- /dev/null +++ b/tools/verification/models/sched/snep.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_non_scheduling_context"}; + {node [shape = ellipse] "non_scheduling_context"}; + {node [shape = plaintext] "non_scheduling_context"}; + {node [shape = plaintext] "scheduling_contex"}; + "__init_non_scheduling_context" -> "non_scheduling_context"; + "non_scheduling_context" [label = "non_scheduling_context", color = green3]; + "non_scheduling_context" -> "non_scheduling_context" [ label = "preempt_disable\npreempt_enable" ]; + "non_scheduling_context" -> "scheduling_contex" [ label = "schedule_entry" ]; + "scheduling_contex" [label = "scheduling_contex"]; + "scheduling_contex" -> "non_scheduling_context" [ label = "schedule_exit" ]; + { rank = min ; + "__init_non_scheduling_context"; + "non_scheduling_context"; + } +} diff --git a/tools/verification/models/sched/snroc.dot b/tools/verification/models/sched/snroc.dot new file mode 100644 index 000000000..8b71c32d4 --- /dev/null +++ b/tools/verification/models/sched/snroc.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_other_context"}; + {node [shape = ellipse] "other_context"}; + {node [shape = plaintext] "other_context"}; + {node [shape = plaintext] "own_context"}; + "__init_other_context" -> "other_context"; + "other_context" [label = "other_context", color = green3]; + "other_context" -> "own_context" [ label = "sched_switch_in" ]; + "own_context" [label = "own_context"]; + "own_context" -> "other_context" [ label = "sched_switch_out" ]; + "own_context" -> "own_context" [ label = "sched_set_state" ]; + { rank = min ; + "__init_other_context"; + "other_context"; + } +} diff --git a/tools/verification/models/sched/sssw.dot b/tools/verification/models/sched/sssw.dot new file mode 100644 index 000000000..4994c3e87 --- /dev/null +++ b/tools/verification/models/sched/sssw.dot @@ -0,0 +1,30 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_runnable"}; + {node [shape = doublecircle] "runnable"}; + {node [shape = circle] "runnable"}; + {node [shape = circle] "signal_wakeup"}; + {node [shape = circle] "sleepable"}; + {node [shape = circle] "sleeping"}; + "__init_runnable" -> "runnable"; + "runnable" [label = "runnable", color = green3]; + "runnable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup\nsched_switch_in\nsched_switch_yield\nsched_switch_preempt\nsignal_deliver" ]; + "runnable" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "runnable" -> "sleeping" [ label = "sched_switch_blocking" ]; + "signal_wakeup" [label = "signal_wakeup"]; + "signal_wakeup" -> "runnable" [ label = "signal_deliver" ]; + "signal_wakeup" -> "signal_wakeup" [ label = "sched_switch_in\nsched_switch_preempt\nsched_switch_yield\nsched_wakeup" ]; + "signal_wakeup" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "sleepable" [label = "sleepable"]; + "sleepable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup" ]; + "sleepable" -> "signal_wakeup" [ label = "sched_switch_yield" ]; + "sleepable" -> "sleepable" [ label = "sched_set_state_sleepable\nsched_switch_in\nsched_switch_preempt\nsignal_deliver" ]; + "sleepable" -> "sleeping" [ label = "sched_switch_suspend\nsched_switch_blocking" ]; + "sleeping" [label = "sleeping"]; + "sleeping" -> "runnable" [ label = "sched_wakeup" ]; + { rank = min ; + "__init_runnable"; + "runnable"; + } +} diff --git a/tools/verification/models/sched/sts.dot b/tools/verification/models/sched/sts.dot new file mode 100644 index 000000000..8f5f38be0 --- /dev/null +++ b/tools/verification/models/sched/sts.dot @@ -0,0 +1,38 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_can_sched"}; + {node [shape = doublecircle] "can_sched"}; + {node [shape = circle] "can_sched"}; + {node [shape = circle] "cant_sched"}; + {node [shape = circle] "disable_to_switch"}; + {node [shape = circle] "enable_to_exit"}; + {node [shape = circle] "in_irq"}; + {node [shape = circle] "scheduling"}; + {node [shape = circle] "switching"}; + "__init_can_sched" -> "can_sched"; + "can_sched" [label = "can_sched", color = green3]; + "can_sched" -> "cant_sched" [ label = "irq_disable" ]; + "can_sched" -> "scheduling" [ label = "schedule_entry" ]; + "cant_sched" [label = "cant_sched"]; + "cant_sched" -> "can_sched" [ label = "irq_enable" ]; + "cant_sched" -> "cant_sched" [ label = "irq_entry" ]; + "disable_to_switch" [label = "disable_to_switch"]; + "disable_to_switch" -> "enable_to_exit" [ label = "irq_enable" ]; + "disable_to_switch" -> "in_irq" [ label = "irq_entry" ]; + "disable_to_switch" -> "switching" [ label = "sched_switch" ]; + "enable_to_exit" [label = "enable_to_exit"]; + "enable_to_exit" -> "can_sched" [ label = "schedule_exit" ]; + "enable_to_exit" -> "enable_to_exit" [ label = "irq_disable\nirq_entry\nirq_enable" ]; + "in_irq" [label = "in_irq"]; + "in_irq" -> "in_irq" [ label = "irq_entry" ]; + "in_irq" -> "scheduling" [ label = "irq_enable" ]; + "scheduling" [label = "scheduling"]; + "scheduling" -> "disable_to_switch" [ label = "irq_disable" ]; + "switching" [label = "switching"]; + "switching" -> "enable_to_exit" [ label = "irq_enable" ]; + { rank = min ; + "__init_can_sched"; + "can_sched"; + } +} diff --git a/tools/verification/models/stall.dot b/tools/verification/models/stall.dot new file mode 100644 index 000000000..50077d1df --- /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"; + } +} diff --git a/tools/verification/models/wip.dot b/tools/verification/models/wip.dot new file mode 100644 index 000000000..2a53a9700 --- /dev/null +++ b/tools/verification/models/wip.dot @@ -0,0 +1,16 @@ +digraph state_automaton { + {node [shape = circle] "non_preemptive"}; + {node [shape = plaintext, style=invis, label=""] "__init_preemptive"}; + {node [shape = doublecircle] "preemptive"}; + {node [shape = circle] "preemptive"}; + "__init_preemptive" -> "preemptive"; + "non_preemptive" [label = "non_preemptive"]; + "non_preemptive" -> "non_preemptive" [ label = "sched_waking" ]; + "non_preemptive" -> "preemptive" [ label = "preempt_enable" ]; + "preemptive" [label = "preemptive"]; + "preemptive" -> "non_preemptive" [ label = "preempt_disable" ]; + { rank = min ; + "__init_preemptive"; + "preemptive"; + } +} diff --git a/tools/verification/models/wwnr.dot b/tools/verification/models/wwnr.dot new file mode 100644 index 000000000..1b206e831 --- /dev/null +++ b/tools/verification/models/wwnr.dot @@ -0,0 +1,16 @@ +digraph state_automaton { + {node [shape = plaintext, style=invis, label=""] "__init_not_running"}; + {node [shape = ellipse] "not_running"}; + {node [shape = plaintext] "not_running"}; + {node [shape = plaintext] "running"}; + "__init_not_running" -> "not_running"; + "not_running" [label = "not_running", color = green3]; + "not_running" -> "not_running" [ label = "wakeup" ]; + "not_running" -> "running" [ label = "switch_in" ]; + "running" [label = "running"]; + "running" -> "not_running" [ label = "switch_out" ]; + { rank = min ; + "__init_not_running"; + "not_running"; + } +} -- cgit v1.3.1