A Compositional Theory of Linearizability
summary
Presents a concrete reformulation of linearizability derived from a base concurrent model via the Karoubi envelope, producing a compositional model by restricting to saturated strategies through a saturation operation. Proves algebraically that this abstract linearizability (1) equals Herlihy‑Wing linearizability when the spec is atomic, (2) yields a simpler proof of locality and equivalence with observational refinement, and (3) connects to a program logic that is sound and used to verify composed implementations on paper.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:19Herlihy-Wing Linearizability
- 2:59Key Contributions
- 3:45Typical Approach for Verifying Concurrent Objects
- 4:15Implementating a Shared Queue
- 6:42Our Methodology
- 7:52Game Semantics
- 9:29Vertical Composition
- 10:42Sequential Copycat
- 13:16Abstract Linearizability
- 16:40Interaction Refinement: Proof (Forward)
- 19:50Program Logic
- 20:39Conclusion
related talks
12mCompositionality and Observational Refinement for Linearizability with Crashes
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
19mScenario-based Proofs for Concurrent Objects
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
10mEfficient Decrease-And-Conquer Linearizability Monitoring
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
20mVisibility Reasoning for Concurrent Snapshot Algorithms
31mTermination in Concurrency, Revisited