ACM SIGCOMM 2017, Los Angeles, CA

ACM SIGCOMM 2017 The Third Workshop on Networking and Programming Languages (NetPL 2017)

NetPL 2017

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.

This is the third NetPL workshop, after last year’s workshop at SIGCOMM and the first edition at ECOOP. Talks in the previous editions of the workshop are on YouTube.

Workshop Program

  • Monday, August 21, 2017, Exploration Room (Luskin)

  • 9:15am - 9:40am Opening Remarks

    Session Chair: Nikolaj Bjørner, Marco Canini, Nik Sultana

    Room: Exploration Room (Luskin)

  • 9:40am - 10:30am Session 1

    Room: Exploration Room (Luskin)

  • Programmable Forwarding Planes are Here to Stay

    Nick McKeown

    • Abstract: Many great research ideas and new languages are emerging for programmable forwarding. In this talk, I'll take a step back and consider how we got here, why programmable forwarding planes are inevitable, why now is the right time, why they are a final frontier for SDN, and why they are here to stay.


      Bio: Nick McKeown (PhD/MS UC Berkeley ’95/’92; B.E Univ. of Leeds, ’86) is the Kleiner Perkins, Mayfield and Sequoia Professor of Electrical Engineering and Computer Science at Stanford University, and Faculty Director of the Open Networking Research Center. From 1986-1989 he worked for Hewlett-Packard Labs in Bristol, England. In 1995, he helped architect Cisco's GSR 12000 router. Nick was co-founder and CTO at Abrizio (acquired by PMC-Sierra, 1998), co-founder and CEO of Nemo (“Network Memory”),acquired by Cisco, 2005. In 2007 he co-founded Nicira (acquired by VMware) with Martin Casado and Scott Shenker. Nick is chairman of Barefoot Networks which he co-founded with Pat Bosshart and Martin Izzard in 2013. In 2011, he co-founded the Open Networking Foundation (ONF) with Scott Shenker; and the Open Networking Lab (ON.Lab) with Guru Parulkar and Scott Shenker. Nick is a member of the US National Academy of Engineering (NAE), the American Academy of Arts and Sciences, a Fellow of the Royal Academy of Engineering (UK), the IEEE and the ACM. He received the British Computer Society Lovelace Medal (2005), the IEEE Kobayashi Computer and Communications Award (2009), the ACM Sigcomm Lifetime Achievement Award (2012), the IEEE Rice communications theory award (1999). Nick has an Honorary Doctorate from ETH (Zurich, 2014). Nick's current research interests include software defined networks (SDN), network verification, video streaming, how to enable more rapid improvements to the Internet infrastructure, and tools and platforms for networking research and teaching.


  • 10:30am - 11:00am Coffee Break (Foyer)

  • 11:00am - 12:30pm Session 2

    Room: Exploration Room (Luskin)

  • For Good Measure: Programmable Measurement Using Emerging Switches

    Jennifer Rexford

    • Abstract: Large networks rely on timely and accurate measurements to detect unwanted traffic, diagnose performance problems, and optimize the use of resources. Emerging programmable forwarding planes are a "game changer" for answering sophisticated measurement questions directly inside the network, rather than shipping reams of data to a remote collector for subsequent analysis. Capitalizing on these new switch capabilities requires innovation in rich, high-level query abstractions as well as runtime systems that can generate efficient data structures for streaming analytics at line rate.


      Bio: Jennifer Rexford (PhD/MSE UMichigan '96/'93, BSE Princeton '91) is the Gordon Y.S. Wu Professor of Engineering and the Chair of Computer Science at Princeton University. Before joining Princeton in 2005, she worked for eight years at AT&T Labs–Research. Jennifer is co-author of the book "Web Protocols and Practice" (Addison-Wesley, May 2001). She served as the chair of ACM SIGCOMM from 2003 to 2007, and a member of the Open Networking Foundation board of directors from 2014 to 2017. Jennifer received ACM's Grace Murray Hopper Award (2004) and Athena Lecturer Award (2016). She is an ACM Fellow (2008), and a member of the American Academy of Arts and Sciences (2013) and the National Academy of Engineering (2014).


  • Programming Network Policies by Examples: Platform, Abstraction, and User Studies

    Boon Thau Loo

    • Abstract: NetEgg is a scenario-based programming toolkit that allows network operators to program network policies by describing representative example behaviors. Given these scenarios, a synthesis algorithm automatically infers the controller state that needs to be maintained along with the rules to process network events and update state. NetEgg executes the generated policy implementation on top of a centralized controller, and automatically infers flow-table rules that can be pushed to switches to improve throughput. This talk will present the design and implementation of the NetEgg toolkit, empirical results on multiple example policies, and experiences on running controlled user studies. The talk concludes with a discussion on the importance of controlled user studies in evaluating new programming languages in the networking domain and the lessons we learnt in the process.


      Bio: Boon Thau Loo is an Associate Professor in the Computer and Information Science (CIS) department at the University of Pennsylvania. He holds a secondary appointment in the Electrical and Systems Engineering (ESE) department. He is also the CIS Masters Chair, overseeing all masters programs within the CIS department, and Director of the Master of Science in Engineering in CIS program. He received his Ph.D. degree in Computer Science from the University of California at Berkeley in 2006. Prior to his Ph.D, he received his M.S. degree from Stanford University in 2000, and his B.S. degree with highest honors from UC Berkeley in 1999. His research focuses on distributed data management systems, Internet-scale query processing, and the application of data-centric techniques and formal methods to the design, analysis and implementation of networked systems. He was awarded the 2006 David J. Sakrison Memorial Prize for the most outstanding dissertation research in the Department of EECS at UC Berkeley, and the 2007 ACM SIGMOD Dissertation Award. He is a recipient of the NSF CAREER award (2009) and the Air Force Office of Scientific Research (AFOSR) Young Investigator Award (2012). He has published 100+ peer reviewed publications and has supervised twelve Ph.D dissertations. His graduated Ph.D. students include 3 tenure-track faculty members and winners of 3 dissertation awards. He is also co-founder and Chief Scientist at Termaxia, a big data storage startup.


  • Abstractions for Safety of Stateful Networks

    Mooly Sagiv

    • Abstract:

      Modern networks store states at individual nodes. This allows the forwarding behavior to change over time, which is useful to implement many kinds of functionalities for performance and security. However, this makes the task of network programming hard and error-prone. I will describe several abstractions that simplify the task of proving the safety of stateful networks. The abstraction include modelling state changes as a finite-state machine, ignoring the order of packet receival, and assuming that nodes can non-deterministically reset to their initial states. I will show that these abstractions reduce the asymptotic complexity of network verification.

      This is a joint work with Kalev Alpernas (TAU), Aurojt Panda (UCB), Roman Manevich (BGU), Scott Shenker (UCB), Sharon Shoham (TAU), Yaron Velner (HUJI)


      Bio: Mooly serves as Member of the Advisory Board at Panaya Inc. He is a Senior Member of staff in the Computer Sciences Department School of Mathematical Sciences Tel-Aviv University. A leading scientist in large scale (inter-procedural) program analysis, his fields of interests include Programming Languages, Compilers, Abstract interpretation, Profiling, Pointer Analysis, Shape Analysis, Inter-procedural dataflow analysis, Program Slicing, Language-based programming environments.


  • 12:30pm - 2:00pm Lunch Break (Centennial Terrace)

  • 2:00pm - 3:30pm Session 3

    Room: Exploration Room (Luskin)

  • Verifying networks with symbolic execution and temporal logic

    Matei Popovici, Radu Stoenescu, Lorina Negreanu, Costin Raiciu (University Politehnica of Bucharest)

    • Abstract: We introduce NetCTL, a language designed for expressing and verifying network operator policies. NetCTL can be deployed on arbitrary network infrastructures. It relies on performing symbolic execution on a model of the network at hand in order to prove policy compliance or violation. We have implemented NetCTL verification as an extension to the Symnet symbolic execution engine.


  • Towards An Auditing Language for Preventing Cascading Failures

    Ennan Zhai, Ruzica Piskac (Yale University)

    • Abstract: In this paper, we present the basic ideas behind a framework RepAudit for preventing cascading failures. RepAudit helps administrators to identify potential root causes resulting in cascading failures at an early stage, i.e., before service outages occur. To the best of our knowledge, RepAudit is the first effort capable of simultaneously achieving expressive, efficient, and accurate structural reliability auditing to cloud systems.


  • Network Protocol Programming in Haskell

    Kazuhiko Yamamoto (Internet Initiative Japan Inc.)

    • Abstract: Over seven years, we have developed several network protocol libraries including anti-spam, DNS, HTTP/1.1, HTTP/2 and TLS 1.3 in Haskell. Based on these experiences, we regard Haskell as a safe and highly-concurrent network programming language thanks to its strong type system and lightweight threads (i.e. green threads). This paper describes advantages and disadvantages of Haskell and reports our experiences.


  • Dynamic Compilation and Optimization of Packet Processing Programs

    Gábor Rétvári (Budapest University of Technology and Economics); László Molnár, Gábor Enyedi, Gergely Pongrácz (TrafficLab, Ericsson Research)

    • Abstract: Data plane compilation is a transformation from a high-level description of the intended packet processing functionality to the underlying data plane architecture. Compilation in this setting is usually done statically, i.e., the input of the compiler is a fixed description of the forwarding plane semantics and the output is code that can accommodate any packet processing behavior set by the controller at runtime. Below we advocate a dynamic approach to data plane compilation instead, where not just the semantics but the intended behavior is also also input to the compiler. We point out a handful of runtime optimization opportunities that can be leveraged to improve the performance of custom-compiled datapaths beyond what is possible in a static setting.


  • Toward building memory-safe network functions with modest performance overhead

    Keunhong Lee, Shinae Woo (KAIST); Sanghyeon Seo (Hyperconnect, Inc.); Jihyeok Park, Sukyoung Ryu, Sue Moon (KAIST)

    • Abstract: For the past few decades network functions have evolved much in variety and complexity. Network functions rely heavily on low-level memory management to deliver high performance but such memory management is error-prone. Rust, a recently developed language for safe system programming, aims to support memory-safety with modest performance overhead. In this work we build network functions in Rust, with type-safe guarantees and modest performance overhead.


  • Mapping Programmable Network Packet Pipelines to HMC-Enabled FPGAs

    Jehandad Khan, Peter Athanas (Virgina Tech)

    • Abstract: A higher tier of network packet processing performance can be achieved by augmenting the agility FPGAs offer with the sheer streaming throughput of a Hybrid Memory Cube (HMC). The notion of a programmable data plane specified in a domain-specific language enables the creation of custom protocol and packet operations. This paper presents an effort to map one such domain specific language, namely P4 (Protocol Independent Packet Processing) to an HMC-enabled FPGA platform by using HLS as the intermediate representation. The use of HLS affords productivity advantages as well as enabling a close correlation between the P4 code and the corresponding hardware units required to achieve the functionality. The resulting code leverages the parallel nature of the HMC to yield a packet pipeline capable of delivering 30 million packets per second (Mpps) using only a single HMC channel, which translates to 30 Gbps of data throughput for a Layer-3 router with an average of 128-byte long packets. Demonstrated here, by using 10 HMC user channels, the system is capable of achieving 300 Mpps (or 300 Gbps) of throughput. Comparisons with other P4 to FPGA endeavors, as well as with CPUs and GPUs, indicate that the proposed system achieves equal or higher performance and lower power while enabling much higher table scale and overall system simplicity.


  • 3:30pm - 4:00pm Posters Session + Coffee Break (Foyer)

  • 3:30pm - 4:30pm Posters Session

    Room: Exploration Room (Luskin)

  • 4:30pm - 5:00pm Session 4

    Room: Exploration Room (Luskin)

  • Network Verification in the Real World

    Wenxuan Zhou (Veriflow / UIUC)

    • Abstract:

      Enterprise networks have become complex software artifacts weaving together interdependent devices, protocols, virtualization layers, optimizations, software bugs, and security controls. Yet communication is now critical infrastructure. How can we be sure networks are doing the right thing? The fact is, too often, they aren't. Despite enormous amounts of manual effort, outages and security vulnerabilities are common.

      Can we prove that a network is correct? This is the goal of the emerging area of network verification, which applies ideas of formal methods to network infrastructure. From its recent genesis in the research community, network verification blossomed into a hot area of research and quickly had impact on industry, with startups and hyperscale cloud providers deploying verification technology today. In this talk, we'll briefly review key research advances that influenced industrial verification software. Then, based on experience with production deployments, we will discuss what principles of verification persevered, what surprises we encountered, and how verification is solving problems in the real world. Finally, we will discuss challenging future research directions.


      Bio: Wenxuan Zhou is a software engineer at Veriflow and a Ph.D. student in Computer Science at the University of Illinois at Urbana-Champaign (UIUC), advised by Prof. Matthew Caesar. Her research focuses on network verification and synthesis, with an emphasis on software-defined networks, data centers, and enterprise networks. She received her Bachelor’s degree in Electronic Engineering from Beijing University of Aeronautics and Astronautics, China, and her Master’s degree in Computer Science from UIUC. She co-authored research that led to network verification startup Veriflow, where she serves as one of the original engineers on the core verification team.


  • 5:00pm - 5:15pm Closing

    Room: Exploration Room (Luskin)

Invited Speakers

The program will include invited talks from experts in the field, with an emphasis on encouraging engaging technical discussions amongst the participants.

Our program includes several illustrious speakers:

  • Nick McKeown, Stanford University
  • Jennifer Rexford, Princeton University
  • Mooly Sagiv, Tel Aviv University
  • Boon Thau Loo, University of Pennsylvania
  • Wenxuan Zhou, Veriflow / University of Illinois at Urbana-Champaign


Topics of Interest

We are also soliciting contributions from prospective participants in the form of talk proposals to broaden the research that is discussed at the workshop.

Language-centric research of the following aspects of computer networks is in scope:

  • specification and topology
  • testing and measurement
  • packet/traffic generation
  • packet/traffic analysis
  • security
  • resource availability or control
  • policy languages
  • interoperability between networking-related languages
  • composition of networking-related languages

Practical aspects of languages, particularly if oriented towards solving networking problems, are also in scope:

  • how to model and prototype languages rapidly
  • what semantic structures are best suited to the networking domain

We give no firm guidelines on topics (go wild but stay within scope!), however we particularly seek talks that can provoke thought and discussion.

Contact workshop co-chairs.

Submission Instructions

Submit a position paper of at most 2 pages length, 10-pt font, which will be lightly reviewed by the workshop program chairs.

Paper submission can be done via HotCRP at:

Important Dates

  • March 24, 2017

    Submission deadline

  • April 17, 2017

    Acceptance notification

  • May 31, 2017

    Camera ready deadline

Authors Take Note

The official publication date is the date the proceedings are made available in the ACM Digital Library. This date may be up to TWO WEEKS prior to the first day of your conference. The official publication date affects the deadline for any patent filings related to published work.


  • Workshop Co-Chairs
  • Nikolaj Bjørner

    Microsoft Research

  • Marco Canini


  • Nik Sultana

    University of Cambridge