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