Formal Abstractions for Packet Scheduling

TL;DR

This paper formalizes the semantics of PIFO trees for programmable packet scheduling in SDN, enabling topology-independent implementation and optimization through compilation and simulation.

Contribution

It introduces a formal operational model for PIFO trees, along with compilation algorithms and a simulator, advancing understanding and practical deployment of programmable packet scheduling.

Findings

Formal semantics for PIFO trees established

Compilation algorithms enable topology-independent implementation

A simulator demonstrates PIFO tree behavior on various algorithms

Abstract

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.