Formal Abstractions for Packet Scheduling

Anshuman Mohan*, Yunhe Liu*, Nate Foster*, Tobias Kappé*, Dexter Kozen*

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review


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.
Original languageEnglish
Article number269
Pages (from-to)1338-1362
Number of pages25
JournalProceedings of the ACM on Programming Languages
Issue numberOOPSLA2
Publication statusPublished - 16 Oct 2023


Dive into the research topics of 'Formal Abstractions for Packet Scheduling'. Together they form a unique fingerprint.

Cite this