Formalize Dequeue-Side Semantics

enq-deq-equiv/refs.bib

@@ -0,0 +1,9 @@
+@misc{OG,
+      title={Formal Abstractions for Packet Scheduling}, 
+      author={Anshuman Mohan and Yunhe Liu and Nate Foster and Tobias Kappé and Dexter Kozen},
+      year={2023},
+      eprint={2211.11659},
+      archivePrefix={arXiv},
+      primaryClass={cs.NI},
+      url={https://arxiv.org/abs/2211.11659}, 
+}

enq-deq-equiv/sched_trans/pifo/z_post-pop.pseudo

@@ -0,0 +1,11 @@
+def z_post-pop(st, pkt):
+    f = flow(pkt)
+    turn = int(s["turn"])
+    i = turn
+    while i != f:
+        st["r_" + str(i)] += n
+        i = (i + 1) % n
+    st["turn"] = float((f + 1) % n)
+    if turn >= st["turn"]:
+        st["cycle"] += 1
+    return st

enq-deq-equiv/sched_trans/pifo/z_pre-push.pseudo

@@ -0,0 +1,7 @@
+def z_pre-push(st, pkt):
+    r = arrival_time(pkt)
+    f = flow(pkt)
+    rank_ptr = "r_" + str(f)
+    r_i = int(st[rank_ptr])
+    st["rank_ptr"] += float(n)
+    return ((f, r_i) :: r, st)

enq-deq-equiv/sched_trans/rio/z_post-pop.pseudo

@@ -0,0 +1,4 @@
+def z_post-pop(st, pkt):
+    f = flow(pkt)
+    st["turn"] = float((f + 1) % n)
+    return st

enq-deq-equiv/sched_trans/rio/z_pre-pop.pseudo

@@ -0,0 +1,7 @@
+def z_pre-pop(st):
+    turn = int(s["turn"])
+    rs = []
+    for i in range(n):
+        # Python %, e.g. -2 % 3 == 1, not -2
+        rs.append((i - turn) % n)
+    return Internal(rs, [Leaf] * n)

enq-deq-equiv/sched_trans/rio/z_pre_push.pseudo

@@ -0,0 +1,2 @@
+def z_pre-push(st, pkt):
+    return arrival_time(pkt)