ACM SIGCOMM Workshop on Networking and Programming Languages (NetPL 2016)
Monday, August 22nd
The workshop will take place at Room Agata 2.
Monday, August 22, 2016
8:30am - 5:30pm Talks
- %s %s
The Next 700 Network Programming Languages
Nate Foster (Cornell University)
Abstract: Specification and verification of computer networks has become a reality in recent years, with the emergence of domain-specific programming languages and automated verification tools. But the design of these languages and tools has been largely ad hoc, driven more by the needs of applications and the capabilities of hardware than by any foundational principles. This talk will present NetKAT, a language for programming networks based on a well-studied mathematical foundation, Kleene Algebra with Tests (KAT). The talk will describe the design of the language, its semantic underpinnings, and extensions with features to support stateful and probabilistic programming.
NetKAT is joint work with colleagues at Cornell, Facebook, Inhabited Type, Princeton, Samsung, UCL, and UMass Amherst.
Bio: Nate Foster is an Assistant Professor of Computer Science at Cornell University. The goal of his search is developing programming languages and tools for building reliable systems. He received a PhD in Computer Science from theUniversity of Pennsylvania in 2009, an MPhil in History and Philosophy of Science from Cambridge University in 2008, and a BA in Computer Science from Williams College in 2001. His awards include a Sloan Research Fellowship, an NSF CAREER Award, a Most Influential POPL Paper Award, a Tien '72 Teaching Award, a Google Research Award, a Yahoo! Academic Career Enhancement Award, and the Morris and Dorothy Rubinoff Award.
Symmetries and Surgeries for Network Verification and Quantitative Network Analysis
Nikolaj Bjorner (Microsoft Research)
Abstract: Packet switched networks build in redundancies that enable scale and fault tolerance. Such redundancies are conveniently implemented by placing routers in symmetric or near symmetric configurations. The symmetries are also present at the level of routing tables. When it comes to checking properties of such networks, whether it being reachability or quantitative properties, such as congestion, the gain in recognizing such symmetries can be dramatic. Reducing the networks to their asymmetric core enables scaling analysis by order of magnitudes compared to a straight-forward analysis. In this talk I describe our efforts around extracting and exploiting symmetries and bisimulations in data-center and wide-area networks. In this quest we develop algorithms that find bisimilar routing states that exploit properties of packet switched routers. We also introduce a data-structure (ddNF) for extracting sets of IP headers that are treated equivalently from the point of view of routing tables. We then develop a notion of bisimulations to quantitative settings.
Bio: Nikolaj Bjorner is a Principal Researcher at Microsoft Research, Redmond, working in the area of Automated Theorem Proving and Software Engineering. His current main line of work is around the state-of-the art theorem prover Z3, which is used as a foundation of several software engineering tools. Z3 is developed by Leonardo de Moura, Nikolaj Bjorner and Christoph Wintersteiger. Z3 received the 2015 ACM SIGPLAN Software System’s award. Previously, he designed the DFSR, Distributed File System - Replication, shipped with Windows Server since 2005 and before that worked on distributed file sharing systems at a startup XDegrees, and program synthesis and transformation systems at the Kestrel Institute. He received his Master’s and Ph.D. degrees in computer science from Stanford University, and spent the first three years of university at DTU and DIKU.
David Walker (Princeton University)
Abstract: Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Oftentimes, these systems are disjoint—one language for programming and another for verification, and yet another for run-time monitoring and debugging. In this paper, we present a new, unified framework, called Temporal NetKAT, capable of facilitating all of these tasks at once. As its name suggests, Temporal NetKAT is the synthesis of two formal theories: past-time (finite trace) linear temporal logic and (network) Kleene Algebra with Tests. Temporal predicates allow programmers to write down concise properties of a packet’s path through the network and to make dynamic packet-forwarding, access control or debugging decisions on that basis. In addition to being useful for programming, the combined equational theory of LTL and NetKAT facilitates proofs of path-based correctness properties. Using new, general, proof techniques, we show that the equational semantics is sound with respect to the denotational semantics, and, for a class of programs we call network-wide programs, complete. We have also implemented a compiler for temporal NetKAT, evaluated its performance on a range of benchmarks, and studied the effectiveness of several optimizations.
This is joint work with Ryan Beckett and Michael Greenberg.
Bio: David Walker is a Professor of Computer Science at Princeton University. He received his B.Sc. from Queen's University, Canada in 1995 and his Ph.D. in Computer Science from Cornell University in 2001. His research interests include programming language theory, design and implementation of all kinds. He is especially interested in type systems and the development of new domain-specific programming languages. He won an NSF Career award in 2003 and Alfred Sloan Fellowship in 2004. In 2007, with his students and colleagues at Princeton, he won the PLDI best paper award for the paper entitled Fault-Tolerant Typed Assembly Language. In 2008, his paper From System F to Typed Assembly Language, co-authored with Greg Morrisett, Karl Crary and Neal Glew, won a 10-year retrospective award for most influential POPL 1998 paper. In 2013, with his students and colleagues at Princeton and Cornell, he won the NSDI community award for his paper on Composing Software-Defined Networks. He served as an associate editor for ACM TOPLAS from 2007-2015, as the Program Chair for POPL 2015, and won the ACM SIGPLAN Robin Milner Young Researcher Award in 2015.
Interactive Query for Dynamic Network Analytics
Haoyu Song (Huawei Technologies)
Abstract: Network data plane needs to be interactively programmed in order to support Dynamic Network Analytics (DNA). We envision the high level DNA applications can be break down into a set of queries and the queries can be further compiled into incremental configurations to the data plane. We emphasize the need to define standard DNA APIs and/or query language for DNA system.
Bio: Haoyu Song is a principal architect at Huawei Technologies. He is a leading researcher on SDN programmable data plane. His current research interests span all aspects of the SDN/NFV ecosystem. He was a researcher at Bell Labs, Alcatel-Lucent before joining Huawei. He hold a doctoral degree in computer engineering from Washington University in St. Louis.
Verifying Reachability in Networks with Mutable Datapaths
Aurojit Panda (UC Berkeley)
Abstract: Recent work has made great progress in verifying the forwarding correctness of networks. However, these approaches cannot be used to verify networks containing middleboxes, such as caches and firewalls, whose forwarding behavior depends on previously observed traffic. We explore how to verify reachability properties for networks that include such "mutable datapath" elements. We want our verification results to hold not just for the given network, but also in the presence of failures. The main challenge lies in scaling the approach to handle large and complicated networks, We address by developing and leveraging the concept of slices, which allow network-wide verification to only require analyzing small portions of the network. We show that with slices the time required to verify an invariant on many production networks is independent of the size of the network itself.
Bio: Aurojit Panda is a PhD candidate at UC Berkeley advised by Scott Shenker. His research largely focuses on how to simplify developing and deploying new network services.
NEMO Engine, A Model Driven Compiler to Execute User's Intent and Manage Service Lifecycle by Multi Layer State Machine
Yinben Xia (Huawei Technologies)
Abstract: In last year's NetPL workshop, I introduced an intent oriented network service programming language - NEMO. This time, I will introduce NEMO's model driven compiler, which compiles intent language to real network executable interface. Second, I will introduce a multi layer state machine engine in NEMO compiler, which will handle various changes from equipments, requirement or governance policy. This engine provides an automatic change management capability for whole service lifecycle. In the last, I will update NEMO's open source implementation progress.
Bio: Dr. Yinben Xia is a senior staff researcher within Huawei's network research department from 2008. He dedicated his research effort in network architecture and SDN technologies. In recent two years, he lead a team to design and developer a NaaS (Network as a Service) programming language (NEMO Project). He owns 15 patents in related domain. He is leading a team to carry out SDN/NEMO research in Beijing. Before joining Huawei, Dr. Xia worked at IBM China Research Lab for 4 years after he got PH.D from Beijing University of Aeronautics and Astronautics.
Towards Correct-by-Construction SDN
Leonid Ryzhyk (Samsung Research America), Nikolaj Bjorner (Microsoft Research), Marco Canini (KAUST, KSA), Jean-Baptiste Jeannin, Nina Narodytska, Cole Schlesinger, Douglas B. Terry (Samsung Research America), George Varghese (Microsoft Research)
Formal Semantics and Automated Verification for the Border Gateway Protocol
Konstantin Weitz, Doug Woos, Emina Torlak, Michael D. Ernst, Arvind Krishnamurthy, Zachary Tatlock (University of Washington)
P4FPGA: High-Level Synthesis for Networking
Han Wang, Ki Suh Lee, Vishal Shrivastav, Hakim Weatherspoon (Cornell University)
Symbolic Execution — Model Equivalence & Applications
Matei Popovici, Radu Stoenescu, Lorina Negreanu, Costin Raiciu (University Politehnica of Bucharest)
Call for Participation
The NetPL workshop provides a forum to bring together researchers and practitioners from the fields of programming languages, formal methods, and networking.
Recent technological trends, such as Software-Defined Networking, Network Functions Virtualization and reconfigurable networking hardware, have created an opportunity for researchers in these traditionally separate communities to collaborate, applying their diverse perspectives towards the development of novel networking applications. It is important to clarify that the scope of this workshop goes strictly beyond SDN. We aim to enable language specialists to better understand opportunities in networking, and networking specialists to better understand opportunities enabled by specially-designed languages.
The program will include invited talks from experts in the field, with an emphasis on encouraging engaging technical discussions amongst the participants.This is the second NetPL workshop, after last year's workshop at ECOOP. All talks in the previous edition of the workshop are on YouTube.
NetPL Student Grants
The NetPL 2016 workshop has limited support for funding students to attend the workshop. Interested students can apply for a grant complement through the SIGCOMM travel grants application.
To apply, select the NetPL option during the application, and motivate your reasons for attending and tell us how you may contribute to the workshop in a separate section of the application letter.
- Confirmed Invited Speakers
Microsoft Research, USA
Xilinx Labs, USA
Brown University, USA
Barefoot Networks, USA
UC Berkeley, USA
April 29, 2016 Deadline May 9, 2016 Speaker notified
June 8, 2016
Travel grant applications due
August 22, 2016
- Workshop Co-Chairs
University of Massachusetts Amherst, USA
Università della Svizzera italiana (USI), Switzerland
University of Cambridge, UK