Petr4: formal foundations for p4 data planes
Abstract
P4 is a domain-specific language for programming and specifying 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 has developed without a formal foundation. The P4 Language Specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode, leaving many aspects of the language semantics up to individual compilation targets. The P4 reference implementation is a complex system, running to over 40KLoC of C++ code, with support for only a few targets. Clearly neither of these artifacts is suitable for formal reasoning about P4 in general.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Jan 04, 2021
- Source ID
- 10.1145/3434322
Entities
People
- A. S. Chang
- Alaia Solko-breslin
- Amanda Xu
- Mina Tahmasbi Arashloo
- Nate Foster
- Newton Ni
- Rudy Peterson
- Ryan Doenges
- Samwise Parkinson
- Santiago Bautista
Organizations
- Cornell University
- Defense Advanced Research Projects Agency
- Fujitsu
- Infosys
- Keysight Technologies
- National Science Foundation