Unblocking Dynamic Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
2023Year
7Citations
4Top-tier citations
Abstract
Abstract Existing dynamic partial order reduction (DPOR) algorithms scale poorly on concurrent data structure benchmarks because they visit a huge number of blocked executions due to spinloops. In response, we develop Awamoche, a sound, complete, and strongly optimal DPOR algorithm that avoids exploring any useless blocked executions in programs with await and confirmation-CAS loops. Consequently, it outperforms the state-of-the-art, often by an exponential factor.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext 44a852cc-5acf-4dc8-ae44-e39c855fc5a8Cited by top-tier papers4
- Model Checking Distributed Protocols in MustConstantin Enea, Dimitra Giannakopoulou, Michalis Kokologiannakis, Rupak MajumdarOOPSLA 2024 · 5 citations
- SPORE: Combining Symmetry and Partial Order ReductionMichalis Kokologiannakis, Iason Marmanis, Viktor VafeiadisPLDI 2024 · 4 citations
- RELINCHE: Automatically Checking Linearizability under Relaxed Memory ConsistencyPavel Golovin, Michalis Kokologiannakis, Viktor VafeiadisPOPL 2025 · 4 citations
- Model Checking C/C++ with Mixed-Size AccessesIason Marmanis, Michalis Kokologiannakis, Viktor VafeiadisPOPL 2025 · 2 citations
Builds on5
- Truly stateless, optimal dynamic partial order reductionMichalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor VafeiadisPOPL 2022 · 46 citations
- VSync: push-button verification and optimization for synchronization primitives on weak memory modelsJonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu et al.ASPLOS 2021 · 40 citations
- HMC: Model Checking for Hardware Memory ModelsMichalis Kokologiannakis, Viktor VafeiadisASPLOS 2020 · 29 citations
- Stateless Model Checking Under a Reads-Value-From EquivalencePratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis et al.CAV 2021 · 25 citations
- Making weak memory models fairOri Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev et al.OOPSLA 2021 · 21 citations
Related papers
- Prioritized Constraint-Aided Dynamic Partial-Order ReductionJie Su, Cong Tian, Zuchao Yang, Jiyu Yang et al.ASE 2022 · 3 citations
- Parsimonious Optimal Dynamic Partial Order ReductionParosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson et al.CAV 2024 · 4 citations
- Symbolic Partial-Order Execution for Testing Multi-Threaded ProgramsDaniel Schemmel, Julian Büning, César Rodríguez, David Laprell et al.CAV 2020 · 12 citations
- The anchor verifier for blocking and non-blocking concurrent softwareCormac Flanagan, Stephen N. FreundOOPSLA 2020 · 7 citations
- A tree clock data structure for causal orderings in concurrent executionsUmang Mathur, Andreas Pavlogiannis, Hünkar Can Tunç, Mahesh ViswanathanASPLOS 2022 · 10 citations
