Monitor 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/[email protected]/

规范

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