Proving linearizability of fault-tolerant register protocols: dependency graph approach
summary
Framework claims a concrete, automatable criterion: build a per-execution dependency graph as the union of four relations (real-time, write-write total order, reads-from and from-read relations) and prove the graph is acyclic. Using timestamps as witnesses, the method yields surprisingly simple proofs of multi-writer multi-reader ABD linearizability (including infinite executions and incomplete operations via a visibility predicate), avoiding linearization-point or forward-simulation machinery via an acyclicity criterion.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 3:30New methodology for proofs
- 9:59Dependency graph approach
- 13:14Dependency graph relations
- 24:00Proving ABD linearizability
- 32:36Conclusions
related talks
14mAutomatically Verifying Replication-aware Linearizability
21mA Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
15mMuch ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D
28mReasoning about Distributed Reconfigurable Systems
22mHow to Enforce and Verify Invariants in Weakly Consistent Databases
25mProperty-agnostic base case extension for scalable verification of distributed systems
36mThe FIDS Theorems: Tensions between Multinode and Multicore Performance in Transactional Systems
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...