| 123456789101112131415161718192021222324252627282930313233343536373839404142434445 |
- 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 broken, 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
|
