EPVerifier: Accelerating Update Storms Verification with Edge-Predicate
Talkat 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24) · 2024-04-16..04-18·
summary
EPVerifier replaces global equivalence-class models with an edge-predicate model (one BDD-like predicate per link), so only actually affected edges are updated and the model avoids EC oscillation. It partitions verification by switch-based partitioning after updates arrive, enabling parallel maintenance and checking. Implemented and tested on synthetic and backbone traces, it verifies storms of ~1M updates in ~10s, giving a consistent 2–10× speedup with comparable memory overhead.
AI-written summary · about
chapters (8)
- 0:00EPVerifier introduction
- 1:50Data plane verification challenges
- 4:44Equivalence models under update storms
- 7:14Edge-Predicate model
- 8:41Parallelization with switch partition
- 10:06EPVerifier design
- 11:55Evaluation and deployment
- 13:22Summary and future work
related talks
01h 01mNetwork Verification: Past, Present, and Future
18mAPKeep: Realtime Verification for Real Networks
23mVeriFlow: Verifying Network-Wide Invariants in Real Time
18mLiveness Verification of Stateful Network Functions
20mPlankton: Scalable network configuration verification through model checking
29mSynthesis of dependable and self-driving communication networks
21mModular Control Plane Verification via Temporal Invariants
16mKatra: Realtime Verification for Multilayer Networks