Making Weak Memory Models Fair
summary
Proposes a uniform memory fairness condition for declarative weak memory models (requires porf-acyclicity) and proves it is equivalent to natural operational fairness for SC, TSO, RA and StrongCOH. Shows the condition preserves local program transformations and the RC11→x86‑TSO compilation scheme, and enables the first mechanized termination proofs for practical locks (MCS and ticket) under weak models. Key results are formalized in Coq and validated against concrete counterexamples where thread fairness alone fails.
AI-written summary · about
chapters (6)
- 0:00Intro
- 1:44Spinlock terminates under interleaving semantics
- 3:28Realistic concurrency semantics are weaker than SC
- 6:38Declarative memory models avoid explicit interleaving
- 10:14The declarative memory fairness definition is uniform
- 11:31Proving program termination with graph-based reasoning
related talks
20mHow Hard is Weak-Memory Testing?
30mA Tale of Shared Memory Concurrency in Programming Languages
21mCSL and relaxed memory
01h 11mProgramming language memory models: Problems, solutions, and directions
15mSoundness of Predictive Concurrency Analyses
23mAn Operational Approach to Library Abstraction under Relaxed Memory Concurrency
23mA Reachability Logic for a Weak Memory Model with Promises
23mVerifying Observational Robustness Against a C11-style Memory Model