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

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bønneland, Sarbojit Das*, Bengt Jonsson, Magnus Lång, Konstantinos Sagonas

*Corresponding author for this work

Research output: Contribution to book/anthology/report/conference proceedingArticle in proceedingResearchpeer-review

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 languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings
EditorsÉtienne André, Jun Sun
Number of pages23
PublisherSpringer
Publication date2023
Pages176-198
ISBN (Print)9783031453311
DOIs
Publication statusPublished - 2023
Event21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023 - Singapore, Singapore
Duration: 24 Oct 202327 Oct 2023

Conference

Conference21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023
Country/TerritorySingapore
CitySingapore
Period24/10/202327/10/2023
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14216 LNCS
ISSN0302-9743

Bibliographical note

Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Fingerprint

Dive into the research topics of 'Tailoring Stateless Model Checking for Event-Driven Multi-threaded Programs'. Together they form a unique fingerprint.

Cite this