一句话：提出 Petr4，用定义式解释器与核心演算为 P4 数据平面建立形式化语义，并通过大规模测试和类型保持终止性证明验证。
P4 是定义数据包处理系统的领域特定语言，但长期缺乏形式化基础：规范混合非形式化描述与伪代码，参考实现庞大且仅支持少数目标，难以支撑一般形式推理。本文提出 Petr4，为 P4 建立坚实基础。Petr4 含一个全新定义式解释器和一个建模 P4 片段的核心演算。解释器不绑定特定目标，而通过目标接口集中收集委托给目标的功能；核心演算用非确定性过近似目标相关行为。作者用参考实现中 750 多个覆盖不同目标的测试验证解释器，并证明核心演算的类型保持终止性。开发中还报告了规范与参考实现的数十个缺陷，许多已修复。
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.
@article{paperbot1175,
title = {Petr4: formal foundations for p4 data planes},
author = {Ryan Doenges and Mina Tahmasbi Arashloo and Santiago Bautista and Alexander Chang and Newton Ni and Samwise Parkinson and Rudy Peterson and Alaia Solko-Breslin and Amanda Xu and Nate Foster},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434322}
}