1Monitor 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
8Description
9-----------
10
11The wakeup in preemptive (wip) monitor is a sample per-cpu monitor
12that verifies if the wakeup events always take place with
13preemption 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
30The wakeup event always takes place with preemption disabled because
31of the scheduler synchronization. However, because the preempt_count
32and its trace event are not atomic with regard to interrupts, some
33inconsistencies 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
50This problem was reported and discussed here:
51  https://lore.kernel.org/r/cover.1559051152.git.bristot@redhat.com/
52
53Specification
54-------------
55Grapviz Dot file in tools/verification/models/wip.dot
56