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