Soundness of Predictive Concurrency Analyses
summary
Presents a unified, graph‑based definition of soundness for predictive concurrency analyses, lifts trace state‑similarity to execution‑graph similarity with symbolic values, and provides a three‑step proof recipe (construct program‑order graph, insert memory edges, concretize symbolic values). Uses that recipe to prove six existing predictors sound, including the first soundness proof for a predictor on weak memory (TSO/MCRTSO); proofs require multicopy‑atomic models and do not yet cover non‑MCA models like ARMv7/Power.
AI-written summary · about
chapters (11)
- 0:00Predictive concurrency analysis intro
- 1:45Weak memory soundness challenges
- 3:09Traces to execution graphs
- 5:16Predictive soundness definition
- 7:04State similarity and predictions
- 8:09Proof recipe for correctness
- 9:35Six analyses proven correct
- 10:40Key insights and results
- 11:44Limitations with non-multicopy-atomic
- 12:50GPU memory models future work
- 13:31Q&A on execution graphs
related talks
14mMaking Weak Memory Models Fair
01h 01mThe Future of Concurrency and Parallelism
28mCAAT: Consistency as a Theory
23mA Reachability Logic for a Weak Memory Model with Promises
19mSound Deadlock Prediction
18mThe Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++
30mMonadic interpreters for concurrent memory models: Executable semantics of a concurrent(…)
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification