Compositionality and Observational Refinement for Linearizability with Crashes
summary
Defines a compositional model for full-system crashes and proves that a new criterion, crash-aware linearizability, supports both locality and observational refinement; shows strict and durable linearizability factor through this criterion via a lemma; gives a sound rely-guarantee program logic for verifying methods under crashes; splits verification per memory location and mechanically verifies a persistence library (a flush-counter design) plus a persistent snapshot implementation; composes client and library to prove durable linearizability for clients and demonstrates the approach handles non-atomic specs.
AI-written summary · about
chapters (7)
- 0:00Introduction
- 1:45Linearizability basics
- 3:32Persistence library example
- 7:47Compositional crash-linearizability
- 9:34Verification approach
- 11:20Correctness theorem
- 12:04Summary
related talks
24mA Compositional Theory of Linearizability
25mThe Path to Durable Linearizability
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
10mEfficient Decrease-And-Conquer Linearizability Monitoring
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
27mC4: verified transactional objects
20mVisibility Reasoning for Concurrent Snapshot Algorithms