Based on kernel version 6.11. Page generated on 2024-09-24 08:21 EST.
| 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 |
Monitor wip
===========
- Name: wip - wakeup in preemptive
- Type: per-cpu deterministic automaton
- Author: Daniel Bristot de Oliveira <bristot@kernel.org>
Description
-----------
The wakeup in preemptive (wip) monitor is a sample per-cpu monitor
that verifies if the wakeup events always take place with
preemption disabled::
|
|
v
#==================#
H preemptive H <+
#==================# |
| |
| preempt_disable | preempt_enable
v |
sched_waking +------------------+ |
+--------------- | | |
| | non_preemptive | |
+--------------> | | -+
+------------------+
The wakeup event always takes place with preemption disabled because
of the scheduler synchronization. However, because the preempt_count
and its trace event are not atomic with regard to interrupts, some
inconsistencies might happen. For example::
preempt_disable() {
__preempt_count_add(1)
-------> smp_apic_timer_interrupt() {
preempt_disable()
do not trace (preempt count >= 1)
wake up a thread
preempt_enable()
do not trace (preempt count >= 1)
}
<------
trace_preempt_disable();
}
This problem was reported and discussed here:
https://lore.kernel.org/r/cover.1559051152.git.bristot@redhat.com/
Specification
-------------
Grapviz Dot file in tools/verification/models/wip.dot
|