P4 is a domain-specific language for specifying the behavior of packet-processing systems. It is based on an elegant design with high-level abstractions like parsers and match-action pipelines that can be compiled to efficient implementations in software or hardware. Unfortunately, like many industrial languages, P4 lacks a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code. Clearly neither of these artifacts is suitable for formal reasoning.
This paper presents a new framework, called Petr4, that puts P4 on a solid foundation. Petr4 consists of a clean-slate definitional interpreter and a calculus that models the semantics of a core fragment of P4. We have validated the interpreter against a suite of over 750 tests from the P4 reference implementation and used the calculus to establish key properties such as type soundness and termination. While developing Petr4, we discovered dozens of bugs in the language specification and the reference implementation, many of which have been fixed.
Wed 15 JunDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 14:50
|(POPL 2021) Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges Cornell University, Mina Tahmasbi Arashloo Cornell University, Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Alexander Chang Cornell University, Newton Ni Cornell University, Samwise Parkinson Cornell University, Rudy Peterson Cornell University, Alaia Solko-Breslin Cornell University, Amanda Xu Cornell University, Nate Foster Cornell University
|(PLDI 2020) Predictable Accelerator Design with Time-Sensitive Affine Types
Rachit Nigam Cornell University, Sachille Atapattu Cornell University, USA, Samuel Thomas Cornell University, USA, Theodore Bauer AWS Inc, Apurva Koti Cornell University, USA, Zhijing Li Cornell University, USA, Yuwei Ye Cornell University, USA, Adrian Sampson Cornell University, Zhiru Zhang Cornell University, USA
|(POPL 2022) Dependently-Typed Data Plane Programming
|(POPL 2022) Safe, Modular Packet Pipeline Programming