From 2b406fdb33387713cb9f880e58e5ff09901c6ebc Mon Sep 17 00:00:00 2001 From: Gabriele Monaco Date: Mon, 30 Mar 2026 13:10:05 +0200 Subject: rv: Convert the opid monitor to a hybrid automaton The opid monitor validates that wakeup and need_resched events only occur with interrupts and preemption disabled by following the preemptirq tracepoints. As reported in [1], those tracepoints might be inaccurate in some situations (e.g. NMIs). Since the monitor doesn't validate other ordering properties, remove the dependency on preemptirq tracepoints and convert the monitor to a hybrid automaton to validate the constraint during event handling. This makes the monitor more robust by also removing the workaround for interrupts missing the preemption tracepoints, which was working on PREEMPT_RT only and allows the monitor to be built on kernels without the preemptirqs tracepoints. [1] - https://lore.kernel.org/lkml/20250625120823.60600-1-gmonaco@redhat.com Reviewed-by: Nam Cao Link: https://lore.kernel.org/r/20260330111010.153663-8-gmonaco@redhat.com Signed-off-by: Gabriele Monaco --- tools/verification/models/sched/opid.dot | 36 +++++++------------------------- 1 file changed, 7 insertions(+), 29 deletions(-) (limited to 'tools') 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"; } } -- cgit v1.2.3