xref: /linux/Documentation/trace/rv/monitor_wwnr.rst (revision 08b7174fb8d126e607e385e34b9e1da4f3be274f) 
1Monitor 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
8Description
9-----------
10
11This is a per-task sample monitor, with the following
12definition::
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
29This model is broken, the reason is that a task can be running
30in the processor without being set as RUNNABLE. Think about a
31task about to sleep::
32
33  1:      set_current_state(TASK_UNINTERRUPTIBLE);
34  2:      schedule();
35
36And then imagine an IRQ happening in between the lines one and two,
37waking the task up. BOOM, the wakeup will happen while the task is
38running.
39
40- Why do we need this model, so?
41- To test the reactors.
42
43Specification
44-------------
45Grapviz Dot file in tools/verification/models/wwnr.dot
46