Wed 15 Jun 2022 14:30 - 14:50 at Cockatoo - Domain Specific Languages Chair(s): Zachary Tatlock

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.

Wed 15 Jun

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 14:50
Domain Specific LanguagesSIGPLAN Track at Cockatoo
Chair(s): Zachary Tatlock University of Washington
13:30
20m
Talk
(POPL 2021) Petr4: Formal Foundations for P4 Data Planes
SIGPLAN Track
Ryan Doenges Cornell University, Mina Tahmasbi Arashloo Cornell University, Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Alexander Chang Cornell University, Newton Ni Cornell University, Samwise Parkinson Cornell University, Rudy Peterson Cornell University, Alaia Solko-Breslin Cornell University, Amanda Xu Cornell University, Nate Foster Cornell University
13:50
20m
Talk
(PLDI 2020) Predictable Accelerator Design with Time-Sensitive Affine Types
SIGPLAN Track
Rachit Nigam Cornell University, Sachille Atapattu Cornell University, USA, Samuel Thomas Cornell University, USA, Theodore Bauer AWS Inc, Apurva Koti Cornell University, USA, Zhijing Li Cornell University, USA, Yuwei Ye Cornell University, USA, Adrian Sampson Cornell University, Zhiru Zhang Cornell University, USA
14:10
20m
Talk
(POPL 2022) Dependently-Typed Data Plane Programming
SIGPLAN Track
Matthias Eichholz Technical University of Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt
14:30
20m
Talk
(POPL 2022) Safe, Modular Packet Pipeline Programming
SIGPLAN Track
Devon Loehr Princeton University, David Walker Princeton University