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