0001 Monitor wwnr
0002 ============
0003
0004 - Name: wwrn - wakeup while not running
0005 - Type: per-task deterministic automaton
0006 - Author: Daniel Bristot de Oliveira <bristot@kernel.org>
0007
0008 Description
0009 -----------
0010
0011 This is a per-task sample monitor, with the following
0012 definition::
0013
0014 |
0015 |
0016 v
0017 wakeup +-------------+
0018 +--------- | |
0019 | | not_running |
0020 +--------> | | <+
0021 +-------------+ |
0022 | |
0023 | switch_in | switch_out
0024 v |
0025 +-------------+ |
0026 | running | -+
0027 +-------------+
0028
0029 This model is borken, the reason is that a task can be running
0030 in the processor without being set as RUNNABLE. Think about a
0031 task about to sleep::
0032
0033 1: set_current_state(TASK_UNINTERRUPTIBLE);
0034 2: schedule();
0035
0036 And then imagine an IRQ happening in between the lines one and two,
0037 waking the task up. BOOM, the wakeup will happen while the task is
0038 running.
0039
0040 - Why do we need this model, so?
0041 - To test the reactors.
0042
0043 Specification
0044 -------------
0045 Grapviz Dot file in tools/verification/models/wwnr.dot
