ACM SOSR 2021
October 11 & 12, 2021
Fully Virtual Conference
Home Program Register Call for Papers SOSR Award Anti-Harassment Policy Organizers
Long
Jason Kim, Hyojoon Kim, Jennifer Rexford (Princeton University)
Long
Serhat Arslan, Stephen Ibanez, Alex Mallery, Changhoon Kim, Nick McKeown (Stanford University)
Long
Vineeth Sagar Thapeta, Komal Shinde, Mojtaba Malekpourshahraki, Darius Grassi, Balajee Vamanan, Brent Stephens (University of Illinois at Chicago)
Long
Maria Apostolaki, Ankit Singla, Laurent Vanbever (ETH Zurich)
Long
Ali Fattaholmanan (Università della Svizzera italiana); Mario Baldi (Politecnico di Torino); Antonio Carzaniga (Università della Svizzera italiana); Robert Soulé (Yale University)
Long
Jedidiah McClurg (Colorado School of Mines)
Short/WIP
Nicu Florin Zaicu, Matthew Luckie, Richard Nelson, Marinho Barcellos (University of Waikato)
Long
Feng Tian, Yang Zhang, Wei Ye, Cheng Jin, Ziyan Wu, Zhi-li Zhang (University of Minnesota - Twin Cities)
Short/WIP
Or Goaz, Roy Friedman, Ori Rottenstreich (Technion)
Abstract: P4 is a domain-specific language for specifying the behavior of packet-processing systems. It is based on an elegant design with high-level abstractions, such as parsers and match action pipelines, which can be compiled to efficient implementations in hardware or software. Unfortunately, like many industrial languages, P4 lacks a formal foundation. The P4 specification is a 160-page document with a mixture of informal prose, graphical diagrams, and pseudocode. The reference compiler is complex, running to over 40KLoC of C++ code. Clearly neither of these artifacts is suitable for formal reasoning. This talk will introduce a new framework called Petr4 (pronounced "Petra"), that puts P4 on a solid foundation. Petr4 uses standard elements of the semantics engineering toolkit, namely type systems and operational semantics, to build a compositional semantics that assigns an unambiguous meaning to every P4 program. Petr4 is implemented as an OCaml prototype that has been validated against a suite of over 750 tests from the reference implementation. While developing Petr4, we discovered dozens of bugs in the language specification and the reference implementation, many of which have been fixed. Furthermore, we have used Petr4 to establish the soundness of P4’s type system, prove key properties such as termination, and formalize a language extension.
Long
Zhenyu Zhou (Duke University); Theophilus A. Benson (Brown University); Marco Canini (KAUST); Balakrishnan Chandrasekaran (Vrije Universiteit Amsterdam)
Long
K Shiv Kumar, Ranjitha K, P S Prashanth (Indian Institute of Technology Hyderabad); Mina Tahmasbi Arashloo (Cornell University); Venkanna U. (International Institute of Information Technology, Naya Raipur); Praveen Tammana (Indian Institute of Technology Hyderabad)
Long
Eman Ramadan, Hesham Mekky, Cheng Jin, Braulio Dumba, Zhi-Li Zhang (University of Minnesota - Twin Cities)
Long
Kausik Subramanian, Anubhavnidhi Abhashkumar, Loris D'Antoni, Aditya Akella (University of Wisconsin-Madison)
Short/WIP
Robert MacDavid (Princeton University); Carmelo Cascone, Pingping Lin, Badhrinath Padmanabhan, Ajay Thakur, Larry Peterson (Open Networking Foundation); Jennifer Rexford (Princeton University); Oguz Sunay (Open Networking Foundation)
Long
Yaniv Sadeh (Tel Aviv University); Ori Rottenstreich (Technion - Israel Institute of Technology); Haim Kaplan (Tel Aviv University)
Short/WIP
Hun Namkung, Daehyeok Kim (Carnegie Mellon University); Zaoxing Liu (Boston University); Vyas Sekar, Peter Steenkiste (Carnegie Mellon University)