Octopus: Practical Equivalence Checking of P4 Packet Parsers
2026-08-03 • Logic in Computer Science
Logic in Computer ScienceProgramming Languages
AI summaryⓘ
The authors developed Octopus, a tool that helps check if two programs written in P4 (a language for designing how network devices read data packets) behave the same way. Octopus works by turning these programs into a type of mathematical model called automata and then symbolically comparing them. It can quickly show if the two programs are equivalent or provide an example when they differ. Unlike older methods, Octopus can handle more complex programs efficiently on regular computers. The authors also tested how well the tool works in real networking situations.
P4packet parserautomatasymbolic equivalence checkingbisimulationcounterexampleprotocol-independent packet processingnetworkingbit-stream
Authors
Jort van Leenen, Tobias Kappé
Abstract
P4 is a domain-specific language for programming protocol-independent packet processors, where packet parsers describe how incoming bit-streams are structured into headers and fields. Building on work by Doenges et al. (2022), we present Octopus, a tool that translates P4 packet parsers into automata and then attempts to (symbolically) check their equivalence. Octopus produces evidence, either in the form of a bisimulation demonstrating equivalence, or a counterexample bit-stream witnessing a behavioral difference between the two parsers. In contrast with earlier work, our tool can check equivalence between non-trivial parsers within minutes, on consumer hardware. We report on the tool's implementation and evaluate its usability in networking contexts.