Avenir: Managing Data Plane Diversity with Control Plane Synthesis
summary
Avenir automatically synthesizes control-plane operations to make diverse data planes behave uniformly, proving soundness and completeness and implementing the algorithm in OCaml and Z3. It uses counter-example guided inductive synthesis with template and query caches to avoid exhaustive search, handles dozens-table pipelines and features like tunneling, and a prototype retargets 40,000 IPv6 route installs to a Broadcom P4 model in 40,000 IPv6 routes in ~12 minutes (comparable to ONOS’s ~15 minutes).
AI-written summary · about
chapters (8)
- 0:00Start
- 1:23A New Driver for Every Target
- 2:38Managing Drivers is Tedious
- 4:47Avenir: Control Plane Synthesis
- 5:50Controller
- 9:16How Broad is Avenir?
- 10:27How Well Does Avenir Scale?
- 10:53How Efficient is Avenir In A Realistic Scenario? - End-to-end ONOS switch reboot load test
related talks
25mDataplane equivalence and its applications
17mPractical Intent-driven Routing Configuration Synthesis
29mSynthesis of dependable and self-driving communication networks
15mEnabling In-situ Programmability in Network Data Plane: From Architecture to Language
27mNetComplete: Practical Network-Wide Configuration Synthesis with Autocompletion
25mAccelerating Control Plane for Edge
15mREAL: Emulating Control Plane at Simulator’s Cost
23mAIN: A Blueprint for an All-IP Data Center Network