COPLAS Talk: A Fast Compiler for NetKAT
Talk by Nate Foster, Cornell University
High-level programming languages play a key role in a growing number of networking platforms. Languages such as nlog and Pyretic are being used in systems such as VMware NVP and SDX to streamline application development and enable formal reasoning about network behavior. But the use of high-level languages comes with a cost: current compilers can take tens of minutes to generate the forwarding state for the network, even on relatively simple programs and small topologies. This forces programmers to waste time working around performance issues or even revert to using hardware-level APIs.
This talk will presents a compiler pipeline for the NetKAT programming language that is orders of magnitude faster than previous compilers for high-level network languages. The compiler is based on new algorithms that use a generalization of binary decision diagrams as an intermediate representation and symbolic automata to generate optimized forwarding state. It also handles programs that use network-wide features such as regular paths and virtual topologies. I will describe the design and implementation of three essential compiler stages: from local programs (which specify single-switch behavior) to forwarding tables, from global programs (which specify network-wide behavior) to local programs, and from virtual programs (which specify behavior in terms of virtual topologies) to global programs. I will also discuss our implementation and present results from experiments on real-world benchmarks that quantify performance in terms of compilation time and forwarding table size.
Joint work with Steffen Smolka (Cornell), Spiros Eliopoulos (Inhabited Type), and Arjun Guha (UMass).
Dexter Kozen and Fritz Henglein