SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Fri 27 Oct 2023 11:54 - 12:12 at Room I - verification 1 Chair(s): Gowtham Kaki

Early programming models for software-defined networking (SDN) focused on basic features for controlling network-wide forwarding paths, but more recent work has considered richer features, such as packet scheduling and queueing, that affect performance. In particular, PIFO trees, proposed by Sivaraman et al., offer a flexible and efficient primitive for programmable packet scheduling. Prior work has shown that PIFO trees can express a wide range of practical algorithms including strict priority, weighted fair queueing, and hierarchical schemes. However, the semantic properties of PIFO trees are not well understood.

This paper studies PIFO trees from a programming language perspective. We formalize the syntax and semantics of PIFO trees in an operational model that decouples the scheduling policy running on a tree from the topology of the tree. Building on this formalization, we develop compilation algorithms that allow the behavior of a PIFO tree written against one topology to be realized using a tree with a different topology. Such a compiler could be used to optimize an implementation of PIFO trees, or realize a logical PIFO tree on a target with a fixed topology baked into the hardware. To support experimentation, we develop a software simulator for PIFO trees, and we present case studies illustrating its behavior on standard and custom algorithms.

Fri 27 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
verification 1OOPSLA at Room I
Chair(s): Gowtham Kaki University of Colorado at Boulder
11:00
18m
Talk
Solving Conditional Linear Recurrences for Program Verification: The Periodic Case
OOPSLA
Chenglin Wang Hong Kong University of Science and Technology, Fangzhen Lin Hong Kong University of Science and Technology
DOI
11:18
18m
Talk
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
OOPSLA
Armaël Guéneau Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria, Johannes Hostert ETH Zurich, Simon Spies MPI-SWS, Michael Sammler MPI-SWS, Lars Birkedal Aarhus University, Derek Dreyer MPI-SWS
Link to publication DOI
11:36
18m
Talk
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning
OOPSLA
Noam Zilberstein Cornell University, Derek Dreyer MPI-SWS, Alexandra Silva Cornell University
DOI Pre-print
11:54
18m
Talk
Formal Abstractions for Packet SchedulingDistinguished Paper
OOPSLA
Anshuman Mohan Cornell University, Yunhe Liu Cornell University, Nate Foster Cornell University, Tobias Kappé Open University of the Netherlands; University of Amsterdam, Dexter Kozen Cornell University
Link to publication DOI
12:12
18m
Talk
P4R-Type: A Verified API for P4 Control Plane Programs
OOPSLA
Jens Kanstrup Larsen DTU, Roberto Guanciale KTH Royal Institute of Technology, Philipp Haller KTH Royal Institute of Technology, Alceste Scalas DTU
DOI Pre-print Media Attached