blob: 80f1777b85aacbbed31b8ccbe11c768c2b40b41c [file] [log] [blame]
Monitor wwnr
============
- Name: wwrn - wakeup while not running
- Type: per-task deterministic automaton
- Author: Daniel Bristot de Oliveira <bristot@kernel.org>
Description
-----------
This is a per-task sample monitor, with the following
definition::
|
|
v
wakeup +-------------+
+--------- | |
| | not_running |
+--------> | | <+
+-------------+ |
| |
| switch_in | switch_out
v |
+-------------+ |
| running | -+
+-------------+
This model is borken, the reason is that a task can be running
in the processor without being set as RUNNABLE. Think about a
task about to sleep::
1: set_current_state(TASK_UNINTERRUPTIBLE);
2: schedule();
And then imagine an IRQ happening in between the lines one and two,
waking the task up. BOOM, the wakeup will happen while the task is
running.
- Why do we need this model, so?
- To test the reactors.
Specification
-------------
Grapviz Dot file in tools/verification/models/wwnr.dot