Message Chains for Distributed System Verification
summary
Defines message chains as a listlike datatype that records send history so proofs avoid reasoning about individual messages or buffers, and implements an automated instrumentation called the up verifier for P-style event handlers. Prototype verifies 16 literature benchmarks plus one new and two industrial systems, runs comparably to prior tools, and uses specification mining with Trio to synthesize recursive message-chain invariants from executions. Works for safety properties only (no liveness guarantee).
AI-written summary · about
chapters (10)
- 0:00Distributed system verification
- 1:47Verifying asynchronous systems
- 3:09Chang-Roberts algorithm example
- 6:18Message passing verification approaches
- 7:21Message chains for verification
- 9:28Verifying Chang-Roberts with chains
- 11:14Automating invariant discovery
- 12:41UP Verifier performance
- 14:28Two-phase commit case study
- 15:34Q&A
related talks
16mCyclic Message Histories for Automated Safety Verification of Distributed Algorithms
25mProperty-agnostic base case extension for scalable verification of distributed systems
48mThe Verification of a Distributed System
38mThe Verification of a Distributed System
27mWar and Peace: The Multi-Chain Reality
45mCorrectness proofs of distributed systems with Isabelle
20mModel Checking Distributed Protocols in Must
13mSharding the State Machine: Automated Modular Reasoning for Complex Concurrent System