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.
Original language | English |
---|---|
Title of host publication | Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings |
Editors | Étienne André, Jun Sun |
Number of pages | 23 |
Publisher | Springer |
Publication date | 2023 |
Pages | 176-198 |
ISBN (Print) | 9783031453311 |
DOIs | |
Publication status | Published - 2023 |
Event | 21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023 - Singapore, Singapore Duration: 24 Oct 2023 → 27 Oct 2023 |
Conference
Conference | 21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023 |
---|---|
Country/Territory | Singapore |
City | Singapore |
Period | 24/10/2023 → 27/10/2023 |
Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 14216 LNCS |
ISSN | 0302-9743 |
Bibliographical note
Publisher Copyright:© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.