Awaiting for Godot: stateless model checking that avoids executions where nothing happens.
Saved in:
| Title: | Awaiting for Godot: stateless model checking that avoids executions where nothing happens. |
|---|---|
| Authors: | Jonsson, Bengt1 (AUTHOR) bengt@it.uu.se, Lång, Magnus1 (AUTHOR) magnus.lang@it.uu.se, Sagonas, Konstantinos1,2 (AUTHOR) kostis@it.uu.se |
| Source: | Formal Methods in System Design. Oct2025, Vol. 67 Issue 1, p71-105. 35p. |
| Subjects: | Software verification, Parallel programs (Computer programs), Synchronization, Computer software execution |
| Abstract: | Stateless Model Checking (SMC) is a verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It is highly effective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and allows SMC to explore only one execution per equivalence class. Even with DPOR, SMC often spends unnecessary effort in exploring loop iterations that are pure, i.e., have no effect on the program state. In this article, we present techniques for making SMC with DPOR more effective on programs with pure loop iterations. The first technique is a static program analysis to detect loop purity and an associated program transformation, called Partial Loop Purity Elimination, that inserts assume statements to block pure loop iterations. Subsequently, some of these assume statements are turned into await statements that completely remove many assume-blocked executions. Finally, we present an extension of the standard DPOR equivalence, obtained by weakening the conflict relation between events. All these techniques are incorporated into a new DPOR algorithm, Optimal-DPOR-Await, which can handle both await statements and the weaker conflict relation, is optimal in the sense that it explores exactly one execution in each equivalence class, and can also diagnose livelocks. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs that are currently challenging for SMC tools, both for exploring their complete set of interleavings, but even for detecting concurrency errors in them. [ABSTRACT FROM AUTHOR] |
| Copyright of Formal Methods in System Design is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) | |
| Database: | Engineering Source |
| FullText | Text: Availability: 0 |
|---|---|
| Header | DbId: egs DbLabel: Engineering Source An: 188715904 AccessLevel: 6 PubType: Academic Journal PubTypeId: academicJournal PreciseRelevancyScore: 0 |
| IllustrationInfo | |
| Items | – Name: Title Label: Title Group: Ti Data: Awaiting for Godot: stateless model checking that avoids executions where nothing happens. – Name: Author Label: Authors Group: Au Data: <searchLink fieldCode="AR" term="%22Jonsson%2C+Bengt%22">Jonsson, Bengt</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> bengt@it.uu.se</i><br /><searchLink fieldCode="AR" term="%22Lång%2C+Magnus%22">Lång, Magnus</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> magnus.lang@it.uu.se</i><br /><searchLink fieldCode="AR" term="%22Sagonas%2C+Konstantinos%22">Sagonas, Konstantinos</searchLink><relatesTo>1,2</relatesTo> (AUTHOR)<i> kostis@it.uu.se</i> – Name: TitleSource Label: Source Group: Src Data: <searchLink fieldCode="JN" term="%22Formal+Methods+in+System+Design%22">Formal Methods in System Design</searchLink>. Oct2025, Vol. 67 Issue 1, p71-105. 35p. – Name: Subject Label: Subjects Group: Su Data: <searchLink fieldCode="DE" term="%22Software+verification%22">Software verification</searchLink><br /><searchLink fieldCode="DE" term="%22Parallel+programs+%28Computer+programs%29%22">Parallel programs (Computer programs)</searchLink><br /><searchLink fieldCode="DE" term="%22Synchronization%22">Synchronization</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+software+execution%22">Computer software execution</searchLink> – Name: Abstract Label: Abstract Group: Ab Data: Stateless Model Checking (SMC) is a verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It is highly effective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and allows SMC to explore only one execution per equivalence class. Even with DPOR, SMC often spends unnecessary effort in exploring loop iterations that are pure, i.e., have no effect on the program state. In this article, we present techniques for making SMC with DPOR more effective on programs with pure loop iterations. The first technique is a static program analysis to detect loop purity and an associated program transformation, called Partial Loop Purity Elimination, that inserts assume statements to block pure loop iterations. Subsequently, some of these assume statements are turned into await statements that completely remove many assume-blocked executions. Finally, we present an extension of the standard DPOR equivalence, obtained by weakening the conflict relation between events. All these techniques are incorporated into a new DPOR algorithm, Optimal-DPOR-Await, which can handle both await statements and the weaker conflict relation, is optimal in the sense that it explores exactly one execution in each equivalence class, and can also diagnose livelocks. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs that are currently challenging for SMC tools, both for exploring their complete set of interleavings, but even for detecting concurrency errors in them. [ABSTRACT FROM AUTHOR] – Name: AbstractSuppliedCopyright Label: Group: Ab Data: <i>Copyright of Formal Methods in System Design is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract.</i> (Copyright applies to all Abstracts.) |
| PLink | https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=188715904 |
| RecordInfo | BibRecord: BibEntity: Identifiers: – Type: doi Value: 10.1007/s10703-025-00479-0 Languages: – Code: eng Text: English PhysicalDescription: Pagination: PageCount: 35 StartPage: 71 Subjects: – SubjectFull: Software verification Type: general – SubjectFull: Parallel programs (Computer programs) Type: general – SubjectFull: Synchronization Type: general – SubjectFull: Computer software execution Type: general Titles: – TitleFull: Awaiting for Godot: stateless model checking that avoids executions where nothing happens. Type: main BibRelationships: HasContributorRelationships: – PersonEntity: Name: NameFull: Jonsson, Bengt – PersonEntity: Name: NameFull: Lång, Magnus – PersonEntity: Name: NameFull: Sagonas, Konstantinos IsPartOfRelationships: – BibEntity: Dates: – D: 01 M: 10 Text: Oct2025 Type: published Y: 2025 Identifiers: – Type: issn-print Value: 09259856 Numbering: – Type: volume Value: 67 – Type: issue Value: 1 Titles: – TitleFull: Formal Methods in System Design Type: main |
| ResultId | 1 |
