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.