Automatically Verifying Replication-aware Linearizability
summary
Automated verification framework proves replication-aware linearizability for Mergeable Replicated Data Types by checking novel algebraic laws on the three-way merge and operations, going beyond commutativity/associativity/idempotence. It implements a bottom-up linearization induction that generates verification conditions as FAR lemmas, discharges them automatically, and produces extracted code. Applied to multiple MRDTs and state-based CRDTs (including a verified JSON MRDT), the tool found and fixed bugs in prior implementations; artifacts and proofs are available online.
AI-written summary · about
chapters (10)
- 0:00Replication-aware linearizability
- 1:02Mergeable replicated data types
- 3:09Defining replication-aware linearizability
- 4:14Bottom-up linearization
- 6:19Conflict resolution in MRDTs
- 7:02Feasible states and proof
- 8:05Induction scheme for verification
- 9:08Theorem and FAR implementation
- 9:50MRDT verification results
- 10:52Questions and answers session
related talks
41mProving linearizability of fault-tolerant register protocols: dependency graph approach
15mModular Verification of Op-Based CRDTs in Separation Logic
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
22mKatara: Synthesizing CRDTs with Verified Lifting
01h 30mImplementing, verifying and debugging distributed event-based systems
16mType-Checking CRDT Convergence
25mSafe Replication through Bounded Concurrency Verification
13mSharding the State Machine: Automated Modular Reasoning for Complex Concurrent System