Operational Semantics For Rio

[KabirSamsi]

Operational Semantics For Rio

Overview

We define Big-Step Operational Semantics For push and pop given a program and a series of queues. For each possible policy constructor form, we will define a new stepping rule.

We operate with the notion of a state tuple, defined as follows:

$$\text{state} = \text{prog} * \text{queue list}$$

Packets. Later on will motivate the need to express that popping a queue may or may not return a packet (in the case that the queue is empty). To this effect, we treat packets as options – that is to say, they may be either None or Some pkt.

Pushing and Popping. Essentially, calling push or pop (with any relevant info) on a state tuple should allow us to mutate the queues based on the program. Exactly how the mutate depends on the program, hence the need for multiple semantic rules.

The nature of how queues work isn't too relevant – we assume they are equipped with the following opaque functions:

$$\text{PUSH} : \text{ pkt} * \text{queue} \rightarrow \text{queue}$$

$$\text{POP } : \text{ queue} \rightarrow \text{pkt option} * \text{queue}$$

Subsequently, we can define push and pop by signature:

$$\text{push} : \text{ pkt} * \text{ queue } * \text{state} \rightarrow \text{state}$$

$$\text{pop} : \text{state} \rightarrow \text{ pkt option} * \text{state}$$

Semantics

Push Semantics

Assume that at enqueue-time, we have a packet with a known destination queue. We also are given a program, though its structure is irrelevant beyond ensuring a well-defined state tuple. Subsequently, we can define push:

$$\frac{p \in \text{Prog} \hspace{0.5cm} qs \subseteq \text{Queue} \hspace{0.5cm} q \in qs \hspace{0.5cm} pkt \in \text{Pkt} \hspace{0.5cm} \text{PUSH } (pkt, q) \Downarrow q'}{\text{push } (pkt, q, (p, qs)) \Downarrow (p, qs[q'/q])}\text{PUSH}$$

---

Pop Semantics of Set-To-Stream Transformers

Helpers. We assume that queues and packets are equipped with a few opaque functions that work as follows.

We define flush : queue -> pkt set. This returns all packets currently enqueued in a given queue.

We define a totally-ordered type t. In other words, any set of elements $\{e_1 \dots e_n\}$ such that e1 : t ... en : t are totally ordered.

We then denote the functions rank : pkt -> t, slack : pkt -> t., weight : pkt -> t, each of which respectively takes a packet and returns a totally-ordered ranking corresponding to some property of the packet. We also assume these functions map packets such that if None -> e1 and Some d -> e2, then $e2 \leq e1$.

We define a higher-order function hd : (pkt -> t ) -> queue -> pkt:

$$\frac{\hspace{0.5cm} \text{flush } q = \{pkt_1 \dots pkt_n\} \hspace{0.5cm} \text{f : pkt} \rightarrow \text{t} \hspace{0.5cm} \forall 1 \leq i \leq n. pkt_i = \text{ None }}{\text{hd f } q = \text{ None}}\text{HD-NONE}$$

$$\frac{\hspace{0.5cm} \text{flush } q = \{pkt_1 \dots pkt_n\} \hspace{0.5cm} \text{f : pkt} \rightarrow \text{t} \hspace{0.5cm} \exists 1 \leq i \leq n. (\forall 1 \leq j \leq n. \text{ f } pkt_i \leq \text{f } pkt_j)) }{\text{hd f } q = pkt_i}\text{HD-SOME}$$

And define a higher-order function heads : (pkt -> t) -> queue list -> pkt list:

$$\frac{qs \subseteq \text{Queue}\hspace{1cm} \text{f}:\text{pkt} \rightarrow \text{t} \hspace{1cm} \forall 1 \leq i \leq n. \text{ } \text{hd f } qs_i = pkt_i}{\text{heads f qs} = \{pkt_1 \dots pkt_n \}}\text{HEADS}$$

In a sense, heads performs the higher-order map with hd on a list of queues.

Subsequently, we can define a general popping rule POP-GEN (with HOF popg) for set-to-streams:

$$\frac{qs \subseteq \text{Queue}\hspace{0.5cm} \text{f}:\text{pkt} \rightarrow \text{t} \hspace{0.5cm} \text{heads f qs} = {pkt_1 \dots pkt_n} \hspace{0.5cm} \exists 1 \leq i \leq n. (\forall 1 \leq j \leq n. \text{f } pkt_i \leq \text{f } pkt_j)}{\text{popg f qs} = (pkt_i, qs[qs_i/pkt_i])}\text{POP-GEN}$$

(Where $qs[qs_i/pkt_i]$ denotes $qs$, but with $qs_i$ having $pkt_i$ removed).

Subsequently, giving the trio of operational semantics for popping from FIFOs, EDFs and SJNs:

$$\frac{s \in \text{Set} \hspace{1cm} qs \subseteq \text{Queue}\hspace{1cm} \text{popg rank } qs = (pkt_i, qs')}{\text{pop}(\text{FIFO}(s), qs) \Downarrow (pkt_i, (p, qs'))}\text{POP-FIFO}$$

$$\frac{s \in \text{Set} \hspace{1cm} qs \subseteq \text{Queue} \hspace{1cm} \text{popg slack } qs = (pkt_i, qs')}{\text{pop}(\text{EDF}(s), qs) \Downarrow (pkt_i, (p, qs'))}\text{POP-EDF}$$

$$\frac{s \in \text{Set} \hspace{1cm} qs \subseteq \text{Queue} \hspace{1cm} \text{popg weight } qs = (pkt_i, qs')}{\text{pop}(\text{SJN}(s), qs) \Downarrow (pkt_i, (p, qs'))}\text{POP-SJN}$$

---

Helpers For Stream-To-Stream Transformers

The key with rigorously defining stream-to-stream transformers is that we need some way to figure out how to partition queues when popping, in order to lock down which partitioning of queues are involved with each recursive call.

To do so, we define nclasses and a series of semantics, allowing us to find the number of classes defined under a policy:

$$\frac{c \in \text{ Class}}{\text{nclasses } c = 1}\text{ NCLASSES-CLSS}$$

$$\frac{c_1 \dots c_n : \textbf{set} \hspace{1cm} \forall 1 \leq i \leq n. \text{ numclasses } c_i = n_i}{\text{nclasses } Union(c_1 \dots c_n) = \sum_{i=1}^n n_i}\text{NCLASSES-UNION}$$

$$\frac{c : \text{set} \hspace{1cm} \text{nclasses } c = n}{\text{nclasses} \text{FIFO d}(c) = n}\text{ NCLASSES-FIFO}$$

$$\frac{c : \text{set} \hspace{1cm} \text{nclasses } c = n}{\text{nclasses} \text{EDF }(c) = n}\text{ NCLASSES-EDF}$$

$$\frac{c : \text{set} \hspace{1cm} \text{nclasses } c = n}{\text{nclasses} \text{SJN }(c) = n}\text{ NCLASSES-SJN}$$

$$\frac{p_1 \dots p_n : \textbf{stream} \hspace{1cm} \forall 1 \leq i \leq n. p_i : \textbf{stream}, \text{numclasses} pi = n_i \hspace{1cm} \forall 1 \leq i \leq n. \text{ numclasses } p_i = n_i}{\text{nclasses } RoundRobin({p_1 \dots p_n}) = \sum_{i=1}^n n_i}\text{NCLASSES-RR}$$

$$\frac{p_1 \dots p_n : \textbf{stream} \hspace{1cm} \forall 1 \leq i \leq n. \text{ numclasses } p_i = n_i}{\text{nclasses } Strict({p_1 \dots p_n}) = \sum_{i=1}^n n_i}\text{NCLASSES-STRICT}$$

$$\frac{p_1 \dots p_n : \textbf{stream} \hspace{1cm} \forall 1 \leq i \leq n. \text{ numclasses } p_i = n_i}{\text{nclasses } WFQ({p_1 \dots p_n}, {w_1 \dots w_n}) = \sum_{i=1}^n n_i}\text{NCLASSES-WFQ}$$

We then dictate rules to partition and merge queues based on the rules of substreams such that we can have well-defined rules:

$$\frac{ks = (k_1 \dots k_n) \hspace{1cm} \sum_{i=1}^n k_i = |qs| \hspace{1cm} \forall 1 \leq i \leq n. |q'_i| = k_i }{\text{partition}(qs, ks) = (q'_1 \dots q'_n)} \text{PARTITION}$$

This equips us to then define semantics for stream-to-stream popping.

Pop Semantics of Stream-To-Stream Transformers

Round-Robin

Though we had previously asserted that programs will not change with a big-step, we can tweak the structure of a Round-Robin program to good effect, giving the following rule:

$$\frac{\forall 1 \leq i \leq n. p_i : \textbf{stream} \land \text{numclasses } p_i = k_i. \hspace{1cm}\text{partition }(qs, (k_1 \dots k_n)) = (q_1 \dots q_n) \hspace{1cm}\text{pop}(p_1, q_1) \Downarrow (pkt, (p_1', q_1'))}{\text{pop}(\text{RR}(p_1, p_2 \dots p_n), qs) \Downarrow (pkt, \text{RR}(p_2 \dots p_n, p_1'), \text{merge} (q_2 \dots q_n, q_1'))}\text{POP-RR}$$

Essentially, we orchestrate pop on the first stream child, return that packet, modify the queues, and then move that stream to the end. This formalizes the 'one-per-round' round-robin effect.

Strict Queueing

This is the primary case where we are concerned about whether packets are None or Some. We utilize the optionality to formalize the network-y notion of a stream 'falling silent'.

Strategy. We can develop two inference rules. Once dictates that if every sub-stream pops None, the result of popping from the current stream transformer is None as well. The other finds the first sub-stream for which Some is returned, and returns that as the popping result.

In the first case, we consider the situation where every stream has fallen silent. In this case, the resultant strict stream must as well:

$$ \frac{\forall 1 \leq i \leq n. p_i : \textbf{stream} \land \text{numclasses } p_i = k_i. \hspace{1cm}\text{partition }(qs, (k_1 \dots k_n)) = (q_1 \dots q_n) \hspace{1cm}\forall 1 \leq i \leq n. \text{pop}(p_i, q_i) \rightarrow (\text{None}, (p_i, q_i))}{\text{pop}(\text{Strict}(p_1 \dots p_n), qs) \rightarrow (\text{None}, \text{Strict}(p_1 \dots p_n), qs)}\text{POP-STRICT-NONE} $$

In the second case, we find the first non-silent stream, and return its packet and modified program/queue. It results in the slightly wordy rule:

$$ \frac{ \forall 1 \leq i \leq n. p_i : \textbf{stream} \land \text{numclasses } p_i = k_i. \hspace{1cm}\text{partition }(qs, (k_1 \dots k_n)) = (q_1 \dots q_n) \hspace{0.5cm}\exists 1 \leq i \leq n. (\forall 1 \leq j < i. \text{pop}(p_j, qj) \rightarrow (\text{None}, (p_j, q_j)) \land \text{pop}(p_i, qi) \rightarrow (\text{Some } pkt, (p_i', q_i')))}{\text{pop}(\text{Strict}(p_1 \dots p_n), qs) \rightarrow (\text{Some } pkt, \text{Strict}((p_1 \dots p_n)[p_i'/p_i]), \text{merge} (q_1 \dots q_n)[q_i'/q_i])}\text{POP-STRICT-EXISTS} $$

Weighted-Fair-Queueing

WFQ Programs contain both a list of sub-streams, and a list of weights, which we type as integers.

With this in mind, we can design four big-stepping rules, each one contingent on the possible program setup.

We'll once again utilize the notion of program modification in state-to-state stepping. We'll also enforce that weights must be positive integers $\geq 1$, and that the number of weights should be either the same length as, or one more than, the number of sub-streams.

Important Note. Round-Robin is just WFQ with all the weights set to $1$. We'll use this notion as we define the semantics.

Strategy. With each iteration, cache the current weight by adding it to the end of the list, and then decrease the weight by one. Once the head's weight reaches 1, we pop the element and step to a state where the remaining $n$ elements of the tail form the new weights. Subsequently, after a full pass, we end up at the same state of programs and weights as initially, giving the desired effect.

Case 1. Let $a_1 = 1$ (Denoting the first weight) and let $m$ (Number of weights) $= n$ (Number of sub-streams).

$$\frac{ \forall 1 \leq i \leq n. p_i : \textbf{stream} \land \text{numclasses } p_i = k_i. \hspace{1cm}\text{partition }(qs, (k_1 \dots k_n)) = (q_1 \dots q_n) \text{pop}(p_1, q_1) \hspace{0.5cm} \Downarrow (pkt, (p_1', q_1')) \hspace{0.5cm} a_1 = 1 \hspace{0.5cm} m=n}{\text{pop}(\text{WFQ}((p1 \dots p_n), (a_1, a_2 \dots a_m)), qs) \Downarrow (pkt, \text{WFQ}((p_2 \dots p_n, p_1'), (a_2 \dots a_n, a_1)), \text{merge}(q_2 \dots q_n, q_1'))}\text{POP-WFQ-1}$$

The implication is then that we have just started a new round, with a weight of $1$. We cache the head value at the end, and pop from the front. This is effectively just performing pop on a Round-Robin policy.

Case 2. Let $a_1 &gt; 1$, and let $m = n$.

$$ \frac{ \forall 1 \leq i \leq n. p_i : \textbf{stream} \land \text{numclasses } p_i = k_i. \hspace{1cm}\text{partition }(qs, (k_1 \dots k_n)) = (q_1 \dots q_n) \hspace{0.5cm} \text{pop}(p_1, q_1) \Downarrow (pkt, (p_1', q_1')) \hspace{0.5cm} a_1 > 1 \hspace{0.5cm} m=n}{\text{pop}(\text{WFQ}((p1 \dots p_n), (a_1 \dots a_m)), qs) \Downarrow (pkt, \text{WFQ}((p_1' \dots p_n), (a_1-1\dots a_m, a_1)), \text{merge}(q_1' \dots q_n)}\text{POP-WFQ-2}$$

The implication is then that we have just started a new round. We cache the head value at the end (thereby getting $m = n+1$), and subtract from the front.

Case 3. Let $a_1 = 1$, and let $m = n+1$.

$$\frac{ \forall 1 \leq i \leq n. p_i : \textbf{stream} \land \text{numclasses } p_i = k_i. \hspace{1cm}\text{partition }(qs, (k_1 \dots k_n)) = (q_1 \dots q_n) \hspace{0.5cm} \text{pop}(p_1, q_1) \Downarrow (pkt, (p_1', q_1')) \hspace{0.5cm} a_1 = 1 \hspace{0.5cm} m=n+1} {\text{pop}(\text{WFQ}((p_1 \dots p_n), (a_1, a_2 \dots a_m)), qs) \Downarrow (pkt, \text{WFQ}((p_1' \dots p_n), (a_2 \dots a_m)), \text{merge}(q_1' \dots q_n)}\text{POP-WFQ-3}$$

Pop as normal, and then remove the head (thereby getting $m = n$). The cached value is already at the end, so will loop around.

Case 4. Let $a_1 &gt; 1$, and let $m = n+1$.

$$\frac{ \forall 1 \leq i \leq n. p_i : \textbf{stream} \land \text{numclasses } p_i = k_i. \hspace{1cm}\text{partition }(qs, (k_1 \dots k_n)) = (q_1 \dots q_n) \hspace{0.5cm} \text{pop}(p_1, q_1) \Downarrow (pkt, (p_1', q_1')) \hspace{0.5cm} a_1 > 1 \hspace{1cm} m=n+1}{\text{pop}(\text{WFQ}((p1 \dots p_n), (a_1 \dots a_m)), qs) \Downarrow (pkt, \text{WFQ}((p_1' \dots p_n), (a_1-1\dots a_m)), \text{merge}(q_1' \dots q_n))}\text{POP-WFQ-4}$$

All we need to do here is subtract $1$ from the head weight, and pop as normal. The cached value is already at the end.

[KabirSamsi]

OCaml implementation under directory 'semantics' on branch operational-semantics (also #70, draft PR)

Note: WFQ needs some updating.

[anshumanmohan]

Near the top you have the following

$$\text{push} : \text{ pkt} * \text{ queue } * \text{state} \rightarrow \text{state}$$

but do you mean the following?

$$\text{push} : \text{ pkt} * \text{state} \rightarrow \text{state}$$

EDIT: oh never mind, on reading further I see that you use that second field to identify the destination queue.

[KabirSamsi]

The queue in the triple comes from the fact that I'm relying on flow inference to tell us which queue a packet needs to be pushed to. Hence why all three arguments are needed.