監控 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