Monitor wwnr

• Name: wwrn - wakeup while not running

• Type: per-task deterministic automaton

• Author: Daniel Bristot de Oliveira <bristot@kernel.org>

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