How Hard is Weak-Memory Testing?
summary
Paper proves that consistency testing for many weak-memory models is NP-complete even with bounded threads, memory locations, and values, ruling out fixed-parameter shortcuts by those parameters. It shows a computational separation: SC, x86-TSO, PSO and Relaxed admit polynomial-time bounded testing, while Release-Acquire variants, several causal models, and POWER are hard. Proof uses intricate reductions, specifically a reduction from Monotone 1-in-3 SAT built with complex gadget constructions.
AI-written summary · about
chapters (21)
- 0:00Weak memory testing intro
- 0:24Motivation for weak memory testing
- 1:07Store buffer example
- 3:14Memory models and weak consistency
- 5:19Execution graphs and axioms
- 6:22Testing problem in weak memory
- 7:26Litmus tests for validation
- 9:53Computational complexity of testing
- 11:16Hardness results for testing
- 13:00Generalizing hardness across models
- 14:06Tractable vs intractable models
- 14:27Q&A
- 14:48Challenges in NP-hard models
- 15:32Litmus test design implications
- 16:13Testing with concurrent writes
- 16:57Hardness proof gadgets
- 17:41Thread and location scales
- 18:23Read-from relations and complexity
- 19:27Multicopy atomicity and separation
- 19:48Bounding memory actions
- 20:09Conclusion
related talks
14mMaking Weak Memory Models Fair
28mCAAT: Consistency as a Theory
16mModel Checking for a Multi-Execution Memory Model
21mChasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Model...
23mHow Do We Know That Weak Memory Matters?
23mVerifying Observational Robustness Against a C11-style Memory Model
05mWelcome
17mDynamic Robustness Verification against Weak Memory