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 <namcao@linutronix.de>
Link: https://lore.kernel.org/r/20260330111010.153663-8-gmonaco@redhat.com
Signed-off-by: Gabriele Monaco <gmonaco@redhat.com>
This commit is contained in:
Gabriele Monaco
2026-03-30 13:10:05 +02:00
parent 13578a0871
commit 2b406fdb33
7 changed files with 82 additions and 230 deletions

View File

@@ -346,55 +346,21 @@ Monitor opid
The operations with preemption and irq disabled (opid) monitor ensures
operations like ``wakeup`` and ``need_resched`` occur with interrupts and
preemption disabled or during interrupt context, in such case preemption may
not be disabled explicitly.
preemption disabled.
``need_resched`` can be set by some RCU internals functions, in which case it
doesn't match a task wakeup and might occur with only interrupts disabled::
doesn't match a task wakeup and might occur with only interrupts disabled.
The interrupt and preemption status are validated by the hybrid automaton
constraints when processing the events::
| sched_need_resched
| sched_waking
| irq_entry
| +--------------------+
v v |
+------------------------------------------------------+
+----------- | disabled | <+
| +------------------------------------------------------+ |
| | ^ |
| | preempt_disable sched_need_resched |
| preempt_enable | +--------------------+ |
| v | v | |
| +------------------------------------------------------+ |
| | irq_disabled | |
| +------------------------------------------------------+ |
| | | ^ |
| irq_entry irq_entry | | |
| sched_need_resched v | irq_disable |
| sched_waking +--------------+ | | |
| +----- | | irq_enable | |
| | | in_irq | | | |
| +----> | | | | |
| +--------------+ | | irq_disable
| | | | |
| irq_enable | irq_enable | | |
| v v | |
| #======================================================# |
| H enabled H |
| #======================================================# |
| | ^ ^ preempt_enable | |
| preempt_disable preempt_enable +--------------------+ |
| v | |
| +------------------+ | |
+----------> | preempt_disabled | -+ |
+------------------+ |
| |
+-------------------------------------------------------+
This monitor is designed to work on ``PREEMPT_RT`` kernels, the special case of
events occurring in interrupt context is a shortcut to identify valid scenarios
where the preemption tracepoints might not be visible, during interrupts
preemption is always disabled. On non- ``PREEMPT_RT`` kernels, the interrupts
might invoke a softirq to set ``need_resched`` and wake up a task. This is
another special case that is currently not supported by the monitor.
|
|
v
#=========# sched_need_resched;irq_off == 1
H H sched_waking;irq_off == 1 && preempt_off == 1
H any H ------------------------------------------------+
H H |
H H <-----------------------------------------------+
#=========#
References
----------