Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs

TL;DR

This paper introduces Event-DPOR, a tailored DPOR algorithm for event-driven multi-threaded programs that improves verification efficiency by avoiding unnecessary execution explorations, demonstrating exponential speedups over existing methods.

Contribution

It extends the optimal DPOR algorithm to event-driven programs, proves its correctness and optimality, and addresses NP-hard redundancy checks with efficient approximations.

Findings

Event-DPOR is exponentially faster than existing tools on various programs.

It completely avoids unnecessary execution explorations.

The redundancy check in Event-DPOR is NP-hard, but approximated efficiently.

Abstract

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.