Event-driven multi-threaded programming is an important idiom for structuring concurrent computations. Stateless Model Checking (SMC) is an effective verification technique for multi-threaded programs, especially when coupled with Dynamic Partial Order Reduction (DPOR). Existing SMC techniques are often ineffective in handling event-driven programs, since they will typically explore all possible orderings of event processing, even when events do not conflict. We present Event-DPOR , a DPOR algorithm tailored to event-driven multi-threaded programs. It is based on Optimal-DPOR, an optimal DPOR algorithm for multi-threaded programs; we show how it can be extended for event-driven programs. We prove correctness of Event-DPOR for all programs, and optimality for a large subclass. One complication is that an operation in Event-DPOR, which checks for redundancy of new executions, is NP-hard, as we show in this paper; we address this by a sequence of inexpensive (but incomplete) tests which check for redundancy efficiently. Our implementation and experimental evaluation show that, in comparison with other tools in which handler threads are simulated using locks, Event-DPOR can be exponentially faster than other state-of-the-art DPOR algorithms on a variety of programs and manages to completely avoid unnecessary exploration of executions.

翻译：事件驱动多线程编程是结构化并发计算的重要范式。无状态模型检测（SMC）是一种有效的多线程程序验证技术，尤其当结合动态偏序归约（DPOR）时效果显著。现有SMC技术在处理事件驱动程序时往往效率低下，因为它们通常会探索事件处理的所有可能顺序，即使事件之间不存在冲突。我们提出Event-DPOR，一种专门针对事件驱动多线程程序设计的DPOR算法。该算法基于Optimal-DPOR（一种针对多线程程序的最优DPOR算法），并展示了如何将其扩展以适用于事件驱动程序。我们证明了Event-DPOR对所有程序的正确定义，并对一大类子程序证明了其最优性。一个复杂性在于：Event-DPOR中用于检查新执行冗余性的操作是NP难问题（本文予以证明）；我们通过一系列低成本（但不完备）的高效冗余检查测试来应对这一问题。我们的实现与实验评估表明，相较于其他使用锁模拟处理程序线程的工具，Event-DPOR在多种程序上比现有最先进DPOR算法快指数级，并能完全避免不必要执行的探索。