Optimal Reads-From Consistency Checking for C11-Style Memory Models
summary
Characterizes reads-from consistency for C11 variants and gives concrete algorithms and hardness results: introduces a minimal coherence witness to avoid building full modification orders and achieves an O(n·K) algorithm for RC20/RA (n events, K threads), a truly linear algorithm for the fully relaxed fragment, and NP-hardness for SRA variants. Implements methods in TruSt/TMC and C11Tester and reports substantial speedups and more executions explored on standard benchmarks, with proofs and fine-grained optimality bounds.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:24Problem definition
- 2:45C11 memory model
- 5:15Formalizing reads-from
- 5:56RC20 model results
- 6:37Minimal coherence witness
- 8:44Experimental evaluation
- 10:50Results for C11 variants
- 11:33Conclusion
- 11:55Q&A
related talks
22mOptimal Stateless Model Checking under the Release-Acquire Semantics
23mVerifying Observational Robustness Against a C11-style Memory Model
01h 11mProgramming language memory models: Problems, solutions, and directions
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
28mCAAT: Consistency as a Theory
14mMaking Weak Memory Models Fair
19mVerifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
17mDynamic Robustness Verification against Weak Memory