Register to attend this P4 Developer Days webinar, “Mechanizing the P4 Language Specification with P4-SpecTec”
Date: September 10th 4:00pm PST | September 11th – 8:00am KST
Abstract
The P4 language has four main representations of its syntax and semantics: the official specification, formalizations, implementations, and a test suite. While the four representations are intended to consistently define the P4 language, they often diverge, as each is managed by different parties and evolves at a different pace. This lack of alignment complicates both specification evolution and compiler maintenance.
To address this challenge, we present P4-SpecTec, a mechanized specification infrastructure for the P4 language. Inspired by successful language mechanization frameworks such as Wasm-SpecTec for WebAssembly and ESMeta for JavaScript, P4-SpecTec introduces a formal, complete, and mechanized P4 language definition. From this single source of truth — the mechanized specification — we aim to generate multiple backends, such as a type checker, interpreter, test suite, and specification document, in a consistent and automated manner.
P4-SpecTec is an ongoing project, where we currently mechanized the P4 type system. Notably, our mechanized type system is executable. That is, the typing rules can be executed, acting as a P4 type checker. Our mechanized specification passes more than 97% of the applicable tests in the p4c test suite. This process already revealed inconsistencies and underspecified behaviors in both the P4 specification and its reference compiler. Based on the mechanized model, we further developed a negative test generation technique that automatically produces ill-typed P4 programs that trigger subtle and diverse ill-typed conditions in the P4 type system. This approach has uncovered 11 compiler bugs and 12 soundness issues in the p4c frontend.
This talk introduces the design of P4-SpecTec, current progress, and long-term vision for a more robust and consistent P4 language ecosystem.
Speaker
Jaehyun Lee is a graduate student in the Programming Language Research Group at KAIST, advised by Sukyoung Ryu. His research focuses on mechanizing programming language definitions to improve their reliability and precision. He leads the P4-SpecTec project, which is a mechanized specification infrastructure for P4. Previously, he contributed to the Wasm-SpecTec project, now part of the official WebAssembly specification authoring toolchain. As part of that effort, he co-authored the paper “Bringing the WebAssembly Standard Up to Speed with SpecTec”, presented at PLDI 2024. His goal is to make language specifications reliable and better aligned with the needs of the developer community.