The Path to Durable Linearizability
summary
Proposes a concrete method that converts an existing linearizability proof into durable correctness by adding small, checkable Delta proof obligations that only force flushes when noncommuting operations could reorder persistently. Works without fixing a persistency or weak-memory model, reuses volatile linearization machinery (including helping and hindsight), separates recovery reasoning, and scales to advanced structures — demonstrated by a full proof for a link-free persistent set and a pathway theorem from linearizability to durable linearizability.
AI-written summary · about
chapters (8)
- 0:00Start
- 5:14Running Example: a Concurrent Set
- 7:14Linearizability via Linearization Points
- 9:25What can go wrong when using NVRAM
- 11:36Flushes to the rescue
- 14:32The gap between volatile and persisted memory
- 19:02The Pathway Theorem
- 19:53The full story
related talks
12mCompositionality and Observational Refinement for Linearizability with Crashes
21mA Fully Verified Persistency Library
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
10mEfficient Decrease-And-Conquer Linearizability Monitoring
24mA Concurrent Program Logic with a Future and History
20mDeadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O...
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
12mProving Highly-Concurrent Traversals Correct