Context: Model checking has become a key tool for gaining confidence in correctness of multi-threaded programs. Unit tests and functional tests do not suffice because of race conditions that are not discovered by those tests. This problem is addressed by model checking tools. A simple model checker is useful for detecting race conditions prior to production. Inquiry: Current model checkers hardwire the behavior of common thread operations, and do not recognize application-dependent thread paradigms or functions using simpler primitive operations. This introduces additional operations, causing current model checkers to be excessively slow. In addition, there is no mechanism to model the semantics of the actual thread wakeup policies implemented in the underlying thread library or operating system. Eliminating these constraints can make model checkers faster. Approach: McMini is an **extensible** model checker based on DPOR (Dynamic Partial Order Reduction). A mechanism was invented to declare to McMini new, primitive thread operations, typically in 100~lines or less of C~code. The mechanism was extended to also allow a user of McMini to declare alternative thread wakeup policies, including spurious wakeups from condition variables. Knowledge: In McMini, the user defines new thread operations. The user optimizes these operations by declaring to the DPOR algorithm information that reduces the number of thread schedules to be searched. One declares: (i) under what conditions an operation is enabled; (ii) which thread operations are independent of each other; and (iii) when two operations can be considered as co-enabled. An optional wakeup policy is implemented by defining when a wait operation (on a semaphore, condition variable, etc.) is enabled. A new enqueue thread operation is described, allowing a user to declare alternative wakeup policies. Grounding: McMini was first confirmed to operate correctly and efficiently as a traditional, but extensible model checker for mutex, semaphore, condition variable, and reader-writer lock. McMini's extensibility was then tested on novel primitive operations, representing other useful paradigms for multithreaded operations. An example is readers-and-two-writers. The speed of model checking was found to be five times faster and more, as compared to traditional implementations on top of condition variables. Alternative wakeup policies (e.g., FIFO, LIFO, arbitrary, etc.) were then tested using an enqueue operation. Finally, spurious wakeups were tested with a program that exposes a bug **only** in the presence of a spurious wakeup. Importance: Many applications employ functions for multithreaded paradigms that go beyond the traditional mutex, semaphore, and condition variables. They are defined on top of basic operations. The ability to directly define new primitives for these paradigms makes model checkers run faster by searching fewer thread schedules. The ability to model particular thread wakeup policies, including spurious wakeup for condition variables, is also important. Note that POSIX leaves undefined the wakeup policies of `pthread_mutex_lock`, `sem_wait`, and `pthread_cond_wait`. The POSIX thread implementation then chooses a particular policy (e.g., FIFO, arbitrary), which can be directly modeled by McMini.

翻译：上下文：模型检测已成为确保多线程程序正确性的关键工具。由于单元测试和功能测试无法发现竞态条件，因此需要模型检测工具来解决这一问题。简单的模型检测器有助于在生产环境前检测竞态条件。问题：当前的模型检测器硬编码了常见线程操作的行为，无法识别应用程序相关的线程范式或使用更简单原语操作的函数。这引入了额外操作，导致现有模型检测器运行速度过慢。此外，缺乏对底层线程库或操作系统中实际线程唤醒策略语义的建模机制。消除这些限制可使模型检测器运行更快。方法：McMini是一种基于DPOR（动态部分序归约）的可扩展模型检测器。我们发明了一种机制，允许用户向McMini声明新的原始线程操作（通常以100行或更少的C代码实现）。该机制进一步扩展，允许McMini用户声明替代线程唤醒策略（包括条件变量的虚假唤醒）。知识：在McMini中，用户可定义新的线程操作，并通过向DPOR算法声明减少待搜索线程调度数量的信息来优化这些操作。用户需声明：（i）操作启用条件；（ii）线程操作间的独立性；（iii）两个操作何时可视为协同启用。可选唤醒策略通过定义等待操作（如信号量、条件变量等）的启用条件来实现。本文还描述了一种新的入队线程操作，用于声明替代唤醒策略。基础验证：McMini首先被验证可作为支持互斥锁、信号量、条件变量和读写锁的传统可扩展模型检测器正确高效运行。随后，针对代表多线程操作其他有用范式的新型原始操作（如"读者与双写者"示例）测试了其可扩展性。相较于基于条件变量的传统实现，模型检测速度提升五倍以上。接着通过入队操作测试了替代唤醒策略（如FIFO、LIFO、任意顺序等）。最后，使用仅在存在虚假唤醒时暴露bug的程序测试了虚假唤醒场景。重要性：许多应用程序使用的多线程范式函数已超越传统互斥锁、信号量和条件变量范畴，这些函数基于基本操作定义。直接定义这些范式的新原语能力可通过搜索更少的线程调度来加速模型检测器。精确建模特定线程唤醒策略（包括条件变量的虚假唤醒）同样重要。值得注意的是，POSIX标准未定义`pthread_mutex_lock`、`sem_wait`和`pthread_cond_wait`的唤醒策略，而是由具体POSIX线程实现选择特定策略（如FIFO、任意顺序），McMini可直接对此类策略进行建模。