Performal: Formal Verification of Latency Properties for Distributed Systems
summary
PerforMal gives a concrete method to prove worst case latency for real distributed code by modeling programs as state machines in Daphne, attaching ghost timestamps that are symbolic latency expressions, and proving invariant bounds by local transition rules. A second tier turns those symbolic expressions into numeric SLO estimates by composing measured component distributions. Applied to a distributed lock, ZooKeeper and a MultiPaxos SMR, it uncovers a real ZooKeeper bug and shows estimates that track observed latencies on AWS and geo clusters.
AI-written summary · about
chapters (10)
- 0:00Performal introduction
- 2:30Latency verification limits
- 4:16Decoupling code from environment
- 5:41Symbolic latency for bounds
- 7:06Timed state machine modeling
- 8:51Proving invariants with domino logic
- 9:56Token ring latency proof
- 12:24Symbolic to real-time bounds
- 14:12Performal summary
- 15:16Q&A
related talks
38mTechniques and Tools for a Coherent Discussion about Performance in Complex...
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
38mThe Verification of a Distributed System
43mWhat We Talk About When We Talk About Distributed Systems
48mThe Verification of a Distributed System
13mTesting LLM-Generated Distributed Protocol Code
27mUnderstanding Distributed Systems with Deterministic Simulation
28mLiveness to Safety for Distributed Systems