Monitor wwnr

• Name: wwrn - wakeup while not running
• Type: per-task deterministic automaton
• Author: Daniel Bristot de Oliveira [email protected]

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