appendix.tex

\section{Appendix for \S2.2}

In the following, we prove a few simple lemmas, which show that $i)$ the dependency forest is correct and $ii)$ minimal in the sense that if any node switches to the new rule before the parent in the dependency forest says so, a packet might be experiencing a loop.

\begin{lemma}\label{lemma:invariant} The invariant of the algorithm is that the current rules in the network are without loops.
\end{lemma}

\begin{proof} The invariant is true at the beginning, since no new rule is included, and the old rules form an in-tree to the destination $d$. The invariant remains true when a node enters the limbo state (uses both old and new rules) as we check at this stage that no loop is introduced when doing so. Finally, the invariant is true as well when a node enters the new state: As this only removes an old rule, no loop can be introduced.
\end{proof}

\begin{lemma}\label{lemma:loop-free} The dependency forest is loop-free.
\end{lemma}

\begin{proof} As the parent of a child must be in the dependency forest already when the child enters the dependency forest, there cannot be loops in the dependency forest.
\end{proof}

\begin{lemma}\label{lemma:forest} At the end, every node (but the destination $d$) is in the dependency forest.
\end{lemma}

\begin{proof} As long as there are nodes in limbo state, we will move them to the new state, one after the other, possibly moving other nodes from old to limbo when removing the old pointers. Assume, for the sake of contradiction, that the process halts prematurely, i.e. that no node remains in the limbo state and some nodes are stuck in the old state. Then there must be a node in old which qualified for limbo at an earlier stage, when its parent in the dependency forest moved to new. We can find this node as follows: Start from an arbitrary old node, and move along the new rules towards the destination $d$. Since the destination is (by definition) new, along this new-rules path, there must be a last pair of nodes $c,p$, where $c.new = p$, $c$ and $p$ are in state old and new, respectively. By Lemma \ref{lemma:invariant} we know that we currently do not have a loop. Adding the new pointer of node $c$ does not introduce a loop, as $c.new$ points to a path of new nodes which cannot introduce a loop. Hence node $c$ was eligible for state limbo -- we have a contradiction!
\end{proof}

%old example which is bogus: Note that there are networks where this jumping mechanism is necessary. Example: A network with three nodes, where $u.old = v$, $u.new = d$, $v.old = d$, and $v.new = u$. Either of the nodes $u,v$ cannot enter the limbo state, as there will be a loop between $u$ and $v$.

\begin{lemma}\label{lemma:correctness} The process is correct (and produces no loops).
\end{lemma}

\begin{proof} The follows directly from Lemmas \ref{lemma:invariant}, \ref{lemma:loop-free} and \ref{lemma:forest}.
\end{proof}

\begin{lemma}\label{lemma:minimal} The process is minimal.
\end{lemma}

\begin{proof}
Root nodes in the dependency forest can flip to the new rule immediately, and are as such by definition optimal. A node $c$ is a child of a parent node $p$ in the dependency forest, exactly because $c$ can only use its new rule after $p$ removed its old rule. As such, the process guaranteed that $c$ was added to the dependency tree at the earliest possible (minimal) time.
\end{proof}

\section{Appendix for \S3}
\label{sec:app2}


\begin{lemma}\label{lemma:imp loop-free} Loop freedom depends on other nodes.
\end{lemma}

\begin{proof}
In the example in Figure \ref{fig:example}, node $x$ depends on node $y$.
\end{proof}

\begin{lemma}\label{lemma:imp packet coherence} Packet coherence depends on all non-trivial downstream switches.
\end{lemma}

\begin{proof} Let $u$ be a switch router that is non-trivial, in the sense that $u$ is affected by a rule change, i.e. $u$'s old rule differs from its new rule. If the source starts to route packets according to the new rule, the switch $u$ will forward the packets wrongly, or drop them, which is not packet coherent.
\end{proof}

\begin{lemma}\label{lemma:imp bandwidth limit} Bandwidth limit potentially depends on all switches.
\end{lemma}

\begin{proof} Let $f$ be a flow that wants to use a new path $p$, or increase its capacity on an existing path. The network may be able to adapt to flow $f$, however, in general only if other flows use different paths as well, which in turn may (recursively) move even other flows (some of which have no single switch/link in common with the new path $p$). As such, any $f$ may potentially depend on any single switch in the network.
\end{proof}

Note that, in some networks and applications, one may be able to implement bandwidth limit with less dependencies.