Anvil: Verifying Liveness of Cluster Management Controllers
Talkat 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) · 2024-07-10..07-12·
summary
Anvil presents eventually stable reconciliation as a concise temporal liveness spec and provides a Rust framework that verifies controllers against it using the virus verifier. The project builds and verifies three Kubernetes controllers (ZooKeeper, RabbitMQ, FluentBit) that are deployable and match feature set and runtime performance of unverified references. Proof-to-code ratios run ~4.5–7.4, verification uncovers four deep bugs (two present in references), and proofs rely on weak-fairness and eventual-crash-stability assumptions.
AI-written summary · about
chapters (11)
- 0:00Introduction to controllers
- 1:28Limitations of testing
- 2:33Anvil approach overview
- 3:33Verification workflow
- 4:16Defining ESR spec
- 7:13ESR benefits and challenges
- 8:53Anvil's proof features
- 10:35Environment modeling
- 13:50Proof strategy
- 15:10Evaluation results
- 16:37Conclusion
related talks
23mKivi: Verification for Cluster Management
38mThe Verification of a Distributed System
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
48mThe Verification of a Distributed System
19mBridging the Verifiability Gap: Why We Need More From Our Specs and How We Get It
22mHow to Enforce and Verify Invariants in Weakly Consistent Databases
14mBolt-On Strong Consistency: Specification, Implementation, and Verification
16mUnconference Session: Reliable K8s Operator: How to Survive Eventual Consistency