Anshuman Mohan: "Formal Abstractions for Packet Scheduling"
*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. However, the semantic properties of PIFO trees are not well understood.
This work 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. This is especially exciting because it opens the doors to real hardware deployment: switch manufacturers can bake some single tree topology into their devices, and yet allow network administrators to program their schedulers against a range of tree topologies.
*Bio*:
Anshuman Mohan is a third-year PhD student at Cornell. His research is in programming languages, and he enjoys applying PL techniques to challenges in computer systems. https://www.cs.cornell.edu/~amohan/
*Link to paper*: https://dl.acm.org/doi/10.1145/3622845
*Zoom*: https://mit.zoom.us/j/94354302263
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. However, the semantic properties of PIFO trees are not well understood.
This work 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. This is especially exciting because it opens the doors to real hardware deployment: switch manufacturers can bake some single tree topology into their devices, and yet allow network administrators to program their schedulers against a range of tree topologies.
*Bio*:
Anshuman Mohan is a third-year PhD student at Cornell. His research is in programming languages, and he enjoys applying PL techniques to challenges in computer systems. https://www.cs.cornell.edu/~amohan/
*Link to paper*: https://dl.acm.org/doi/10.1145/3622845
*Zoom*: https://mit.zoom.us/j/94354302263