Monitor wwnr ============ - Name: wwrn - wakeup while not running - Type: per-task deterministic automaton - Author: Daniel Bristot de Oliveira 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