DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
Talkat 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) · 2021-07-14..07-16·
summary
DistAI simulates protocols to collect states, enumerates strongest possible invariants up to a bounded formula size, and checks inductiveness with an SMT-based verifier, then applies minimum weakening monotically until the conjunction is inductive. It proves a completeness guarantee for ∃-free invariants, verifies 13 of 14 benchmark protocols (fails only on the existential-quantifier case Toxos), and runs up to two orders of magnitude faster than prior tools like i4 and IC3 in the authors’ evaluation.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:26Why learn invariants for distributed protocols?
- 0:56Example: mutual exclusion protocol
- 2:34Related work
- 3:39DistAI Workflow
- 5:21Subsampling
- 7:04Candidate invariant enumeration
- 9:20Monotonic refinement
- 11:36Convergence
- 12:13Evaluation
- 13:05Runtimes
- 13:45Conclusion
related talks
11mFinding Invariants of Distributed Systems: It's a Small (Enough) World After All
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
16mBasilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols
45mCorrectness proofs of distributed systems with Isabelle
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
48mThe Verification of a Distributed System
01h 30mImplementing, verifying and debugging distributed event-based systems
22mHow to Enforce and Verify Invariants in Weakly Consistent Databases