Documentation/trace/rv/monitor_wwnr.rst

   1 Monitor wwnr
   2 ============
   3
   4 - Name: wwrn - wakeup while not running
   5 - Type: per-task deterministic automaton
   6 - Author: Daniel Bristot de Oliveira <bristot@kernel.org>
   7
   8 Description
   9 -----------
  10
  11 This is a per-task sample monitor, with the following
  12 definition::
  13
  14                |
  15                |
  16                v
  17     wakeup   +-------------+
  18   +--------- |             |
  19   |          | not_running |
  20   +--------> |             | <+
  21              +-------------+  |
  22                |              |
  23                | switch_in    | switch_out
  24                v              |
  25              +-------------+  |
  26              |   running   | -+
  27              +-------------+
  28
  29 This model is borken, the reason is that a task can be running
  30 in the processor without being set as RUNNABLE. Think about a
  31 task about to sleep::
  32
  33   1:      set_current_state(TASK_UNINTERRUPTIBLE);
  34   2:      schedule();
  35
  36 And then imagine an IRQ happening in between the lines one and two,
  37 waking the task up. BOOM, the wakeup will happen while the task is
  38 running.
  39
  40 - Why do we need this model, so?
  41 - To test the reactors.
  42
  43 Specification
  44 -------------
  45 Grapviz Dot file in tools/verification/models/wwnr.dot