Mutating state at dequeue

[polybeandip]

This is a mirror of this slack thread, made so there's a paper trail for this decision.

Currently, we model scheduling algorithms via Definition 3.7 of Formal Abstraction. Here, a scheduling algorithm is a triple $(s, q, z)$, where $s \in \mathrm{St}$ is our state, $q$ is our PIFO tree with topology $t$, and $z$ is a map $\mathrm{St} \times \mathrm{Pkt} \to \mathrm{Path}(t) \times \mathrm{St}$. The scheduling transaction $z$ runs only when the switch first encounters a packet, before it's pushed into $q$. This is our only chance to update state!

How would folks feel about modifying the formalism to allow updating state at dequeue as well? More precisely, we call $\mathrm{pop}$ and then update state depending on what packet we've received. In math land, this would amount to defining a control as a quadruple $(s, q, z_{\mathrm{in}}, z_{\mathrm{out}})$, where $s$ and $q$ remain the same, $z_{\mathrm{in}}$ is the scheduling transaction from before (previously called $z$), and $z_{\mathrm{out}}$ is a new map $\mathrm{St} \times \mathrm{Pkt} \to \mathrm{St}$. In this model, $z_{\mathrm{in}}$ would run before $\mathrm{push}$, and $z_{\mathrm{out}}$ would run after $\mathrm{pop}$.

This tweak to $\mathrm{Control}(t)$ is motivated by our implementation for n-flow, round-robin policies on a one-level n-ary tree.

[polybeandip]

@anshumanmohan gave me a green light over slack! Still, I have concerns.

In his SIGCOMM 2016 talk (3:18 - 5:17) on Programmable Packet Scheduling at Line Rate (the OG PIFO paper), Sivaraman stresses the importance of minimizing logic on the dequeue side, instead advocating for programmable logic to be placed at enqueue. This appears to be a key design decision behind PIFOs. I worry our $z_{\mathrm{out}}$ might be a step in the wrong direction since it goes against this philosophy.