MatchBox: A Semantic Foundation for Data Plane Portability
summary
MatchBox provides a provable translation pipeline that turns source match-action tables into compact, semantically equivalent target tables using a new declarative language called Match Algebra, a static type system based on guarded functional dependencies, and a monadic compiler that emits concrete tables. The system handles P4-like programmable switches, multi-cloud firewall policies, and eBPF dataplanes, and the paper reports that generated tables are compact and run at industrial scale and speed (artifacts available).
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:45What is MatchBox
- 1:48Match-action tables
- 3:35Switch behavior variations
- 5:20Porting tables with MatchBox
- 6:25Match algebra expression
- 7:51Type system for match algebra
- 8:53Match algebra operators
- 12:06Parallel join and pairing
- 13:34Function composition
- 14:36Transforming table keys
- 16:22Guarded functional dependencies
- 17:23Case studies and evaluation
- 18:07Q&A
related talks
47mDeep Programmability: A New Lens on Networking
18mLearning-Enhanced High-Throughput Pattern Matching Based on Programmable Data Plane
25mDataplane equivalence and its applications
22mDependently-Typed Data Plane Programming
15mEnabling In-situ Programmability in Network Data Plane: From Architecture to Language
01h 08mThe Network is the Computer: A Programming Language Perspective
28mSafe, Modular Packet Pipeline Programming
12mFlightplan: Dataplane Disaggregation and Placement for P4 Programs