46 lines · plain
1Monitor wwnr2============3 4- Name: wwrn - wakeup while not running5- Type: per-task deterministic automaton6- Author: Daniel Bristot de Oliveira <bristot@kernel.org>7 8Description9-----------10 11This is a per-task sample monitor, with the following12definition::13 14 |15 |16 v17 wakeup +-------------+18 +--------- | |19 | | not_running |20 +--------> | | <+21 +-------------+ |22 | |23 | switch_in | switch_out24 v |25 +-------------+ |26 | running | -+27 +-------------+28 29This model is broken, the reason is that a task can be running30in the processor without being set as RUNNABLE. Think about a31task 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 is38running.39 40- Why do we need this model, so?41- To test the reactors.42 43Specification44-------------45Grapviz Dot file in tools/verification/models/wwnr.dot46