Safe, Modular Packet Pipeline Programming

on YouTube ↗28m

" summary

Introduces Lucid 2.0, a language and type system that guarantees programs are pipeline-safe on pipelined switches (P4/Intel Tofino targets), adding polymorphism, abstract hierarchical pipeline locations, compile-time vectors and bounded loops, and type inference. Proves soundness and encodes ordering-constraint checking as an SMT constraint encoding; loops are safely verified by unrolling three iterations. Demonstrations include reusable libraries and applications: Bloom filters, sketches, cuckoo hash tables, distributed firewalls, DNS reflection defenses, NATs, and a probabilistic traffic monitor; artifacts are available.

AI-written summary · about

" chapters (13)

1. 0:00Intro
2. 0:37Switch Pipeline
3. 2:31Lucid: A Language for Control in the Data Plane
4. 7:02Polymorphic Function Types Function types may also refer to polymorphic locations (here, a and b)
5. 7:53First Extension: Compound, Abstract Data Types
6. 10:47Abstracting Records
7. 12:25Hierarchical Locations
8. 15:47Second Extension: Vectors and Bounded Loops
9. 17:39Typechecking loops Tricky part catching errors across iterations of a loop
10. 18:26Loop Unrolling Lemma
11. 19:54Related Work
12. 20:16Conclusion
13. 23:50Pipeline Types: The Basics If we try to access a global after we've passed it in the pipeline, ERROR!

" related talks

• 01h 08mThe Network is the Computer: A Programming Language PerspectiveNate Foster · POPL 2024
• 47mDeep Programmability: A New Lens on NetworkingNate Foster · ICFP 2022
• 29mSwitchLog: A Logic Programming Language for Network SwitchesVaibhav Mehta, Devon Loehr, David Walker, John Sonchack · PADL 2023
• 14mEmpower Programmable Pipeline for Advanced Stateful Packet ProcessingYong Feng, Bin Liu, Yang Xu, Zhikang Chen, Haoyu Song, Chuwen Zhang, Yinchao Zhang, Hanyi Zhou, Ruoyu Sun, Wenkuo Dong, Peng Lu, Shuxin Liu · 21st USENIX Symposium on Networked Systems Design and Implementation (NSDI '24)
• 15mIsolation Mechanisms for High-Speed Packet-Processing PipelinesAurojit Panda, Tao Wang, Anirudh Sivaraman, Gianni Antichi, Xiangrui Yang · 19th USENIX Symposium on Networked Systems Design and Implementation (NSDI '22)
• 18mP4Cub: A Little Language for Big RoutersEric Hayden Campbell, Nate Foster, Rudy Peterson, Ryan Doenges, John Chen, Natalie Isak, Calvin Shyu, Parsia Ataei · CPP 2023
• 19mHOL4P4: mechanized small-step semantics for P4Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam · OOPSLA 2024
• 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)