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.
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 core calculus that models a fragment of P4. Petr4 is not tied to any particular target: the interpreter is parameterized over an interface that collects features delegated to targets in one place, while the core calculus overapproximates target-specific behaviors using non-determinism.
We have validated the interpreter against a suite of over 750 tests from the P4 reference implementation, exercising our target interface with tests for different targets. We validated the core calculus with a proof of type-preserving termination. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.
Wed 20 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
|16:00 - 16:10|
|A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types|
POPLLink to publication DOI
|16:10 - 16:20|
|Internalizing Representation Independence with Univalence|
Carlo AngiuliCarnegie Mellon University, Evan CavalloCarnegie Mellon University, Anders MörtbergDepartment of Mathematics, Stockholm University, Max ZeunerStockholm UniversityLink to publication DOI
|16:20 - 16:30|
|Petr4: Formal Foundations for P4 Data Planes|
Ryan DoengesCornell University, Mina Tahmasbi ArashlooCornell University, Santiago BautistaUniv Rennes, ENS Rennes, Inria, IRISA, Alexander ChangCornell University, Newton NiCornell University, Samwise ParkinsonCornell University, Rudy PetersonCornell University, Alaia Solko-BreslinCornell University, Amanda XuCornell University, Nate FosterCornell UniversityLink to publication DOI Pre-print
|16:30 - 16:40|
|The (In)Efficiency of Interaction|
Beniamino AccattoliInria & Ecole Polytechnique, Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Gabriele VanoniUniversity of Bologna & INRIA Sophia AntipolisLink to publication DOI
|16:40 - 16:50|
|Functorial Semantics for Partial Theories|
Chad NesterTallinn University of Technology, Ivan Di LibertiCzech Academy of Sciences, Fosco LoregianTallinn University of Technology, Pawel SobocinskiTallinn University of TechnologyLink to publication DOI
|16:50 - 17:00|