Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
Talkat 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) · 2024-07-10..07-12·
summary
Claim: Kondo auto-generates and proves the network-level lemmas that make host-level invariants inductive, so developers only prove the synchronous proof about host states. It synthesizes Regular Invariants from protocol step semantics, lifts a human proof to the asynchronous model, and targets general verifiers like Daphne (no decidable-logic restrictions). Evaluation shows concrete savings: Two‑phase commit invariant count drops 8→4 and proof LOCs fall up to ~60% (Echo server) and ~20% (2PC).
AI-written summary · about
chapters (10)
- 0:00Invariant taxonomies intro
- 4:56Finding invariants challenges
- 7:46Network complexity in proofs
- 8:28Recurring patterns insight
- 10:57Message invariants tiers
- 12:00Introducing Condo
- 13:27Condo user workflow
- 14:29Condo evaluation results
- 14:52Conclusion & future
- 15:34Q&A
related talks
11mFinding Invariants of Distributed Systems: It's a Small (Enough) World After All
14mDistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
16mBasilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols
45mCorrectness proofs of distributed systems with Isabelle
22mHow to Enforce and Verify Invariants in Weakly Consistent Databases
24mFrom Enhanced Coinduction towards Enhanced Induction
28mReasoning about Distributed Reconfigurable Systems
21mTowards composable proofs of cache coherence protocols