| 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 |
