Unblocking Dynamic Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis
2023年份
7被引次数
4顶会引用
摘要
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.
问问这篇 Paper
智能体会读完全文。
Lune 把这篇 Paper 索引到了最后一个公式,引用它的顶会 Paper 也一样。你提问,回答直接引用原文。
引用它的顶会 Paper4
- Model Checking Distributed Protocols in MustConstantin Enea, Dimitra Giannakopoulou, Michalis Kokologiannakis, Rupak MajumdarOOPSLA 2024 · 被引用 5 次
- SPORE: Combining Symmetry and Partial Order ReductionMichalis Kokologiannakis, Iason Marmanis, Viktor VafeiadisPLDI 2024 · 被引用 4 次
- RELINCHE: Automatically Checking Linearizability under Relaxed Memory ConsistencyPavel Golovin, Michalis Kokologiannakis, Viktor VafeiadisPOPL 2025 · 被引用 4 次
- Model Checking C/C++ with Mixed-Size AccessesIason Marmanis, Michalis Kokologiannakis, Viktor VafeiadisPOPL 2025 · 被引用 2 次
它引用的顶会 Paper5
- Truly stateless, optimal dynamic partial order reductionMichalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor VafeiadisPOPL 2022 · 被引用 46 次
- VSync: push-button verification and optimization for synchronization primitives on weak memory modelsJonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu 等ASPLOS 2021 · 被引用 40 次
- HMC: Model Checking for Hardware Memory ModelsMichalis Kokologiannakis, Viktor VafeiadisASPLOS 2020 · 被引用 29 次
- Stateless Model Checking Under a Reads-Value-From EquivalencePratyush Agarwal, Krishnendu Chatterjee, Shreya Pathak, Andreas Pavlogiannis 等CAV 2021 · 被引用 25 次
- Making weak memory models fairOri Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev 等OOPSLA 2021 · 被引用 21 次
相关 Paper
- Prioritized Constraint-Aided Dynamic Partial-Order ReductionJie Su, Cong Tian, Zuchao Yang, Jiyu Yang 等ASE 2022 · 被引用 3 次
- Parsimonious Optimal Dynamic Partial Order ReductionParosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson 等CAV 2024 · 被引用 4 次
- Symbolic Partial-Order Execution for Testing Multi-Threaded ProgramsDaniel Schemmel, Julian Büning, César Rodríguez, David Laprell 等CAV 2020 · 被引用 12 次
- The anchor verifier for blocking and non-blocking concurrent softwareCormac Flanagan, Stephen N. FreundOOPSLA 2020 · 被引用 7 次
- A tree clock data structure for causal orderings in concurrent executionsUmang Mathur, Andreas Pavlogiannis, Hünkar Can Tunç, Mahesh ViswanathanASPLOS 2022 · 被引用 10 次
