Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Wed 20 Jan 2021 16:20 - 16:30 at POPL-B - Semantics

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 - 17:00: SemanticsPOPL at POPL-B
16:00 - 16:10
Talk
A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types
POPL
Chao-Hong ChenIndiana University, Amr SabryIndiana University
Link to publication DOI
16:10 - 16:20
Talk
Internalizing Representation Independence with Univalence
POPL
Carlo AngiuliCarnegie Mellon University, Evan CavalloCarnegie Mellon University, Anders MörtbergDepartment of Mathematics, Stockholm University, Max ZeunerStockholm University
Link to publication DOI
16:20 - 16:30
Talk
Petr4: Formal Foundations for P4 Data Planes
POPL
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 University
Link to publication DOI Pre-print
16:30 - 16:40
Talk
The (In)Efficiency of Interaction
POPL
Beniamino AccattoliInria & Ecole Polytechnique, Ugo Dal LagoUniversity of Bologna, Italy / Inria, France, Gabriele VanoniUniversity of Bologna & INRIA Sophia Antipolis
Link to publication DOI
16:40 - 16:50
Talk
Functorial Semantics for Partial Theories
POPL
Chad NesterTallinn University of Technology, Ivan Di LibertiCzech Academy of Sciences, Fosco LoregianTallinn University of Technology, Pawel SobocinskiTallinn University of Technology
Link to publication DOI
16:50 - 17:00
Break
Break
POPL