Software dataplanes are emerging as an alternative to traditional hardware switches and routers, promising programmability and short time to market. These advantages are set against the concern of introducing buggy or under-performing code into the network. We explore whether it is practical to formally prove that a software dataplane satisfies key properties that would ensure smooth network operation. In general, proving properties of real programs remains an elusive goal, but we argue that dataplanes are different: they typically follow a pipeline structure that enables our proposed approach, in which we verify pieces of the code in isolation, then compose the results to reason about the entire dataplane. We preliminarily demonstrate the potential of our approach by applying it on simple Click pipelines and proving that they are crash-free and execute a bounded number of instructions. This takes on the order of minutes, whereas a general-purpose state-of-the-art verifier fails to complete the same task within 12 hours.

We revisit the problem of scaling software routers, motivated by recent advances in server technology that enable high-speed parallel processing--a feature router workloads appear ideally suited to exploit. We propose a software router architecture that parallelizes router functionality both across multiple servers and across multiple cores within a single server. By carefully exploiting parallelism at every opportunity, we demonstrate a 35Gbps parallel router prototype; this router capacity can be linearly scaled through the use of additional servers. Our prototype router is fully programmable using the familiar Click/Linux environment and is built entirely from off-the-shelf, general-purpose server hardware.