The Reads-From Equivalence for the TSO and PSO Memory Models
summary
Presents algorithms that decide reads-from (RF) consistency for TSO and PSO with explicit complexity: n^{k+1} bound for TSO and n^{k+1}·min(n^{k^2},2^{k·d}) for PSO, plus a constructive procedure using TSO-executable conditions and fence maps to build linearizations. Delivers an exploration-optimal SMC that visits one RF class once and runs polynomial time per class when k is fixed, implements everything in Nidhugg, and reports substantial experimental speedups over Shasha-Snir/Mazurkiewicz-based checking.
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:23Concurrent program example
- 1:07Formal methods for memory models
- 2:30TSO and PSO operations
- 3:14Execution consistency verification
- 4:26TSO consistency algorithm
- 6:16PSO consistency bounds
- 7:47Intuition behind PSO bounds
- 8:54Experiments for consistency
- 9:37Stateless Model Checking problem
- 10:18Trace equivalence in SMC
- 11:24Reads-from equivalence in SMC
- 12:06Experiments for Stateless Model Checking
- 13:52Summary
related talks
15mOptimal Reads-From Consistency Checking for C11-Style Memory Models
21mCSL and relaxed memory
20mTruly Stateless, Optimal Dynamic Partial Order Reduction
23mPersistence Semantics for Weak Memory
30mDeciding Reachability under Persistent x86-TSO
20mHow Hard is Weak-Memory Testing?
20mSPORE: Combining Symmetry and Partial Order Reduction
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification