P4Testgen: An Extensible Test Oracle For P4

TL;DR

P4Testgen is an extensible, automated test oracle for the P4 language that models target semantics, handles complex externs, and has been validated across multiple architectures, uncovering bugs in production toolchains.

Contribution

It introduces P4Testgen, a comprehensive test oracle for P4 that supports multiple architectures and handles non-determinism and externs through advanced techniques.

Findings

Validated P4Testgen across multiple architectures.

Discovered 25 bugs in production P4 toolchains.

Achieved high coverage with reduced test sets.

Abstract

We present P4Testgen, a test oracle for the P4$_{16}$ language. P4Testgen supports automatic test generation for any P4 target and is designed to be extensible to many P4 targets. It models the complete semantics of the target's packet-processing pipeline including the P4 language, architectures and externs, and target-specific extensions. To handle non-deterministic behaviors and complex externs (e.g., checksums and hash functions), P4Testgen uses taint tracking and concolic execution. It also provides path selection strategies that reduce the number of tests required to achieve full coverage. We have instantiated P4Testgen for the V1model, eBPF, PNA, and Tofino P4 architectures. Each extension required effort commensurate with the complexity of the target. We validated the tests generated by P4Testgen by running them across the entire P4C test suite as well as the programs supplied with the Tofino P4 Studio. Using the tool, we have also confirmed 25 bugs in mature, production toolchains for BMv2 and Tofino.