A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie...
summary
Introduces a forward-only proof method called possibility tracking that is claimed to be universal, sound, and complete for proving linearizability, with a variant single possibility tracking complete for strong linearizability; it maintains the set P of all possible atomic states and proves the invariant P not empty. The paper machine-verifies proofs in TLAPS for three nontrivial cases: Herlihy‑Wing queue, Jayanti single-scanner snapshot, and Jayanti‑Tarjan union‑find (strong linearizability); artifacts are available and evaluated.
AI-written summary · about
chapters (7)
- 0:00Concurrency and linearizability proofs
- 1:06Machine-verified concurrent object proofs
- 4:56Limitations of forward simulation
- 5:18Possibility tracking proof technique
- 6:01How possibility tracking works
- 10:56Hurley-Hewing queue case study
- 16:54Conclusion and Q&A
related talks
41mProving linearizability of fault-tolerant register protocols: dependency graph approach
25mProperty-agnostic base case extension for scalable verification of distributed systems
31mParameterized Verification of Systems with Precise (0,1)-Counter Abstraction
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
14mAutomatically Verifying Replication-aware Linearizability
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
20mStratified Guarded First-Order Transition Systems
01h 03mTrustworthy Automated Reasoning