MatchBox: A Semantic Foundation for Data Plane PortabilityDistinguished Paper
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 \textsc{MatchBox}, a system for translating match-action tables across heterogeneous environments. At its core is the \emph{Match Algebra}, a compositional formalism for concisely and declaratively expressing transformations on match-action tables. To ensure unambiguous semantics, \textsc{MatchBox} introduces a static type system based on \emph{guarded functional dependencies (GFDs)} that guarantees that every well-typed Match Algebra expression denotes a well-defined function. From such specifications, the \textsc{MatchBox} compiler efficiently computes compact target tables that are semantically faithful. Across case studies in programmable switches, multi-cloud firewalls, and eBPF systems, \textsc{MatchBox} enables concise, declarative portability specifications and realizes them as compact target tables.
Wed 17 JunDisplayed time zone: Mountain Time (US & Canada) change
14:00 - 15:40 | Networking and Distributed SystemsPLDI Research Papers at Flatirons 2 Chair(s): Mae Milano Princeton University | ||
14:00 20mTalk | A Formally Verified Foundation for Compositional Heterogeneous Coherence PLDI Research Papers An Qi Zhang University of Utah, Andrés Goens TU Darmstadt, Daniel Sorin Duke University, Vijay Nagarajan University of Utah DOI | ||
14:20 20mTalk | MatchBox: A Semantic Foundation for Data Plane PortabilityDistinguished Paper PLDI Research Papers Eric Hayden Campbell University of Texas at Austin, Robert Zhang University of Texas at Austin, Divyanshu Saxena University of Texas at Austin, Aditya Akella University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI | ||
14:40 20mTalk | SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols PLDI Research Papers Longfei Qiu Yale University, Jingqi Xiao University of Hong Kong, Ji-Yong Shin Northeastern University, Zhong Shao Yale University DOI | ||
15:00 20mTalk | Implementability of Global Distributed Protocols Modulo Network Architectures PLDI Research Papers DOI | ||
15:20 20mTalk | Weighted NetKAT: A Programming Language For Quantitative Network Verification PLDI Research Papers Emmanuel Suárez Acevedo Cornell University, Tiago Ferreira University College London, Kevin Batz Cornell University, Oliver Emil Bøving Technical University of Denmark, Nate Foster EPFL; Jane Street, Alexandra Silva Cornell University DOI | ||