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