wip 監視器¶

名稱: wip - 搶佔式喚醒
型別: 每 CPU 確定性自動機
作者: Daniel Bristot de Oliveira <bristot@kernel.org>

描述¶

搶佔式喚醒 (wip) 監視器是一個示例性的每 CPU 監視器，用於驗證喚醒事件是否總是在搶佔停用時發生。

                   |
                   |
                   v
                 #==================#
                 H    preemptive    H <+
                 #==================#  |
                   |                   |
                   | preempt_disable   | preempt_enable
                   v                   |
  sched_waking   +------------------+  |
+--------------- |                  |  |
|                |  non_preemptive  |  |
+--------------> |                  | -+
                 +------------------+

由於排程器同步，喚醒事件總是在搶佔停用時發生。然而，由於 preempt_count 及其跟蹤事件在中斷方面不是原子的，可能會出現一些不一致。例如

preempt_disable() {
      __preempt_count_add(1)
      ------->        smp_apic_timer_interrupt() {
                              preempt_disable()
                                      do not trace (preempt count >= 1)

                              wake up a thread

                              preempt_enable()
                                       do not trace (preempt count >= 1)
                      }
      <------
      trace_preempt_disable();
}

此問題已在此處報告和討論: https://lore.kernel.org/r/cover.1559051152.git.bristot@redhat.com/

規範¶

Grapviz Dot 檔案位於 tools/verification/models/wip.dot