tjh.dev
Linux kernel mirror (for testing)
git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
kernel
os
linux
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 borken, 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