kirancodes.me
To Proof Maintenance & Beyond!
PLDI 2026★ Distinguished Paper

MatchBox: A Semantic Foundation for Data Plane Portability

Eric Hayden Campbell, Robert Zhang, Divyanshu Saxena, Aditya Akella, Isil Dillig

Abstract

Match-action tables are the core abstraction underlying network packet-processing systems, from fixed-function switches to eBPF-based software dataplanes. However, their concrete syntax and semantics vary widely across programming environments, reflecting differences in hardware generations, engineering practices, and vendor design choices. This syntactic and semantic variation renders portability of match-action tables across environments a persistent challenge. This paper presents MatchBox , a system for translating match-action tables across heterogeneous environments. At its core is the Match Algebra , a compositional formalism for concisely and declaratively expressing transformations on match-action tables. To ensure unambiguous semantics, MatchBox introduces a static type system based on guarded functional dependencies (GFDs) that guarantees that every well-typed Match Algebra expression denotes a well-defined function. From such specifications, the MatchBox compiler efficiently computes compact target tables that are semantically faithful. Across case studies in programmable switches, multi-cloud firewalls, and eBPF systems, MatchBox enables concise, declarative portability specifications and realizes them as compact target tables.

Related papers