监控 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）发生在第一行和第二行之间，唤醒了任务。砰，唤醒将在任务运行时发生。

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

• 为了测试反应器。

规范

Grapviz Dot 文件位于 tools/verification/models/wwnr.dot