GNU Linux-libre 6.1.91-gnu
[releases.git] / Documentation / trace / rv / monitor_wip.rst
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