Petr4：P4数据平面的正式基础
Petr4: Formal Foundations for P4 Data Planes
摘要：
P4是一种用于编程和指定数据包处理系统的特定领域语言。它基于一个优雅的设计，具有高级抽象，如解析器和匹配操作管道，可以编译为软件或硬件中的有效实现。不幸的是，像许多工业语言一样，P4的发展没有正式的基础。P4语言规范是一个160页的文档，混合了非正式的散文、图形图表和伪代码。P4参考实现是一个复杂的系统，运行超过40KLoC的C++代码。显然，这两种人工制品都不适合形式推理。本文提出了一个新的框架，称为Petr 4，把P4的坚实基础。Petr 4由一个干净的定义解释器和一个演算组成，该演算对P4的核心片段的语义进行建模。在整个规范中，程序行为的某些方面留给目标。我们的解释器是在一个目标接口上参数化的，该接口将规范中所有特定于目标的行为收集在一个接口中。该规范对某些程序结构的嵌套进行了特别的限制，以简化编译并避免程序不终止的可能性。我们通过对核心演算的类型系统进行分层，而不是强加不自然的语法限制，来捕捉核心演算的后一个意图，并且我们证明了核心演算中的所有程序都可以终止。我们已经通过P4参考实现中的750多个测试对解释器进行了验证，并通过针对不同目标的测试来练习我们的目标接口。我们在分层型系统上用归纳法建立了核心演算的终止性。在开发Petr 4时，我们报告了语言规范和参考实现中的数十个错误，其中许多已经修复。
英文摘要：
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. 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. Throughout the specification, some aspects of program behavior are left up to targets. Our interpreter is parameterized over a target interface which collects all the target-specific behavior in the specification in a single interface. The specification makes ad-hoc restrictions on the nesting of certain program constructs in order to simplify compilation and avoid the possibility of nonterminating programs. We captured the latter intention in our core calculus by stratifying its type system, rather than imposing unnatural syntactic restrictions, and we proved that all programs in this core calculus terminate. 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 established termination for the core calculus by induction on the stratified type system. While developing Petr4, we reported dozens of bugs in the language specification and the reference implementation, many of which have been fixed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
