Liveness to Safety for Distributed Systems
summary
Claims a mechanical reduction of liveness to safety by encoding justice (weak fairness) as finite planners — finite sequences of fairness conditions — and replacing liveness proof rules with a non-interfering monitor that waits for the planner to be exhausted. Method handles probabilistic liveness (probability one) and is demonstrated on three protocols: a spanning tree builder, per-tree leader choice, and a randomized maximal independent set. Example specifics: a dumb-token semaphore uses a “schedule everybody three times” planner; probabilistic planners use patterns like n lows then one high. The constructions are implementable and mechanizable.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:09Liveness vs safety in distributed systems
- 2:38Verification challenges
- 3:45Reducing liveness to safety
- 5:55Planners for liveness
- 9:04Mutual exclusion example
- 12:13Spanning tree example
- 16:13Maximal independent set example
- 20:59Termination proof for MIS
- 23:52Synchronous vs asynchronous
- 24:57Bounded safety replacing liveness
- 25:40Conclusion
related talks
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
17mLiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
30mCan Private Proof-of-Stake Blockchains Obtain All of Safety, Liveness, and Privacy?
20mPerformal: Formal Verification of Latency Properties for Distributed Systems
56mHerding LLMs: Predictable Outcomes from Unpredictable Agents
28mReasoning about Distributed Reconfigurable Systems
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
24mFormal Verification of a Distributed Dynamic Reconfiguration Protocol