A Fully Verified Persistency Library
summary
Claims a sound, machine-checked correctness path showing that the FliT durability transformation refines an abstract PLib abstract persistency library specification and therefore preserves durable linearizability. Proof structure uses a forward simulation coupled with a prophecy variable as an oracle, then a refinement proof of FliT against PLib under the realistic PTSO memory model. The refinement and intermediate models are fully mechanised in KIV, producing a verified guarantee that FliT’s transformations to durability are sound.
AI-written summary · about
chapters (12)
- 0:00Verified persistency library intro
- 1:06What is persistency & NVM
- 3:11Durable invariants & PWB/PFENCE
- 5:40Linearizability & durable linearizability
- 8:07Legacy to durable algorithms
- 9:08FLIT library overview
- 11:14FLIT linearizability theorem
- 13:21Proof strategy & refinement
- 16:30PB library specification
- 17:15Final FLIT refinement on x86
- 18:18Summary & future work
- 18:38Q&A
related talks
25mThe Path to Durable Linearizability
12mCompositionality and Observational Refinement for Linearizability with Crashes
23mPersistence Semantics for Weak Memory
15mLilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
27mC4: verified transactional objects
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
17mRELINCHE: Automatically Checking Linearizability under Relaxed Memory Consistency
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz