The P4 language and programmable switch hardware, like the Intel Tofino, have made it possible for network engineers to write new programs that customize operation of computer networks, thereby improving performance, fault-tolerance, energy use, and security. Unfortunately, \emph{possible} does not mean \emph{easy}—there are many implicit constraints that programmers must obey if they wish their programs to compile to specialized networking hardware. In particular, all computations on the same switch must access data structures in a consistent order, or it will not be possible to lay that data out along the switch’s packet-processing pipeline. In this paper, we define Pipe, a new language and type system that guarantees programs access data in a consistent order and hence are \emph{pipeline-safe}. Pipe builds on top of Lucid, which is also pipeline-safe, but lacks the features needed for modular construction of data structure libraries. Hence, Pipe adds (1) polymorphism and ordering constraints for code reuse; (2) abstract, hierarchical pipeline locations and data types to support information hiding; (3) compile-time constructors, vectors and loops to allow for construction of flexible data structures; and (4) type inference to lessen the burden of program annotations. We develop the meta-theory of Pipe, prove soundness, and show how to encode constraint checking as an SMT problem. We demonstrate the utility of Pipe by developing a suite of useful networking libraries and applications that exploit our new language features, including Bloom filters, sketches, cuckoo hash tables, distributed firewalls, DNS reflection defenses, network address translators (NATs) and a probabilistic traffic monitoring service.
Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change
10:20 - 12:00 | |||
10:20 25mResearch paper | Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson POPL DOI Media Attached | ||
10:45 25mResearch paper | Fair Termination of Binary SessionsRemote POPL DOI Media Attached | ||
11:10 25mResearch paper | Safe, Modular Packet Pipeline ProgrammingRemote POPL DOI Media Attached | ||
11:35 25mResearch paper | Dependently-Typed Data Plane ProgrammingRemote POPL Matthias Eichholz TU Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt DOI Media Attached |