Synthesizing Runtime Programmable Switch Updates

on YouTube ↗15m

" summary

FlexPlan synthesizes step-by-step runtime P4 switch update plans using program synthesis and an SMT-based verifier, encoding intermediate states as version sketches and pruning search with a snapshot learner and introspection for early termination. It guarantees each transition meets a user spec and fits switch memory, finds a plan whenever one exists, and empirically reduces peak resource spikes versus all-at-once updates while scaling to large, real-world switch.p4 programs; code and evaluations are open source.

AI-written summary · about

" chapters (13)

1. 0:00Intro
2. 0:25Background: Runtime programmable devices
3. 1:27Background: multi-step runtime update
4. 2:59SOTA: graph analysis and P4 verification
5. 4:26FlexPlan: a formal synthesis approach
6. 5:08Specification language
7. 6:52Program update sketching
8. 10:01Optimization: Snapshot learning
9. 11:14Optimization: Loop termination
10. 12:36Implementation and setup
11. 13:00Expressive specs save resources
12. 13:41Optimizations improve scalability
13. 14:16Summary

" related talks

• 16mRuntime Programmable SwitchesJiarong Xing, Kuo-Feng Hsu, Matty Kadosh, Alan Lo, Yonatan Piasetzky, Arvind Krishnamurthy, Ang Chen · 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22)
• 14mModular Switch Programming Under Resource ConstraintsDavid Walker, Mina Tahmasbi Arashloo, Shir Landau Feibish, Mary Hogan, Jennifer Rexford · 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22)
• 15mEnabling In-situ Programmability in Network Data Plane: From Architecture to LanguageYong Feng, Bin Liu, Ying Wan, Zhikang Chen, Haoyu Song, Wenquan Xu, Jiahao Li, Zijian Zhang, Tong Yun · 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22)
• 12mFlightplan: Dataplane Disaggregation and Placement for P4 ProgramsBoon Thau Loo, Isaac Pedisich, John Sonchack, Nik Sultana, Hans Giesen, Zhaoyang Han, Nishanth Shyamkumar, Shivani Burad, André DeHon · NSDI ’21
• 16mSequence Abstractions for Flexible, Line-Rate Network MonitoringDavid Walker, Ryan Beckett, Ratul Mahajan, Xiaoqi Chen, Andrew Johnson · 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24)
• 20mContra: A Programmable System for Performance aware RoutingDavid Walker, Ryan Beckett, Kuo-Feng Hsu, Ang Chen, Jennifer Rexford, Praveen Tammana · NSDI 2020
• 15mSketchLib: Enabling Efficient Sketch-based Monitoring on Programmable SwitchesZaoxing Liu, Hun Namkung, Daehyeok Kim, Vyas Sekar, Peter Steenkiste · 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22)
• 17mMultitenant In-Network Acceleration with SwitchVMAlon Rashelbach, Mark Silberstein, Sajy Khashab · 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24)