ACM SIGCOMM Workshop on Networking and Programming Languages (NetPL 2016)
Monday, August 22nd
Live Streaming
Please click here to watch NetPL on live streaming.
Location
The workshop will take place at Room Topazio 1 and 2.
Technical Program
- Opening Remarks
- Languages that will come ...
-
Update on P4: Where are we now, and where are we heading toward?
Changhoon Kim (Barefoot Networks)
Abstract: Since its original publication, P4 has been drawing significant attention from both networking industry and research community. Motivated by that, industry experts and research groups have formed the P4 Language Consortium and have been nurturing the language to produce an industry-wide common data-plane programming framework. In this talk I will summarize what has happened to P4 since its original publication, what kinds of activities are currently ongoing, who in the field of networking can benefit from P4 and how, what kinds of novel networking applications are being developed in P4, how we expect the language and its associated development tools to evolve, and what kinds of interesting research problems arise as data-plane programmability becomes commonplace. -
P4FPGA: High-Level Synthesis for Networking
Han Wang, Ki Suh Lee, Vishal Shrivastav, Hakim Weatherspoon (Cornell University)
Abstract: Field-programmable gate arrays (FPGAs) are often used to prototype custom packet processing algorithms. FPGAs are appealing because they balance the speed of hardware and the flexibility of software. From a programming language perspective, domain specific languages (DSLs), such as P4and PX, are emerging to allow succinct expression of packet processing algorithms. What remains difficult, is the process to translate high level DSLs to low-level hardware description language, such as Verilog, in order to generate FPGA firmware. This talk presents P4FPGA, an open-source framework that enables compilation of high-level P4 language to FPGA firmware. Our framework translates a given P4 program through a number of intermediate steps. It leverages existing intermediate representations of a P4 program,and generates corresponding Bluespec System Verilog (BSV) for simulation and synthesis. In addition, we provide runtime support for a packet processing algorithm to enable communication with network interfaces and host OS through PCI express bus. We have implemented a number of P4 applications on top of our framework to show its general applicability.
-
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. - Coffee Break
- ... for the needs of today and tomorrow
-
Temporal NetKAT
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. -
Towards Correct-by-Construction SDN
Leonid Ryzhyk (Samsung Research America), Nikolaj Bjorner (Microsoft Research), Marco Canini (Université catholique de Louvain, Belgium), Jean-Baptiste Jeannin, Nina Narodytska, Cole Schlesinger, Douglas B. Terry (Samsung Research America), George Varghese (Microsoft Research)
Abstract: High-level SDN languages raise the level of abstraction in SDN programming from managing individual switches to programming network-wide policies. In this talk, we present Cocoon (for Correct by Construction Networking), an SDN programming language designed around the idea of iterative refinement. The network programmer starts with a high-level functional description of the desired network behavior, focusing on the service the network should provide to each packet, as opposed to how this service is implemented within the network fabric. The programmer then iteratively refines the top-level specification, adding details of the topology, routing, fault recovery, etc., until reaching a level of detail sufficient for the Cocoon compiler to generate an SDN application that manages network switches via the southbound interface.
-
(Cancelled due to flight issues)
NEMO Engine, A Model Driven Compiler to Execute User's Intent and Manage Service Lifecycle by Multi Layer State MachineYinben 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. -
(Cancelled due to flight issues)
Interactive Query for Dynamic Network AnalyticsHaoyu 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. - Lunch Break
- With advanced methods to soar ...
-
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)
Abstract: We present the first mechanized formal semantics of BGP (implemented in the Coq proof assistant) that models all required features of the BGP specification RFC-4271 modulo low-level details. We demonstrate our semantic's correctness and usefulness by: 1) extending and formalizing the pen-and-paper proof by Gao & Rexford on the convergence of BGP, revealing necessary extensions to their original configuration guidelines; 2) building the Bagpipe tool which automatically checks that BGP configurations adhere to given policy specifications, revealing 19 apparent errors in three ASes with over 240,000 lines of BGP configuration; and 3) testing the BGP simulator C-BGP, revealing one bug.
-
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. -
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. -
Student Pitches
- Coffee Break
- ... together networking and PL will roar
-
Symbolic Execution — Model Equivalence & Applications
Matei Popovici, Radu Stoenescu, Lorina Negreanu, Costin Raiciu (University Politehnica of Bucharest)
Abstract: Symbolic execution has been applied to network dataplane code (e.g. middlebox C code), to capture a series of interesting bugs - however it does not scale very well, with verification times in the order of minutes to hours per box. Thus, all symbolic execution papers use models instead of the real code to perform symbolic execution in reasonable time; There is one downside: models may be written at different abstraction levels and offer no strong guarantees that the model is a faithful representation of the real code. We present a possible solution which essentially relies on verifying model equivalence.
-
Monitoring as a Design Target for Programmable Switches
Rodrigo Fonseca (Brown University)
Abstract: Despite much recent progress on static network verification, dynamic monitoring of network properties remains a vital approach to detecting (and gaining insight into) incorrect network behavior. In this talk we look at dynamic monitoring of stateful properties on switches. In particular, we focus on cross-packet and cross-flow notions of correctness that not only require state on the switches, but also interact in subtle ways with other switch features. Through examples, we examine current proposals for stateful primitives on programmable switches; we argue that the requirements of monitoring cross-packet properties differ from typical packet forwarding, and should inform the design of future switch primitives. -
Closing Remarks
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.
Invited Speakers
- Confirmed Invited Speakers
-
Changhoon Kim
Barefoot Networks, USA
-
Haoyu Song
Huawei, USA
-
Yinben Xia
Huawei, China
Sponsors
Important Dates
-
April 29, 2016Deadline -
May 9, 2016Speaker notified -
June 8, 2016Travel grant applications due -
August 22, 2016
Workshop day
Organizers
- Workshop Co-Chairs
