监视器 wwnr

• 名称：wwrn - 唤醒时未运行

• 类型：每个任务的确定性自动机

• 作者：Daniel Bristot de Oliveira <bristot@kernel.org>

描述

这是一个每个任务的示例监视器，定义如下：

             |
             |
             v
  wakeup   +-------------+
+--------- |             |
|          | not_running |
+--------> |             | <+
           +-------------+  |
             |              |
             | switch_in    | switch_out
             v              |
           +-------------+  |
           |   running   | -+
           +-------------+

此模型已损坏，原因是任务可以在处理器中运行，而无需设置为 RUNNABLE。想想一个即将休眠的任务

1:      set_current_state(TASK_UNINTERRUPTIBLE);
2:      schedule();

然后想象一下，在第一行和第二行之间发生了一个 IRQ，唤醒了该任务。嘣，唤醒将在任务运行时发生。

• 那么，我们为什么需要这个模型呢？

• 为了测试反应器。

规范

tools/verification/models/wwnr.dot 中的 Grapviz Dot 文件