一句话：在 HOL4 中形式化 P4 16 的小步语义与类型系统，支持 extern、并发及体系结构级端到端包处理验证。
本文提出首个能充分刻画 P4 16 关键特性的网络数据平面语言 P4 语义，涵盖外部函数（extern）与并发；在 P4 中 extern 调用是线程间相互影响的唯一途径。语义采用小步风格，避免使用堆，以反映 P4 无通用内存且支持多线程的特点。除语言语义外，还给出体系结构级语义，可组合 P4 程序块、建模端到端包处理，并支持仲裁与包重循环等特性。作者提供相应类型系统，并证明进展、保持与类型可靠性。语义、类型系统及元理论均在 HOL4 定理证明器中形式化；由此导出可执行语义，支持对具有部分符号包的程序的受验证执行，以验证简单端到端程序性质。
We present the first semantics of the network data plane programming language P4 able to adequately capture all key features of P4 16 , the most recent version of P4, including external functions (externs) and concurrency. These features are intimately related since, in P4, extern invocations are the only points at which one execution thread can affect another. Reflecting P4’s lack of a general-purpose memory and the presence of multithreading the semantics is given in small-step style and eschews the use of a heap. In addition to the P4 language itself, we provide an architectural level semantics, which allows the composition of P4-programmed blocks, models end-to-end packet processing, and can take into account features such as arbitration and packet recirculation. A corresponding type system is provided with attendant progress, preservation, and type-soundness theorems. Semantics, type system, and meta-theory are formalized in the HOL4 theorem prover. From this formalization, we derive a HOL4 executable semantics that supports verified execution of programs with partially symbolic packets able to validate simple end-to-end program properties.
@article{paperbot2520,
title = {HOL4P4: Mechanized Small-Step Semantics for P4},
author = {Anoud Alshnakat and Didrik Lundberg and Roberto Guanciale and Mads Dam},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA1},
year = {2024},
doi = {10.1145/3649819}
}