PerpLE: Improving the Speed and Effectiveness of Memory Consistency Testing
Themis Melissaris, Markos Markakis, Kelly A. Shaw, Margaret Martonosi
Abstract
Even as most of today's computer systems have turned to parallelism to improve performance, their documentation often remains informal, incomplete or even incorrect regarding their memory consistency models. This leads to programmer and designer confusion and to buggy concurrent systems. Existing tools for empirical memory consistency testing rely on large numbers of iterations of simple multi-threaded litmus tests to perform conformance testing. The current approach typically employs thread synchronization at every iteration, which imposes a significant overhead and can reduce testing performance and efficiency.
This paper proposes new litmus test variants called perpetual litmus tests, which allow for consistency testing without periteration synchronization. Perpetual litmus tests use arithmetic sequences in store operations to reduce the required synchronization points. We present PerpLE, a software suite that includes tools for the generation, execution, and analysis of perpetual litmus tests. We introduce an algorithm for determining the outcomes of perpetual litmus tests as well as a scalable linear heuristic algorithm. Evaluating the performance, scalability and ability of our tool to find outcomes of interest on an x86 system, we observe a wider variety of outcomes than litmus7 while experiencing runtime speedups over all litmus7 synchronization modes (8.89x over the default user mode). Compared to the default litmus7 synchronization (user) mode, PerpLE offers over four orders-of-magnitude improvement in the rate with which we detect target outcomes.
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 6b5b43ae-9330-443e-9424-520dc22c8b90Cited by top-tier papers2
- Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model ImplementationsYao Hsiao, Dominic P. Mulligan, Nikos Nikoleris, Gustavo Petri et al.MICRO 2021 · 20 citations
- From Logs to Causal Inference: Diagnosing Large SystemsMarkos Markakis, Brit Youngmann, Trinity Gao, Ziyu Zhang et al.VLDB 2025 · 6 citations
Related papers
- Foundations of empirical memory consistency testingJake Kirkham, Tyler Sorensen, Esin Tureci, Margaret MartonosiOOPSLA 2020 · 7 citations
- Rely-Guarantee Reasoning for Causally Consistent Shared MemoryOri Lahav, Brijesh Dongol, Heike WehrheimCAV 2023 · 11 citations
- Improving the Concurrency Performance of Persistent Memory Transactions on MulticoresQing Wang, Youyou Lu, Zhongjie Wu, Fan Yang et al.DAC 2020 · 3 citations
- Checking robustness to weak persistency modelsHamed Gorjiara, Weiyu Luo, Alex Lee, Guoqing Harry Xu et al.PLDI 2022 · 13 citations
- Efficiently detecting concurrency bugs in persistent memory programsZhangyu Chen, Yu Hua, Yongle Zhang, Luochangqi DingASPLOS 2022 · 11 citations
