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