1 Monitor 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 8 Description 9 ----------- 10 11 This is a per-task sample monitor, with the following 12 definition:: 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 29 This model is broken, the reason is that a task can be running 30 in the processor without being set as RUNNABLE. Think about a 31 task about to sleep:: 32 33 1: set_current_state(TASK_UNINTERRUPTIBLE); 34 2: schedule(); 35 36 And then imagine an IRQ happening in between the lines one and two, 37 waking the task up. BOOM, the wakeup will happen while the task is 38 running. 39 40 - Why do we need this model, so? 41 - To test the reactors. 42 43 Specification 44 ------------- 45 Grapviz Dot file in tools/verification/models/wwnr.dot
Linux® is a registered trademark of Linus Torvalds in the United States and other countries.
TOMOYO® is a registered trademark of NTT DATA CORPORATION.