Petr4: Formal Foundations for P4 Data Planes
summary
Petr4 provides a clean‑slate definitional interpreter and a compact core calculus that models a P4 fragment, validated by running over 750 tests from the P4 reference suite. The interpreter is about 10KLoC OCaml interpreter, parameterized by an architecture interface; the paper proves a type‑preserving termination theorem for the calculus. Development finds and reports dozens of bugs in the 160‑page spec and the 40KLoC C++ reference implementation, and includes a web demo that evaluates P4 programs end to end.
AI-written summary · about
chapters (29)
- 0:00Intro
- 1:03The Data Plane
- 1:54Networking has Flown the IETF Nest
- 2:22Languages for Data Plane Programming
- 2:34P4 Unifies Data Planes
- 2:53This Work: Foundations for P4 Data Planes
- 3:21Example: Source Routing + ACL
- 3:53Packet-Processing Phases
- 4:24P4 Header Types
- 4:37Packet Parsing in P4 type
- 5:47Packet Transformations in P4 metadata
- 6:38Deparsing in P4
- 6:59A Subtle Bug...
- 8:26Some Benefits of Foundations
- 9:08The Petr 4 System
- 11:07P4 in situ
- 11:36Excavating the P4 Type System
- 13:32The Final Result
- 13:52What is P4's Type System?
- 14:41The Petr4 Solution
- 15:27Returning to Our Dig: Evaluation
- 16:38What is P4's Operational Behavior?
- 18:13The Petr4 Implementation
- 19:13Core Calculus
- 19:54Metatheory
- 20:18Case Study: Adding Type-Safe Unions
- 20:48Tested Semantics
- 25:35Ongoing and Future Work
- 26:32Conclusion
related talks
19mHOL4P4: mechanized small-step semantics for P4
22mDependently-Typed Data Plane Programming
18mP4Cub: A Little Language for Big Routers
19mP4R-Type: A Verified API for P4 Control Plane Programs
25mP4-SpecTec: A Language Mechanization Framework for P4
15mOn Temporal Verification of Stateful P4 Programs
12mFlightplan: Dataplane Disaggregation and Placement for P4 Programs
01h 08mThe Network is the Computer: A Programming Language Perspective