text:
\section{Safeness}\label{appendix:proofs}

\ignore{
\begin{figure}[h!]
	\centering
	\hspace*{-3.15cm}%
	\begin{tikzpicture}[shorten >=1pt,node distance=2.5cm,on grid,auto]
	\tikzset{every state/.append style={rectangle, rounded corners}}
	\node[state] (Match)  {$Match$};
	\node[state] (Send) [below=of Match] {$Send$};
	\node[state] (Recv) [right=of Send] {$Recv$};
	\node[state] (Add) [above right=4cm and 1cm of Match]  {$Add$};
	\node[state] (Del) [right=of Add] {$Del$};
	\node[state] (Brepl) [above right=1.5cm and 1.2cm of Add]  {$Brepl$};
	\node[state] (Ctrl) [below=of Recv] {$Ctrl$};
	\node[state] (Bsync) [below=1.5cm of Ctrl] {$Bsync$};
	\node[state] (Fwd) [right=of Recv] {$Fwd$};
	\node[state] (NoMatch) [above=of Fwd] {$NoMatch$};

	\path[->,>=latex,gray!30]
	(Add)   	 edge[bend right=30, looseness=1.5]  	node {} 	(Match)
	edge[red!70, thick, bend right=15]  					    node {}	   (Match)
	edge[red!70, thick]  					node {}    (NoMatch)
	edge  														node  {} 	(Match)

	(Del)   	  edge[bend left=30]                           		 node {} 	(Match)
	edge[red!70, thick]  						 node {} 	(Match)
	edge[]  													node {} 	(NoMatch)
	(Match) 	edge[loop left]  									   node {} ()
	edge[bend right=90,looseness=2]  		node {} 	(Recv)
	edge[]  													node {}    (NoMatch)
	(Send)  	edge  														node  {} 	(Match)
	edge  														node  {}   (NoMatch)
	(NoMatch)  edge[bend left=50, looseness=1.6]  	  node {} 	(Ctrl)
	(Ctrl)   		edge[bend right=20]  							node {}   (Fwd)
	edge[bend left=90, looseness=1.4]  	node {} 	(Add)
	edge[out=0,in=-30, looseness=1.4]  node {} 	(Del)
	(Fwd)   	  edge[out=220,in=-150, looseness=1.9]  node {} (Match)
	edge[]  													node {}   (NoMatch)
	edge[]  													node {} (Recv)
	(Bsync) 	edge[out=155,in=-190, out looseness=2.5, in looseness=.5]  	node {} 	(Add)
	edge[out=--30,in=10, out looseness=2.5, in looseness=.3]  	node {} 	(Del)
	edge[out=--25,in=10, out looseness=4.5, in looseness=.3]  	node {} 	(Fwd)
	(Brepl) 	edge[out=175,in=-190, out looseness=1.2, in looseness=1.8]  	node {} 	(Bsync)
	;
	\path[<->,>=latex,gray!30]
	(Add)   edge  														node  {} 	(Brepl)
	(Del)   edge  														node  {} 	(Brepl)
	;
	\end{tikzpicture}
	\captionsetup{width=0.9\textwidth}
	\caption{The graph represents the enabling/disabling relations and is derived directly from the guards and semantics of the transitions. Each node is a set of actions of same type. If two nodes are connected by a grey edge, then there may exist a concrete action in the predecessor node that enables a concrete action in the successor node. If the edge is red then the action in the predecessor node may disable a concrete action in the successor node.}
	\label{graph:depend}
\end{figure}
}

\begin{customlemma}{\ref{lemma:safe}}[Safeness]
	For an SDN network model $\mathcal{M}_{(\lambda,\textsc{cp})}  = (S, A, \hookrightarrow, s_0, AP, L)$ and context {\sc ctx}~$=(${\sc cp},~$\lambda,~\varphi)$ with $\varphi\in \text{LTL}_{ \setminus \{\bigcirc \}}$,

	\[\alpha \in A  \text{ is safe   }\iff  \bigwedge\nolimits^3_{i=1} \mathit{Safe}_i(\alpha)  \]
	where $\mathit{Safe}_i$, given in Table \ref{tab:safeness}, are per-row.
\end{customlemma}

\begin{proof}
To show safety we need to show two properties: \emph{independence} (action is independent of any other action) and \emph{invisibility} w.r.t.\ the context, in particular controller program, topology function and formula $\varphi$.

\paragraph{Independence:}
Recall that two actions $\alpha$ and $\beta \neq \alpha$ are independent iff for any state $s$ such that $\alpha\in A(s)$ and $\beta\in A(s)$:
\begin{enumerate}
\item $\alpha \in A\big(\beta(s)\big)$ and $\beta\in A\big(\alpha(s)\big)$
\item $\alpha\big(\beta(s)\big)=\beta\big(\alpha(s)\big)$
\end{enumerate}
(1): It can be easily checked that no safe action disables any other action, nor is any safe action disabled by any other action, so the first condition of independence holds.
\\
(2): For any safe action $\alpha$ and any other action $\beta$ we can assume already that they meet Condition (1). Let us perform a case analysis on $\alpha$:

\ignore{
	\begin{table}[h!]
	\begin{center}
		\caption{Actions and their effect on state}
		\label{tab-access}
		\begin{minipage}{\linewidth}
			\centering
			\begin{tabular}{l|l|l}
				\toprule
				\textbf{Action} & \textbf{Dequeues} & \textbf{Enqueues/Updates}\\
				$\alpha$& \textbf{from}  & \textbf{into} \\
				\midrule
				$send(h,pk)$ & & $\lambda(h).\boldsymbol{pq}$\\
				$recv(h,pk)$&$h.\boldsymbol{pq}$& \\
				$match(sw,pk,r)$ \footnote{In our model the $(0,\infty)$-abstraction is built-in only for the packet queues of the switches. Hence, packets are actually never dequeued.}  & & $D.\boldsymbol{pq}$, with $D \subseteq Hosts \cup Switches$\footnote{$D$ is defined by the topology function $\lambda$ with input $(sw,\{r.forwarding\_ports\})$.}\\
				$nomatch(sw,pk)$ & & $\boldsymbol{rq}$\\
				$ctrl(sw,pk,cs)$  & $\boldsymbol{rq}$ & $sw.\boldsymbol{fq}, Sw.\boldsymbol{cq}, \boldsymbol{cs}$, with $Sw \subseteq Switches$\footnote{$Sw$ is defined according to the controller program at stake.} \\
				$fwd(sw,pk,ports)$&  $sw.\boldsymbol{fq}$& $D.\boldsymbol{pq}$, with $D \subseteq Hosts \cup Switches$\footnote{$D$ is defined by the topology function $\lambda$ with input $(sw,\{ports\})$.}\\
				$add(sw,r)$& $sw.\boldsymbol{cq}$ & $sw.\boldsymbol{ft}$\\
				$del(sw,r)$& $sw.\boldsymbol{cq}$, $sw.\boldsymbol{ft}$ & \\
				$brepl(sw,xid)$ & $sw.\boldsymbol{cq}$& $\boldsymbol{brq}$\\
				$bsync(sw,xid,cs)$ & $\boldsymbol{brq}$ & $sw.\boldsymbol{fq}, Sw.\boldsymbol{cq}, \boldsymbol{cs}$, with $Sw \subseteq Switches$\\
				\bottomrule
			\end{tabular}
		\end{minipage}
	\end{center}
\end{table}
}

 \begin{itemize}[label=$\blacktriangleright$]
 	\item $\alpha$ is either \emph{brepl}, \emph{recv} or \emph{fwd}:\\
	To show that any interleaving with any action $\beta \neq \alpha$ leads to the same state, we observe that the changes of packet queues by these actions

	do not interfere with each other.
 	In cases where a packet is removed from a queue by $\alpha $ (e.g.\ $\alpha = \mathit{recv(h,pkt)}$ removes from $\mathit{h.rcvq}$) but then inserted into the same queue by $\beta$ (e.g.\ $\beta = \mathit{fwd(sw,pkt,ports)}$ where $\mathit{h \in \lambda(sw,ports)}_1$), there is no conflict either, as both actions must have been enabled in the original state in the first place. So no conflicts arise for those $\alpha$.
 	\item $\alpha$ is $\mathit{ctrl(pkt,cs)}$:
 	\begin{itemize}
 		\item If $\beta$ is not a \emph{ctrl} or \emph{bsync} action, then the same argument as above holds.
 		\item The interesting cases occur when $\beta$ is in $\{\mathit{ctrl(\cdot), bsync(\cdot)}\}$.
 		\ignore{
 		Either the controller is insensitive to the order of any two \emph{ctrl} actions $\alpha$ and $\beta$ and we are done, or it is sensitive to some packets, but then from \emph{Safe}$_2(\alpha)$ in Table~\ref{tab:safeness}
		 we know that $\alpha$ with given $pkt$ and $\beta$ with given $\mathit{pkt'}$, respectively, have no effect on the given controller state.
		}
From \emph{Safe}$_2(\alpha)$ we know that {\sc cp} is not order-sensitive, which implies that $\alpha$ and $\beta$ are independent.
Order-insensitivity is a relatively strong condition but it ensures correctness of the lemma and thus partial order reduction.\footnote{Generalisations by a more clever analysis of the controller program are a future research topic.} Thus any interleaving of $\alpha$ and $\beta$ leads to the same state.

 	\end{itemize}
 \item $\alpha$ is $\mathit{bsync(sw,xid,cs)}$:\\
The same line of argument applies as for $\mathit{ctrl(pkt,cs)}$, simply exchanging the roles of $\alpha$ and $\beta$.
 \end{itemize}

 \paragraph{Invisibility}:
 We show this for all safe actions separately:
 \begin{itemize}

 \item $\alpha = \mathit{ctrl(pk,cs)}$.
 The only variables $\alpha$ can change are the $\mathit{controller.rq}$, $\mathit{sw'.fq}$, $\mathit{sw'.cq}$ (for some switches $\mathit{sw'}$), and the control state $\mathit{cs}$. The first three can not appear in $\varphi$ due to the definition of the specification language. In case the control state changes, $\alpha$ is invisible to $\varphi$ because \emph{Safe}$_3(\alpha)$ in Table~\ref{tab:safeness}.
\item $\alpha = \mathit{bsync(sw,xid,cs)}$. This $\alpha$
only affects \emph{brq}, $\mathit{sw'.fq}$, $\mathit{sw'.cq}$ (for some switches $sw'$), and the control state $\mathit{cs}$.
We know by definition of Specification Language (\S\ref{spec}) that it cannot refer to \emph{brq} or any $\mathit{sw'.fq}$, $\mathit{sw'.cq}$.
In case the control state changes, $\alpha$ is invisible to $\varphi$ because \emph{Safe}$_3(\alpha)$ in Table~\ref{tab:safeness}.

 \item $\alpha = \mathit{fwd(sw,pk,ports)}$. Assumption \emph{Safe}$_3(\alpha)$ in Table~\ref{tab:safeness} guarantees that the only variables $\alpha$ can change, i.e.\ $\mathit{D.pq}$ or $\mathit{D.rcvq}$ for any $D$ in $\lambda(\mathit{sw,p})_1 \mid p \in \mathit{ports}$ and $\mathit{sw.pq}$,
actually remain unchanged. Thus it follows by definition that $\alpha$ is invisible to $\varphi$.

 \item $\mathit{\alpha = brepl(sw,xid)}$. Since, by definition of Specification Language (\S\ref{spec}), the atomic propositions refer neither to any $\mathit{cq}$ nor $\mathit{brq}$, it follows from the effect of $\alpha$ that only affects $\mathit{sw.cq}$ and $\mathit{brq}$

 that any $\mathit{brepl(\cdot)}$ is always invisible.
\item $\mathit{\alpha = recv(h,pk)}$. Assumption \emph{Safe}$_3(\alpha)$ in Table~\ref{tab:safeness} guarantees that $\varphi$ does not refer to $\mathit{h.rcvq}$, which is the only variable affected by $\alpha$,
and therefore $\mathit{recv(h,pk)}$ is invisible to $\varphi$.

 \end{itemize}

\end{proof}

\ignore{
\noindent\textbf{Theorem \ref{thm1}}
\begin{proof}
	Detailed proofs are provided in \cite{Baier2008}\footnote{Theorem 8.13. (page 611)}
\end{proof}

\noindent\textbf{Lemma \ref{lemmaimpl1}}
\begin{proof}
	We will prove that
	$\forall \rho = s_0 \xhookrightarrow[]{\alpha_1}_2 s_1  \xhookrightarrow[]{\alpha_2}_2...$ in $\mathcal{M}_2$,
	$\exists \dot{\rho} = s_0 \xhookrightarrowdbl[]{\dot{\alpha}_1} \dot{s}_1  \xhookrightarrowdbl[]{\dot{\alpha}_2}...$ in $\mathcal{M}'$
	s.t.
	$\rho \stutt  \dot{\rho}$.\\\\
	We construct $\dot{\rho}$ by scanning $\rho$ from $s_0$.
	For all transitions in $\rho$ labelled by the action $ctrl\_h{\text -}fwd(sw,pk,fpts,cs)$, we split the latter into $ctrl(pk,cs)$ and $h{\text -}fwd(sw,pk,fpts)$, which, according to the definition of $\hookrightarrow_2 $, gives the fragment

	$\dot{s}_i \xhookrightarrowdbl{ctrl(pk,cs)}   \dot{s}_i' \xhookrightarrowdbl{h{\text -}fwd(sw,pk,fpts)}   \dot{s}_{i+1} $ in $\dot{\rho}$.\\
	By defining
	$$
	\infer{\dot{s}_i  \xhookrightarrowdbl[]{\alpha_{i+1}}~ \dot{s}_{i+1} } {s_i \xhookrightarrow[]{ \alpha_{i+1}}_2    s_{i+1} \land \alpha \text{ is not } ctrl\_h{\text -}fwd(sw,pk,fpts,cs) }
	$$
	the construction of $\dot{\rho}$ ensures that $\forall i \geq 0, s_i = \dot{s}_i$.\\
	Last, since $h{\text -}fwd(sw,pk,fpts)$ is invisible (by Lemma \ref{lemmafwdinv}), $L(\dot{s}_i') = L(\dot{s}_{i+1})$. Then $s_is_{i+1}$ and $\dot{s}_i \dot{s}_i' \dot{s}_{i+1}$ are stuttering equivalent, and thus
\end{proof}

\noindent\textbf{Lemma \ref{lemmaimpl2}}
\begin{proof}
	We now prove that any trace in $\mathcal{M}'$ is mimicked by a stuttering one in $\mathcal{M}_2$.
	Let $\rho = s_0 \xhookrightarrowdbl[]{\alpha_1} s_1  \xhookrightarrowdbl[]{\alpha_2}...$ a run in $\mathcal{M}'$.
	$\dot{\rho}$ is constructed as follows. We walk through $\rho$ looking for a $h{\text -}fwd$-enabler $ctrl(pk,cs)$ action (denoted $ctrl^\ast$). If no $ctrl^\ast(pk,cs)$ is found, then $\rho$ exists in $\mathcal{M}_2$ by definition of $\hookrightarrow_2$.
	Otherwise, $\rho$ is of the form
	$\rho = s_0 \xhookrightarrowdbl[]{\alpha_1} s_1  \xhookrightarrowdbl[]{\alpha_2}...\xhookrightarrowdbl[]{\alpha_{i-1}} s_{i-1}  \xhookrightarrowdbl[]{ctrl^\ast(pk,cs)} s_i \xhookrightarrowdbl[]{h{\text -}fwd} s_{i+1}...$,
	where $\forall_{1 \leq j \leq i-1}, \alpha_j$ is not a $ctrl^\ast$ action.
	Given the walk $\rho$, the rule of inference in definition of $\hookrightarrow_2$ returns
	$\hat{\rho} = s_0 \xhookrightarrow[]{\alpha_1}_2 s_1  \xhookrightarrow[]{\alpha_2}_2...\xhookrightarrow[]{\alpha_{i-1}}_2 s_{i-1}  \xhookrightarrow[]{ctrl\_h{\text -}fwd(sw,pk,fpts)}_2  s_{i+1}...$.
	The path prefixes $s_0 \xhookrightarrowdbl[]{} ^* s_{i+1}$ of $\rho$ and $s_0 \hookrightarrow^*_2 s_{i+1}$ of $\hat{\rho}$ are stutter equivalent as $h{\text -}fwd(sw,pk,fpts)$ is invisible.
	By a similar reasoning it can be deduced that the rest fragments from $s_{i+1}$ of $\rho$ and $\hat{\rho}$ are stutter equivalent.
	Next, applying the same reasoning from $s_{i+1}$ on in $\hat{\rho}$ we end up with an execution $\dot{\rho}$ in $\mathcal{M}_2$ such that $\rho \stutt \dot{\rho}$.
\end{proof}

\noindent\textbf{Theorem \ref{thm2}}
\begin{proof}
	Follows immediately by Lemmas \ref{lemmaimpl1} and \ref{lemmaimpl2}.
\end{proof}

\noindent\textbf{Theorem \ref{thm3}}
\begin{proof}
	Follows directly from Theorems \ref{thm1} and \ref{thm2}.
\end{proof}

\newpage

\noindent Cycles proof:\\

\noindent It is worth pointing out that if all the edges of a cycle are safe ones, then any unsafe action enabled at some state $s$ of the cycle is never included in $ample(s)$ of the cycle for any state $s$ of it.

{A handy way to reason about independence of actions is as follows.
	%

	%
	Let $\mathcal{M}  = (S, A, \hookrightarrow, s_0, AP, L)$ be a transition system over a finite set $X$ of variables.
	%
	Since states represent  evaluations of system variables, the consequence on a variable to taking a transition is formalised as
	%

	$$ conseq : A \times S  ~\to~  S  $$
	%
	such that for $s \in S$ and $\alpha \in A(s)$, $\exists s' \in S $ with $ (s, \alpha, s') \in \hookrightarrow$.\\
	%
	Let $\bar{x} = (x_1,...,x_k)$ be a variable tuple in $X$ and $s[\bar{x}] $ denote the current evaluation of $\bar{x}$ in a state $s$.
	$ conseq(\alpha, s[\bar{x}])$ expresses the (re)evaluation of variable $\bar{x}$ by performing $\alpha$ in state $s$, i.e., $ conseq(\alpha, s[\bar{x}]) = \alpha(s)[\bar{x}]$.
	%
	%
	%
	%
	%
	\begin{comment}
	Further, let $\mathcal{E}(X)$ denote the set of all evaluations of $X$ that assign values to variables.
	%
	The consequence on a variable to taking a transition is formalised as

	$$ conseq : A \times \mathcal{E}(X) ~\to~  \mathcal{E}(X)  $$
	Let $\bar{x} = (x_1,...,x_k)$ be a variable tuple in $X$ and $\varepsilon_s \in \mathcal{E}(X)$ the current evaluation of $X$ in a state $s$.
	$ conseq(\alpha, \varepsilon_s)(\bar{x})$ expresses the (re)evaluation of variable $\bar{x}$ by performing $\alpha$, i.e., $ conseq(\alpha, \varepsilon_s)(\bar{x}) = \alpha(s)(\bar{x})$.\\
	\end{comment}
	%
	An action $\alpha \in A $ is independent of every action $\beta \in A \setminus \{\alpha\}$, and vice versa, if for any state $s$ such that $ s \xhookrightarrow[]{  g_\alpha? \shortto \alpha  }    s'  $ and $ s \xhookrightarrow[]{  g_\beta? \shortto \beta  }    s''  $,
	\begin{enumerate}[(a)]
		\item guard $g_\alpha$ does not refer to the variables that appear in $\beta$,
		\item guard $g_\beta$ does not refer to the variables that appear in $\alpha$, and
		\item $ conseq(\alpha \interleave \beta, s) = conseq\big(   (\alpha \triangleright \beta   )   ~\hexstar~  (\beta \triangleright \alpha   ),  s \big)  $

	\end{enumerate}
	%
	where the interleaving operator $\interleave$ stands for the concurrent execution of independent activities (by enumerating all the possible orders in which they can be executed), $\triangleright$ for sequential execution, and $\hexstar$ for nondeterministic choice.
	Intuitively, $\alpha$ and $\beta$ are independent of each other when they access disjoint variables.
	The following statement is equivalent to condition (c):
	%
	\[ conseq(\alpha, s[\bar{x}_\beta]) = s[\bar{x}_\beta]   ~\land~    conseq(\beta, s[\bar{x}_\alpha]) = s[\bar{x}_\alpha] \]
	%
	for all data $\bar{x}_\beta$ accessed by $\beta $ and $\bar{x}_\alpha$ accessed by $\alpha $.
	}

}

\ignore{
\section{Topology Setups}\label{appendix:topo}

The network setups used to evaluate MOCS are depicted in Figure \ref{table:topologies1} for the MAC learning application and Figure \ref{table:topologies2} for the stateful firewall. The topology setups for the stateless firewall follow the pattern of those with two switches in Figure \ref{table:topologies1}.

\begin{figure}[h]
	\captionsetup{width=1\textwidth}
	\includegraphics[width=1\linewidth]{figures/topo1.pdf}

		\caption{Network topologies for verifying absence of loops in the MAC address learning application.}

	\label{table:topologies1}
\end{figure}

\begin{figure}[h]
	\centering
	\captionsetup{width=1\textwidth}
	\includegraphics[width=1\linewidth]{figures/topo2.pdf}
	\caption{Network topologies for the stateful firewall.}

	\label{table:topologies2}
\end{figure}

}

\section{Controller Programs}\label{appendix:CP}

\setcounter{algocf}{0}
\renewcommand{\thealgocf}{CP\arabic{algocf}}
\renewcommand{\theHalgocf}{Supplement.\thealgocf}
\resizebox{1\textwidth}{!}{%
	\begin{minipage}{1.8\textwidth}
		\begin{algorithm}[H]

			\DontPrintSemicolon
			\SetKwInOut{Input}{Input}
			\SetKwInOut{Output}{Output}
			\SetKwFunction{FMain}{pktIn}
			\SetKwProg{Fn}{handler}{:}{}
			\SetAlgorithmName{\large Controller Program}{}

			%

			%

			\Fn{\FMain{\upshape{\texttt{sw, pkt}}}}{

				\If(\textcolor{gray}{\tcp*[f]{Otherwise, pkt is dropped silently}} ){\upshape{\texttt{\textcolor{black}{\textbf{not}} pkt.SSH}}}{

					\texttt{send\_message}\big(\texttt{PacketOut(pkt, 2), sw}\big)   \;
				}

				$\texttt{rule1} \gets \texttt{\big \{\{prio} \gets \texttt{10\}, \{SSH } \gets \texttt{1~~\}, \{in\_port} \gets \texttt{*\}, \{fwd\_port} \gets \texttt{drop\}\big \}  } $\;

				$\mathrlap{\texttt{rule2} \gets \texttt{\big \{\{prio} \gets \texttt{~1\}, \{SSH } \gets \texttt{*~~\},}}\hphantom{\texttt{rule1 = \big \{\{prio = 10\}, \{prot = SSH\}, }}  \texttt{\{in\_port} \gets \texttt{1\}, \{fwd\_port} \gets \texttt{2  ~ \}\big \}  }$ \textcolor{gray}{\tcp*[r]{asterisk (*) matches any value}}

				$\mathrlap{\texttt{rule3} \gets \texttt{\big \{\{prio} \gets \texttt{~1\}, \{SSH } \gets \texttt{*~~\},}}\hphantom{\texttt{rule1 = \big \{\{prio = 10\}, \{prot = SSH\}, }}  \texttt{\{in\_port} \gets \texttt{2\}, \{fwd\_port} \gets \texttt{1   ~~\}\big \}  }$\;

				\ForAll(\textcolor{gray}{\tcp*[f]{Switches is the set of all switches}}){\upshape{\texttt{s}} $\in$ \upshape{\texttt{Switches}}}{

					\texttt{send\_message}\big(\texttt{FlowMod\big(add(rule2)\big), s}\big)  \;
					\texttt{send\_message}\big(\texttt{FlowMod\big(add(rule1)\big), s}\big)  \;
					\texttt{send\_message}\big(\texttt{BarrierReq\big(b\_id\big), ~~~s}\big)  \textcolor{gray}{\tcp*[r]{b\_id is a barrier identifier}}
					\texttt{send\_message}\big(\texttt{FlowMod\big(add(rule3)\big), s}\big)  \;
				}

			}
			\caption{\large A stateless firewall filter with control messages reordering bug. In a bug-free program (the one we used to verify in \S\ref{experimental-evaluation}), \texttt{rule1} should be sent first and followed by a barrier. Property: \emph{``neither host should be accessed over {\sc ssh}"}. Formally, $\Box\big(\forall h\, {\in}\, \mathit{Hosts}\,\forall \mathit{pkt}\, {\in}\, \mathit{h.rcvq} \,.\, \neg \mathit{pkt}.\mathrm{\textsc{ssh}})$.}
			\label{rq1-alg11}
		\end{algorithm}
	\end{minipage}%

\\\\\\
\resizebox{1\textwidth}{!}{%
	\begin{minipage}{1.8\textwidth}
		\begin{algorithm}[H]

			\DontPrintSemicolon
			\SetKwInOut{Input}{Input}
			\SetKwInOut{Output}{Output}
			\SetKwFunction{FMain}{pktIn}
			\SetKwFunction{FBar}{barrierIn}
			\SetKwProg{Fn}{handler}{:}{}
			\SetAlgorithmName{\large Controller Program}{}

				%

				%

			\Fn{\FMain{\upshape{\texttt{sw,  pkt}}}}{

				\uIf(\textcolor{gray}{\tcc*[f]{allowed\_conn is a fixed  ~~~~\textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\hspace{2.6mm}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~* whitelist of TCP   ~~~~\textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\hspace{2.6mm}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~* socket connections  \textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\hspace{2.6mm}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~* (host, TCP\_port) $\mapsto$ ~~~~\textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\hspace{2.6mm}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~* (host, TCP\_port) ~~~~\textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\hspace{2.6mm}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}} ){\upshape{\texttt{allowed\_conn[pkt.src][pkt.src\_TCP\_port][pkt.dest][pkt.dest\_TCP\_port]   }}}{

					\texttt{send\_message}\big(\texttt{PacketOut(pkt, 2), sw}\big)   \;

					$\mathrlap{\texttt{rule1.src}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{pkt.src} $ \;
					$\mathrlap{\texttt{rule1.src\_TCP\_port}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{pkt.src\_TCP\_port} $ \;
					$\mathrlap{\texttt{rule1.dest}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{pkt.dest} $ \;
									  $\texttt{rule1.dest\_TCP\_port}	\gets 	\texttt{pkt.dest\_TCP\_port} $      \;
					$\mathrlap{\texttt{rule1.fwd\_port}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{2} $ \;
					$\mathrlap{\texttt{rule1.prio}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{2} $ \;

					$\mathrlap{\texttt{rule2.src}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{pkt.dest} $ \;
					$\mathrlap{\texttt{rule2.src\_TCP\_port}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{pkt.dest\_TCP\_port} $ \;
					$\mathrlap{\texttt{rule2.dest}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{pkt.src} $ \;
									  $\texttt{rule2.dest\_TCP\_port}	\gets 	\texttt{pkt.src\_TCP\_port} $      \;
					$\mathrlap{\texttt{rule2.fwd\_port}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{1} $ \;
					$\mathrlap{\texttt{rule2.prio}}\hphantom{\texttt{rule2.dest\_TCP\_port}} \gets 	\texttt{2} $ \;

					\ForAll(\textcolor{gray}{\tcp*[f]{access rules are uniform across all switches, any of which acting as firewall replica}}){\upshape{\texttt{s}} $\in$ \upshape{\texttt{Switches}}}{

						\texttt{send\_message}\big(\texttt{FlowMod\big(add(rule1)\big), s}\big)  \;
						\texttt{send\_message}\big(\texttt{FlowMod\big(add(rule2)\big), s}\big)  \;
						\texttt{send\_message}\big(\texttt{BarrierReq\big(b\_id\big), ~~~s}\big)  \textcolor{gray}{\tcp*[r]{b\_id is uniquely associated with an allowed connection}}
					}

				}
				\Else{

					\texttt{send\_message}\big(\texttt{PacketOut(pkt, drop), sw}\big)   \;

					$\mathrlap{\texttt{drop\_rule.src}}\hphantom{\texttt{drop\_rule.dest\_TCP\_port}} \gets 	\texttt{pkt.src} $ \;
					$\mathrlap{\texttt{drop\_rule.src\_TCP\_port}}\hphantom{\texttt{drop\_rule.dest\_TCP\_port}} \gets 	\texttt{pkt.src\_TCP\_port} $ \;
					$\mathrlap{\texttt{drop\_rule.dest}}\hphantom{\texttt{drop\_rule.dest\_TCP\_port}} \gets 	\texttt{pkt.dest} $ \;
									   $\texttt{drop\_rule.dest\_TCP\_port}	\gets 	\texttt{pkt.dest\_TCP\_port} $      \;
					$\mathrlap{\texttt{drop\_rule.fwd\_port}}\hphantom{\texttt{drop\_rule.dest\_TCP\_port}} \gets 	\texttt{drop} $ \;
					$\mathrlap{\texttt{drop\_rule.prio}}\hphantom{\texttt{drop\_rule.dest\_TCP\_port}} \gets 	\texttt{1} $ \;

					\ForAll{\upshape{\texttt{s}} $\in$ \upshape{\texttt{Switches}}}{
						\texttt{send\_message}\big(\texttt{FlowMod\big(add(drop\_rule)\big), s}\big)  \textcolor{gray}{\tcp*[r]{access restrictions are uniform across all replicas}}
					}
				}
			}
				\;
		\Fn{\FBar{\upshape{\texttt{sw, xid}}}}{

			\texttt{controller\_view[b\_id][sw]} $\gets$ \texttt{\textcolor{violet}{\textbf{true}}} \textcolor{gray}{\tcc*[r]{controller\_view associates installed rules (through the respective b\_id) \textcolor{white}{a}~~~~~~~~~~~\hspace{2mm}~~~~~~~~~\quad\,~~~~~~~~~\enspace~~~* for respective allowed connections with switches  \textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~\hspace{2.5mm}~~~~~~~~~~}}
		}
			\caption{\large Stateful inspection firewall (Figure \ref{fig:prop2}). The property we verify is: \emph{``a packet is never dropped by a rule in a switch if the controller is aware of a matching rule being already installed in this switch"}. Formally:
				$\Box \Big([\mathit{drop_m(pkt, sw)}]   \neg \mathit{controller\_view[pkt.src][pkt.src\_TCP\_port][pkt.dest][pkt.dest\_TCP\_port][sw]}\Big)$ \newline where $[\mathit{drop_m(pkt, sw)}]P$ is short for
				$[\mathit{match(sw, pkt, r)}]\big((r.\mathit{fwd\_ports}=\texttt{drop}) \Rightarrow P\big)$.
		}

			\label{rq1-alg12}
		\end{algorithm}
	\end{minipage}%

\\\\\\
\newlength{\commentWidth}
\setlength{\commentWidth}{8.5cm}
\newcommand{\atcp}[1]{\textcolor{gray}{\tcp*[r]{\makebox[\commentWidth]{#1\hfill}}}}
\resizebox{1\textwidth}{!}{%
	\begin{minipage}{1.8\textwidth}
		\begin{algorithm}[H]

			\DontPrintSemicolon

			\SetKwInOut{Input}{Input}
			\SetKwInOut{Output}{Output}
			\SetKwFunction{FMain}{pktIn}
			\SetKwProg{Fn}{handler}{:}{}
			\SetAlgorithmName{\large Controller Program}{}

			%

			%

			\Fn{\FMain{\upshape{\texttt{sw,  pkt}}}}{

				\If(\textcolor{gray}{\tcp*[f]{MAC\_table associates sender with a switch port}}){\upshape{\texttt{\textcolor{black}{\textbf{not}} MAC\_table[sw][pkt.src]}}   }{
					\upshape{\texttt{MAC\_table[sw][pkt.src] $ \gets$ \texttt{pkt.in\_port} }} \;
				}

				\uIf{\upshape{\texttt{MAC\_table[sw][pkt.dest]}}}{
					\texttt{send\_message}\big(\texttt{PacketOut(pkt, MAC\_table[sw][pkt.dest]), sw}\big)

					$\mathrlap{\texttt{rule.src}}\hphantom{\texttt{rule.fwd\_port}} \gets 	\texttt{pkt.src} $ \;
					$\mathrlap{\texttt{rule.dest}}\hphantom{\texttt{rule.fwd\_port}} \gets 	\texttt{pkt.dest} $ \;
					$\mathrlap{\texttt{rule.in\_port}}\hphantom{\texttt{rule.fwd\_port}} \gets  \texttt{pkt.in\_port}$ \;

					$\texttt{rule.fwd\_port}	\gets 	\texttt{MAC\_table[sw][pkt.dest]} $      \;
					$\mathrlap{\texttt{rule.prio}}\hphantom{\texttt{rule.fwd\_port}} \gets 	\texttt{1} $ \;
					\texttt{send\_message}\big(\texttt{FlowMod\big(add(rule)\big), sw}\big)   				}
				\Else{
					\texttt{send\_message}\big(\texttt{PacketOut(pkt, flood\textbackslash\{pkt.in\_port\}), sw}\big)   	   \textcolor{gray}{\tcp*[f]{ \text{pkt} will be flooded to all ports except incoming one}}

				}
			}
			\caption{\large MAC learning application\textsuperscript{$^\dag$} for verifying absence of loops. In order to keep track of the network devices the packet passes through (i.e. the packet path history), the packet type is augmented with a history bit-field \emph{reached}, where each bit represents a visited/unvisited switch. As packets are being flooded, their history bit-field is re-written. The loop freedom property asserts that \emph{``a packet should not come back to the same switch"}. Formally,
				$\Box \big(\forall \mathit{sw}\, {\in}\,\mathit{Switches} ~\forall \mathit{pkt}\, {\in}\,\mathit{sw.pq} \,. \,\neg \mathit{pkt.reached[sw]}\big)$.}
			\label{rq1-alg13}
		\end{algorithm}
		\small\textsuperscript{$^\dag$} \url{https://github.com/noxrepo/pox/blob/412a6adb38cb646748c8cfb657549787ab6d2e88/pox/forwarding/l2_learning.py}
	\end{minipage}%

\\\\\\
\resizebox{1\textwidth}{!}{%
	\begin{minipage}{1.8\textwidth}
		%
		\MyBox{starta}{enda}{red}
		\MyBox[-3ex]{startb}{endb}{gray}
		%
\hspace{-5mm}		\begin{algorithm}[H]

			\DontPrintSemicolon
			\SetKwInOut{Input}{Input}
			\SetKwInOut{Output}{Output}
			\SetKwFunction{FMain}{pktIn}
			\SetKwFunction{FBar}{barrierIn}
			\SetKwProg{Fn}{handler}{:}{}
			\SetAlgorithmName{\large Controller Program}{}

				%

				%

			\Fn{\FMain{\upshape{\texttt{sw, pkt}}}}{

				\uIf{\upshape{\texttt{pkt.SSH and pkt.dest == S}}}{
					\tikzmark{startb}
					\uIf(\textcolor{gray}{\tcp*[f]{f is initialised as false. pkt is dropped silently} }){\upshape{\texttt{\textcolor{black}{\textbf{not}} f}}}{

						$\mathrlap{\texttt{f}}\hphantom{\texttt{drop\_rule.fwd\_port}}  \gets   \texttt{\textbf{true}}  $\;

						$\mathrlap{\texttt{drop\_rule.prio}}\hphantom{\texttt{drop\_rule.fwd\_port}} \gets 	\texttt{1} $ \;
						$\mathrlap{\texttt{drop\_rule.SSH}}\hphantom{\texttt{drop\_rule.fwd\_port}} \gets 	\texttt{pkt.SSH} $ \;
						$\mathrlap{\texttt{drop\_rule.dest}}\hphantom{\texttt{drop\_rule.fwd\_port}} \gets  \texttt{pkt.dest}$ \;

						$\texttt{drop\_rule.fwd\_port}	\gets 	\texttt{drop} $      \;

						\ForAll{\upshape{\texttt{s}} $\in$ \upshape{\texttt{Switches}}}{
							\texttt{send\_message}\big(\texttt{FlowMod\big(add(drop\_rule)\big), s}\big)  \;
							\texttt{send\_message}\big(\texttt{BarrierReq\big(b\_id\big), ~~~~~~~s}\big)   \textcolor{gray}{\tcp*[f]{b\_id is a barrier identifier}}\tikzmark{endb}
						}
					}
					\tikzmark{starta}
					\Else{
						\texttt{send\_message}\big (\texttt{PacketOut(pkt, 2), sw}\big)   \;

						$\mathrlap{\texttt{rule.prio}}\hphantom{\texttt{rule.fwd\_port}} \gets  \texttt{2} $ \;
						$\mathrlap{\texttt{rule.SSH}}\hphantom{\texttt{rule.fwd\_port}} \gets  \texttt{pkt.SSH} $ \;
						$\mathrlap{\texttt{rule.dest}}\hphantom{\texttt{rule.fwd\_port}} \gets  \texttt{pkt.dest} $ \;

						$\texttt{rule.fwd\_port} \gets \texttt{2} $	\;

						\ForAll{\upshape{\texttt{s}} $\in$ \upshape{\texttt{Switches}}}{

							\texttt{send\_message}\big(\texttt{FlowMod\big(add(rule)\big), s}\big) \hfill \tikzmark{enda}
						}
					}
				}
				\Else{
					... \;
				}

			}

			\caption{\large Wrong nesting level bug: Executing the \texttt{else}-branch - shaded red - would violate the policy that \emph{``server S (Figure \ref{fig:prop1}) should not be accessed over {\sc ssh}"}, $\Box(\forall \mathit{pkt}\, {\in}\, \mathit{S.rcvq} \,.\, \neg \mathit{pkt}.\mathrm{\textsc{ssh}})$.}
			\label{rq1-alg2}
		\end{algorithm}
	\end{minipage}%

\\\\\\
	\resizebox{1\textwidth}{!}{%
	\begin{minipage}{1.8\textwidth}
		\begin{algorithm}[H]

			\DontPrintSemicolon
			\SetKwInOut{Input}{Input}
			\SetKwInOut{Output}{Output}
			\SetKwFunction{FMain}{pktIn}
			\SetKwFunction{FBar}{barrierIn}
			\SetKwProg{Fn}{handler}{:}{}
			\SetAlgorithmName{\large Controller Program}{}

				%

		%

			\Fn(\textcolor{gray}{\tcp*[f]{Assumption: a drop-all rule with priority 0 is installed in switch B (Fig.\ref{fig:prop1})}}){\FMain{\upshape{\texttt{sw, pkt}}}}{

				\uIf(\textcolor{gray}{\tcc*[f]{b\_id is uniquely associated with rule\_S which \textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~~~~~\,\,~~~~~~\hspace{1.4mm}~~~~~~~~~~~~~~~~~~~~~~~~~~~~* overrides the drop-all entry at B, and  \textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\,\,~\hspace{1.3mm}~~~~~~~~~~~~~~* allows packets to be forwarded to S through  \textcolor{white}{a}~~~~~~~~~~~~~~~~~\hspace{1.3mm}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\,\,~~~~~~* port 2 \textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\hspace{.8mm}~~~~~~~~~~~~~~~~~~~~~~~~~~~~~}}){\upshape{\texttt{pkt.dest == S  and  BarrierRes(b\_id) not received}}}  {
						\If(\textcolor{gray}{\tcc*[f]{packets\_held is temporarily storing packets sent by B until consistent \textcolor{white}{a}~~~~~~~~~~~~~~~~~~~~~~~~\,\,~~~~~~\hspace{1.4mm}~~~~* update is complete \textcolor{white}{a} ~~~~~~~~~\textcolor{white}{a} ~~~~~~~~~~~ \textcolor{white}{a}~\textcolor{white}{a}~~~~~~~\hspace{1.2mm}~~~ ~~~~~~\,\,~ ~~~~\hspace{.3mm}~~~~~~~\textcolor{white}{a}}}){\upshape{\texttt{\textcolor{black}{\textbf{not}} packets\_held[sw][pkt]  }}}{
							\upshape{\texttt{packets\_held[sw][pkt] $ \gets$ \texttt{\textbf{true}} }} \;
							$\texttt{rule\_S} \gets \texttt{\big \{\{dest} \gets \texttt{S\}, \{fwd\_port} \gets \texttt{2\}, \{prio} \gets \texttt{2\}\big \}  } $\;
							\texttt{send\_message}\big(\texttt{FlowMod\big(add(rule\_S)\big), B}\big)   	\;
							\texttt{send\_message}\big(\texttt{BarrierReq\big(b\_id\big), ~~~~B}\big)
					}
				}
				\Else{

						\texttt{send\_message}\big (\texttt{PacketOut(pkt, 2), sw}\big)   \;
				}
			}
		\;
			\Fn{\FBar{\upshape{\texttt{sw, xid}}}}{
					\If{\upshape{\texttt{xid == b\_id}}}{
					$\texttt{rule\_S} \gets \texttt{\big \{\{dest} \gets \texttt{S\}, \{fwd\_port} \gets \texttt{2\}, \{prio} \gets \texttt{2\}\big \}  } $\;
						\ForAll(\textcolor{gray}{\tcp*[f]{all switches except B}}){\upshape{\texttt{s}} $\in$ \upshape{\texttt{Switches\textbackslash\{B\}}}}{

							\texttt{send\_message}\big(\texttt{FlowMod\big(add(rule\_S)\big), s}\big)
					}

				\While{\upshape{\texttt{packets\_held[swi][p] for some (p, swi) \texttt{\textbf{and}} p.dest == S}}}{
					\upshape{\texttt{packets\_held[swi][p]}} $\gets$ \texttt{\textbf{false}}    \textcolor{gray}{\tcp*[r]{swi is the switch packet p was sent from}}

					\texttt{send\_message}\big (\texttt{PacketOut(p, 2), swi}\big)
				}
				}
			}
			\caption{\large Consistent updates. We verify the property that \emph{``a packet destined to server S is never dropped at any switch"}. Formally:
				$\Box \big( [\mathit{drop_{mf}(pkt,sw)}]   \neg (\mathit{pkt.dest = S})  \big)$, where $[\mathit{drop_{mf}(pkt,sw})]P$ is  short for $[\mathit{match(sw, pkt, r)}]\big((r.\mathit{fwd\_ports}=\texttt{drop}) \Rightarrow P\big) \land [\mathit{fwd}(\mathit{sw, pkt}, \mathit{fwd\_ports})]\big((\mathit{fwd\_ports}=\texttt{drop}) \Rightarrow P\big).$
							}
			\label{rq1-alg3}
		\end{algorithm}
	\end{minipage}%

\newpage

\ignore{
\noindent \textbf{Disproof for the $(0,\infty)$ abstraction of Kuai }
Let $r$ a flow entry which matches packet $pkt$ in switch $A$ (Fig. \ref{fig:prop2}) and adds it in the $pq$ of switch $B$.
Then, the property $\Box (pkt \in B.pq \implies pkt \in A.pq)$ holds always in the abstract transition system $TS_4$ with $(0,\infty)$ packet queues but could be violated in the original ($TS_3$).\\
We fix this by redefining the specification language such that no more then one atomic propositions of the property are allowed to assert about the (non)existence of the same packet in different buffers. This way, the property is restricted to asserting about one only occurrence of an object in all buffers, and only then the $(0,\infty)$ abstract model is a property-preserving abstraction, i.e., a homomorphic image of the unabstracted one.
}

\ignore{

\newpage

\begin{defn}[SDN instantiation]
	\label{def:instantiation}
	An SDN instantiation $sdn_i$ is the pair $(\lambda, \textsc{controller})$.
\end{defn}

\begin{defn}[Context]
	\label{def:context}
	A context {\sc ctx} is a pair of an SDN instantiation $sdn_i$ and a state property $\varphi$.
\end{defn}

\begin{defn}[Subtrace]
	\label{subtrace}
	A subtrace $\sigma'$ is a trace that can be derived from another trace $\sigma$ by deleting some or no elements without changing the original order of the remaining elements, where elements are sets of atomic propositions that are valid in the states of the corresponding path. We denote $\sigma' \subtrace ~\sigma$.
\end{defn}

\begin{defn}[Trace Fragment]
	A trace fragment $\sigma'$ of a trace $\sigma$ is a trace which consists a contiguous sequence of state labels within $\sigma$. The trace fragment is a refinement of the subtrace.
\end{defn}

\noindent \textbf{MOCS\ inclusiveness}
In the following we will show that Kuai model's behaviour-set is subsumed into MOCS\ (equivalently, MOCS\ is inclusive of Kuai). Intuitively, a transition system is subsumed into another if every behaviour in the former can be mimicked by at least one behaviour in the latter.
We analyse the inclusiveness of MOCS\ before any abstraction is applied to Kuai and MOCS\ because each abstract transition system is inclusive of the one it was abstracted from.

MOCS\ incorporates all actions of Kuai but \emph{barrier}.
With regard to the \emph{wait}-variable that is part of the state in Kuai (but not in MOCS) we remind that Kuai uses it as a lock (binary semaphore) in order to orchestrate threads by enforcing a mutual exclusion concurrency control policy: whenever a \emph{nomatch} occurs the mutex for the switch in question is locked and it is unlocked by the \emph{fwd} action of the thread \emph{nomatch-ctrl-fwd} which refers to the same packet; all other threads are forced to wait.
Via this form of synchronisation, the actions \emph{nomatch-ctrl-fwd} are not interleaved with other actions in the switch.\\
The existence of a barrier in the $cq$ of a switch is another lock in Kuai model\footnote{This is done via the predicate $noBarrier(sw)$ which guards all the actions.} used to prioritise the installation of all control messages prior to the barrier.
Through these locks, Kuai restricts the interleavings of the concurrent threads.
On the other hand, MOCS\ is asynchronous in this regard: it gets rid of the two locks and generalises Kuai derestricting interleavings of transitions. Also, the properties in Kuai do not use assertions over the \emph{wait}-variable, so the \emph{wait}-mode is not projected in any trace.

Two traces $\sigma$ and $\sigma'$ are said to be stuttering equivalent if they
are identical after removing all repeated labels of the states with atomic proposition, denoted by $\sigma \stutt \sigma'$.

\begin{thm}[MOCS\ inclusiveness]
	\label{thm:inclusiveness}
	Let
	$\mathcal{M}  = (S, A, \hookrightarrow, s_0, AP, L)$
	and
	$\mathcal{M}_ K  = (S_K, A_K, \hookrightarrow_K, s_0, AP, L)$
	the original models of MOCS\ and Kuai, respectively, and
	$Traces(\mathcal{M})$,
	$Traces(\mathcal{M}_ {K})$
	denote the set of all initial traces in these models.
	The set of traces of MOCS\ is inclusive of stutter-equivalent traces of Kuai, denoted $\mathcal{M}_ {K} \sqsubseteq \mathcal{M}$, where $\sqsubseteq$ is defined by:
	\[\mathcal{M}_ {K} \sqsubseteq \mathcal{M} \iff \forall \sigma_{\!_K} \in Traces(\mathcal{M}_ {K})  ~\exists \sigma_{\!_M} \in Traces(\mathcal{M}) ~.~ \sigma_{\!_K} \stutt \sigma_{\!_M} \]
\end{thm}

\begin{proof}
	Let $B(sw)$ represent the sequence of all control messages ($add/del$ actions) in the $sw.cq$ prior to the first barrier. Further, $s_{\setminus[wait]}$ is a shorthand notation for the evaluation obtained from state $s$ by disregarding the variable $wait$.

	\noindent From the definition of the transitions systems of Kuai and MOCS, it follows that:
		\begin{align*}
		\infer{s_{\setminus[wait]} \xhookrightarrow[]{\alpha} s'_{\setminus[wait]} }{s \xhookrightarrow[]{\alpha}_K s' ~\land~ \alpha \in A_K \setminus Barrier } \
	\\[10pt]
	\infer{s_{\setminus[wait]} \xhookrightarrow[]{B(sw)} s'_{\setminus[wait]}  }{s \xhookrightarrow[]{barrier(sw)}_K s' }
	\end{align*}
	Since the atomic propositions in Kuai do not assert about the $wait$ variable, and furthermore, the $add/del$ actions are invisible, it always follows that $L(s_{\setminus[wait]} ) =  L(s)$ and $L(s'_{\setminus[wait]} ) = L(s')$.
	Hence, by applying the above rules, it follows directly that every trace which occurs in $\mathcal{M}_ {K}$ can be converted into an equivalent trace in $\mathcal{M}$.
\end{proof}

\noindent The following corollary follows directly from Thm. \ref{thm:inclusiveness}.
\begin{corollary}[Property preserving]
	For a context $\textsc{ctx}=(sdn_i, \varphi)$, if $\mathcal{M}(sdn_i) \models \Box \varphi$, then $\mathcal{M}_K(sdn_i) \models \Box \varphi$.
\end{corollary}

\ignore{
\begin{thm}[MOCS\ inclusiveness]
	\label{thm:correct}
	Let $Runs(\mathcal{M})$ denote the set of all initial runs of model $\mathcal{M}$.
	The set of behaviours of $\mathcal{M}_ {MOCS}  = (S_M, A_M, \hookrightarrow_M, s_0, AP, L)$ is inclusive of behaviours of $\mathcal{M}_ {Kuai}  = (S_K, A_K, \hookrightarrow_K, s_0, AP, L)$, denoted $\mathcal{M}_ {Kuai} \sqsubseteq \mathcal{M}_ {MOCS}$, where $\sqsubseteq$ is defined by:
	\[\mathcal{M}_ {Kuai} \sqsubseteq \mathcal{M}_ {MOCS} \iff \forall \rho_{\!_K} \in Runs(\mathcal{M}_ {Kuai})  ~\exists \rho_{\!_M} \in Runs(\mathcal{M}_ {MOCS}) ~\mathrm{s.t.:}  \]
	\begin{enumerate}[leftmargin=2cm]

		\item $L(\rho_{\!_K}) \subtrace ~L(\rho_{\!_M})$, or
		\item for every transition $s \xhookrightarrow{barrier_i(\cdot)}_K s'$ in $\rho_{\!_K}$, if we split $barrier_i$ into the add and del-actions which are flushed by the $barrier_i$,\\

		then we obtain $\rho'_{\!_K} \stutt \rho_{\!_K} : L(\rho'_{\!_K}) \subtrace ~L(\rho_{\!_M})$.
	\end{enumerate}

\end{thm}
\begin{proof}
	$ $\newline
	\vspace{-.4cm}
	\begin{enumerate}[(1)]
		\item This is the case when there is no any \emph{barrier} transition in $\rho_{\!_K}$. MOCS\ incorporates all actions of Kuai but \emph{barrier}.
		With regard to the \emph{wait}-variable that is part of the state in Kuai (but not in MOCS) we remind that Kuai uses it as a lock (binary semaphore) in order to orchestrate threads by enforcing a mutual exclusion concurrency control policy: whenever a \emph{nomatch} occurs the mutex is locked and it is unlocked by the \emph{fwd} action of the thread \emph{nomatch-ctrl-fwd} which refers to the same packet; all other threads are forced to wait.
		Via this form of synchronisation, the actions \emph{nomatch-ctrl-fwd} are merged (not interleaved with other actions) and the size of \emph{rq} is bounded above  to 1. This way, Kuai restricts the interleavings of the concurrent threads.
		On the other hand, MOCS\ is asynchronous in this regard: it generalises Kuai by derestricting interleavings of transitions. Also, the properties in Kuai do not use assertions over the \emph{wait}-variable, so the \emph{wait}-mode is not projected in any trace.
		Thus, by Definition \ref{subtrace} it follows that $L(\rho_{\!_K}) \subtrace ~L(\rho_{\!_M})$.

		\item Let $\rho_{\!_K} = s_0 ...  s_{i-1}  \xhookrightarrow{barrier_i(\cdot)}_K s_i ...$. We replace the transition $s_{i-1}  \xhookrightarrow{barrier_i(\cdot)}_K s_i$ with a  contiguous sequence of \emph{add} and \emph{del} transitions corresponding to all the control messages up to the last barrier in the control queue, in the same order they are flushed by the $barrier_i$. This sequence could be a subtrace of $\rho_{\!_M}$ (due to the interposition of \emph{brepl} if there are more than one barriers in the control queue in state $s_{i-1}$) or a trace fragment (if only one barrier). Then this case falls into case (1).

	\end{enumerate}

	More formally:\\

	\[ \infer[\mbox{\small ~$\textup{if}~pre\!-\!\check{\alpha}(\cdot) \in Enable(\check{\alpha}(\cdot))$  } ]{s \xrightarrow[]{\mathit{merge-}\check{\alpha}(\cdot)}_m s'' }{s \xhookrightarrowdbl[]{\mathit{pre-}\check{\alpha}(\cdot)} s'  \xhookrightarrowdbl[]{\check{\alpha}(\cdot)} s''  } \
	\qquad\qquad
	\infer{s \xrightarrow[]{\alpha(\cdot)}_m s' }{s \xhookrightarrowdbl[]{\alpha(\cdot)} s' }
	\]

\end{proof}
}

\newpage

\noindent If $M$ is a finite multi-set, then a \emph{multi-set permutation} of $M$ is an ordering of elements of $M$ in which each element appears exactly as often as is its multiplicity in $M$.
A multi-set permutation whose multiple instances are collapsed into one is called a \emph{collapsed permutation}.

\ignore{
\begin{defn}[Order-sensitive Controller Program]
	\label{def:ord-sens}
	Let $A'(s) \subseteq A$ denote the finite multi-set of all actions $ctrl(\cdot)$ and $bsync(\cdot)$ enabled in state $s$, and $G\big(A'(s)\big)$ the set of all collapsed permutations of $A'(s)$. A controller program is order-sensitive if there exists a state $s \in S$ such that the program state varies when changing the input collapsed permutation over $G\big(A'(s)\big)$.
\end{defn}
}

Let $A'(s) \subseteq A$ denote the finite multi-set of all actions $ctrl(\cdot)$ and $bsync(\cdot)$ enabled in state $s$, $G\big(A'(s)\big)$ the set of all multi-set permutations of $A'(s)$, and $g\big(A'(s)\big)$ is obtained by collapsing all the permutations of $G\big(A'(s)\big)$.
\ignore{
\begin{defn}[Order/Multiplicity-sensitive Controller Program]
	\label{def:mult-sens}
	A controller program {\sc cp} is order or multiplicity-sensitive if there exists a state $s \in S$ such that the program state varies when changing the input multi-set permutation from $G\big(A'(s)\big)$ -- for the sake of brevity, we say ``{\sc cp} is sensitive''.
\end{defn}
}
\begin{defn}[Order-sensitive Controller Program]
	\label{def:ord-sens}
	A controller program {\sc cp} is order-sensitive if there exists a state $s \in S$ and two collapsed permutations in $g\big(A'(s)\big)$ with different orders
	such that the program state varies when changing the input between the two permutations.
\end{defn}

\begin{defn}[Multiplicity-sensitive Controller Program]
	\label{def:mult-sens}
	A controller program {\sc cp} is multiplicity-sensitive to packet $pkt$ arrived from switch $sw$ if there exists a state $s \in S$, and two multi-set permutations in $G\big(A'(s)\big)$ which differs only on the multiplicity of $ctrl(sw,pkt,s.\gamma.cs)$ such that the program state varies when changing the input between the two multi-set permutations.
	For the sake of brevity, we say ``{\sc cp} is m-sensitive to $(sw,pkt)$ for some state $s$'' or ``{\sc cp} is m-sensitive to $ctrl(sw,pkt,s.\gamma.cs)$". \\
	Similarly, {\sc cp} is multiplicity-sensitive to barrier xid from sw if there exists a state $s \in S$, and two multi-set permutations in $G\big(A'(s)\big)$ which differs only on the multiplicity of $bsync(sw,xid,s.s.\gamma.cs)$ such that the program state varies when changing the input between the two.
	Throughout we write $\widetilde{\alpha}(\cdots)$ for actions the {\sc cp} is m-sensitive to.
\end{defn}
\noindent If the {\sc cp} is order-sensitive or multiplicity-sensitive to at least a packet, for the sake of brevity, we say informally (but still precisely) that ``{\sc cp} is sensitive".

\noindent \textbf{(0,1) Abstraction }
We define a $(0,1)$ counter abstraction, where the abstract occurrences are 0 when there are no elements in the buffer, and 1 if there is one or more elements in the buffer. The difference between $(0,1)$ and $(0,\infty)$ is that in the former abstraction the elements in the buffer the abstraction is applied to are consumable, i.e., de-bufferable.
Given a multiset $m$, we further define $under(m)(d)$ which
sets the non-zero multiplicity of $d$ in $m$ to $1$, and $over(m)(d)$ which sets the non-zero instances of $d$ to $\infty$.\\
\noindent \textbf{$\mathbf{(0,1)/(0,\infty)}$ Abstraction for \emph{rq}, $\mathbf{(0,1)}$ for \emph{fq}} \\
We explore a more contextually specific level of abstraction for the $rq$.
Intuitively, for every pair $(sw,pkt)$ in $rq$, if the controller program is m-sensitive to $ctrl(sw,pkt,cs)$ then we over-approximate its instances in $rq$ to $\infty$; otherwise the occurrences are under-approximated to 1. For $fq$ we apply $(0,1)$ abstraction.\\
We write $approx(s)$ to denote the state that is obtained from $s$ after under/over-approximating the instances in the $rq$ and all $fq$-s, where for every state $s \in S$, for every $sw \in Switches$, and non-zero instances of $(sw,pkt) \in s.\gamma.rq$, and $(pkt, pts) \in s.\delta(sw).fq$, $approx(s)$ is defined as:

\begin{itemize}
	\item $over(s.\gamma.rq)(sw,pkt) \otimes under(s.\delta(sw).fq)(pkt, pts)$ if {\sc cp} is m-sensitive to $(sw,pkt)$
	\item $under(s.\gamma.rq)(sw,pkt) \otimes under(s.\delta(sw).fq)(pkt, pts)$,  otherwise
\end{itemize}
where $\otimes$ denotes simultaneous operations in buffers in a state.
\ignore{
\[
approx(s) =
\left\{
\begin{aligned}
&over(s.\gamma.rq)(sw,pkt)    &~\text{if {\sc cp} is m-sensitive to $(sw,pkt)$}& \\
&under(s.\gamma.rq)(sw,pkt)  &~\text{if {\sc cp} is not m-sensitive to $(sw,pkt)$} &\\
&under(s.\delta(sw).fq)(pkt, pts)  &~\text{  }&
\end{aligned}
\right.
\]
}
Let
$\widetilde{Ctrl}$ the set of all $ctrl(sw,pkt,cs)$ actions such that the {\sc cp} is m-sensitive to $(sw,pkt)$.
Given a context $\textsc{ctx}=(sdn_i, \varphi)$ and a transition system $\mathcal{M}(sdn_i)  = (S, A, \hookrightarrow, s_0, AP, L)$, we define
$\mathcal{M}_{rq}  = (S_{rq}, A_{rq}, \hookrightarrow_{rq}, s_0, AP_{rq}, L_{rq} )$, where
\[
S_{rq} =
\{approx(s)  \mid s \in S  \}
\]
$A_{rq} = A$, $AP_{rq} = AP$,
$L_{rq} = L$, and for $s,s' \in S_{rq}$, $s \xhookrightarrow{\alpha}_{rq} s'$ is defined as:
\begin{align*}\label{rul:rq}
\infer [$R$ ^{s_0}]{approx(s_0) \xhookrightarrow[]{\alpha}_{rq} approx(s') }  {s_0 \xhookrightarrow[]{\alpha} s'     } \
\\[10pt]
\infer [$R$_1 ^{(0,\infty)}]{approx(s) \xhookrightarrow[]{\widetilde{ctrl}(sw,pkt,cs)}_{rq} approx(s')[m_{rq}(pkt) := 1] }  {s \xhookrightarrow[]{\widetilde{ctrl}(sw,pkt,cs)} s'   ~\land pkt \notin^1 s'.\gamma.rq  } \
\\[10pt]
\infer [$R$_2 ^{(0,\infty)}]{approx(s')[m_{rq}(pkt) := 1] \xhookrightarrow[]{\alpha}_{rq} approx(s'') }  {s \xhookrightarrow[]{\widetilde{ctrl}(sw,pkt,cs)} s' \xhookrightarrow[]{\alpha} s''  ~\land pkt \notin^1 s'.\gamma.rq  ~\land \alpha \notin  \widetilde{Ctrl} } \
\\[10pt]
\infer [$R$^{(0,1)}]{approx(s') \xhookrightarrow[]{\alpha_2}_{rq} approx(s'') }  {s \xhookrightarrow[]{\alpha_1} s_1 \xhookrightarrow[]{\alpha_2} s_2   ~\land    \bigwedge\limits_{i=1,2} \alpha_i = \widetilde{ctrl}(sw_i,pkt_i, cs_i)  \implies pkt_i \in^1 s_i.\gamma.rq}   \
\ignore{
\\[10pt]
\infer [$R.$ ~rq^{(0,1)}]{s \xhookrightarrow[]{nomatch(sw,pkt)}_{rq} s'[m_{rq}(pkt) := 1] }  {s \xhookrightarrow[]{nomatch(sw,pkt)} s'     } \
\\[10pt]
\infer [$R.$ ~rq^{(0,\infty)}]{s \xhookrightarrow[]{\widetilde{ctrl}(sw,pkt,cs)}_{rq} s'[m_{rq}(pkt) := 1] }  {s \xhookrightarrow[]{\widetilde{ctrl}(sw,pkt,cs)} s'  } \
\\[10pt]
\infer [$R.$ ~rq]{s \xhookrightarrow[]{\alpha}_{rq} s'  }  {s \xhookrightarrow[]{\alpha} s'  ~\land \alpha \notin (Nomatch \cup \widetilde{Ctrl}  )   } \
}
\end{align*}
where
$s[m_{rq}(pkt) := 1]$ stands for the state obtained from $s$ by updating the number of instances (multiplicity) of $pkt$ in $rq$ to $1$, and $\in^1$ is predicate that means `occurs at least once'.\\
\noindent Intuitively, the rules upper bound the size of $rq$ and $fq$ such that only one concrete instance can occur for each element: all other instances of the same object are abstracted away.
The second and third rule deal also with all the $\widetilde{ctrl}$-actions which are visible. They abstract any concrete instance $\widetilde{pkt}$ for the packets the program is sensitive to by over-approximating them to $\infty$, ensuring that $\widetilde{pkt} \in^1 \gamma.rq  \implies \Box (\widetilde{pkt} \in^1 \gamma.rq ) $: a non-deletable concrete instance represents $\infty$ abstract instances.

\noindent It is worth noting that the two first rules which deal with $(0,\infty)$ abstraction do not match the safe actions. This is important for the cycle condition in Thm.\ref{thm:POR} to hold.

\noindent For the sake of generality, for every transition $r \xhookrightarrow[]{\alpha} s$ we extend $approx(s)$ to:
\[
\small
\overline{approx}(s) =
\begin{cases}
approx(s)[m_{rq}(pkt) := 1]    &\text{if $\alpha = \widetilde{ctrl}(sw,pkt,cs) \land pkt \notin^1 s.\gamma.rq $} \\
approx(s)  &otherwise
\end{cases}
\]
Then, the above rules can be collapsed into a single one:
\[
\infer [$R$ ^{(0,1,\infty)}]{\overline{approx}(s) \xhookrightarrow[]{\alpha}_{rq} \overline{approx}(s') }  {s \xhookrightarrow[]{\alpha} s'    } \
\]
\begin{thm}[Property preserving for $rq, fq$ -Abstraction]
	\label{thm:rq}
	If $\mathcal{M}_{rq} \models \Box \varphi$ then $\mathcal{M} \models \Box \varphi$.
\end{thm}

\begin{proof}

	Let $\rho = s_0 \xhookrightarrow[]{\alpha_1} s_1  \xhookrightarrow[]{\alpha_2} ... $ an initial run in $\mathcal{M}$.
	We will attempt to construct a stutter equivalent run $\rho_{rq}$ in $\mathcal{M}_{rq}$.
We apply the rule R$^{(0,1,\infty)}$ for all transitions
in $\rho$, whence
	$\rho_{rq} = \overline{approx}(s_0) \xhookrightarrow[]{\alpha_1}_{rq} \overline{approx}(s_1)  \xhookrightarrow[]{\alpha_2}_{rq} ... $.

\ignore{
	Let $ctrl(sw,pkt,s.\gamma.cs)$ enabled in $s$ by the first $nomatch(sw,pkt)$ in $\rho$.
	From Fig. \ref{graph:depend} it can be inferred that any $nomatch(sw,pkt)$ in $\rho$ triggers a chain of actions which starts with an unrolling pattern of the form:\\

	\includegraphics[scale=.5]{figures/nomatch.pdf}\\
	If the controller is not sensitive to $(sw,pkt)$, then every other $nomatch(sw,pkt)$ in $\rho$ after the first one will stop triggering new transitions beyond the highlighted path, due to the fact that the $cq$ and $pq$ are abstracted by $(0,\infty)$ and as such there is no change of the state caused by the unhighlighted transitions.\\

	The bounding of the instances of $(sw,pkt)$ in $rq$, to which the controller is not sensitive, allows the enabling of one only instance of $ctrl(sw,pkt,cs)$ while all other $ctrl(sw,pkt,cs)$ actions, which are concurrently enabled with the first one, are discarded. By extension, the respective $fwd$ actions which are enabled by $ctrl(sw,pkt,cs)$ in $\mathcal{M} $, are disregarded in $\mathcal{M}_{rq} $. Thus, the first rule removes the $ctrl(sw,pkt,cs)$ and $fwd(sw,pkt,pts)$ which are caused by a $nomatch(sw,pkt)$ which is not the first in $\rho$. In the following we will show that by disregarding these threads no observable behaviour is lost.
	Let
	\begin{flalign}
	\rho' = & s \xhookrightarrow[]{nomatch(sw,pkt)} ...   s_i \xhookrightarrow[]{\alpha_{i+1}} s_{i+1} \xhookrightarrow[]{ctrl(sw,pkt,s_{i+1}.\gamma.cs)} s_{i+2} \xhookrightarrow[]{\alpha_{i+3}} s_{i+3}...\notag&\\
	 & s_k \xhookrightarrow[]{\alpha_{k+1}} s_{k+1} \xhookrightarrow[]{fwd(sw,pkt,pts)} s_{k+2} \xhookrightarrow[]{\alpha_{k+3}} s'&
	\end{flalign}
	be a subtrace of $\rho$ which shows the states and actions which are affected by the rules: these are related with the transitions enabled by the execution of a $nomatch(sw,pkt)$ which comes after another concurrently enabled $nomatch(sw,pkt)$ in $\rho$. By applying the first rule we get the following subtrace in $\mathcal{M}_{rq} $:
\begin{flalign}
	\rho_{rq}' = &	s \xhookrightarrow[]{nomatch(sw,pkt)} ...   s_i \xhookrightarrow[]{\alpha_{i+1}} s_{i+1}  \xhookrightarrow[]{\alpha_{i+3}} s_{i+3}...
	 s_k \xhookrightarrow[]{\alpha_{k+1}} s_{k+1} \xhookrightarrow[]{\alpha_{k+3}} s'&
	\end{flalign}
	The states $s_{i+2}$ and $s_{k+2}$ which are collapsed, have the same labelling as the precursors because the atomic propositions can not assert about elements in the $rq$ and $fq$ (while $pq$s in this care are $(0,\infty)$-abstracted both for $sw$ and the switch the $fwd$ action adds $pkt$ to. Additionally, as analysed above, no other transitions are enabled or disabled as a result of ignoring copies of $ctrl$ and $fwd$ in $\rho'$.
}
\noindent There is a one-to-one correspondence between the transitions in $\rho$ and $\rho_{rq}$, while every state $s_i$ in $\rho$ differs from the corresponding state $\overline{approx}(s_i)$ in $\rho_{rq}$ only in the multiplicities of the objects in $rq$ and $fq$. Since the properties in our specification language do not assert about these buffers, it follows immediately that the labelling of the states for both $\rho$ and $\rho_{rq}$ is identical, i.e., $L(\rho) = L(\rho_{rq})$.

\end{proof}

Similarly, we apply contextual abstraction for $brq$; similar proofs can be carried out.
}

\ignore{

\clearpage

\noindent \textbf{Merging of safe actions.} In the following we consider further reductions relying on the fact that one can safely merge every transition of a safe action with its precursory enabling one.

\noindent Let $\mathit{en-}\check{\alpha}$ denote the enabler action of $\check{\alpha}$, and $merge(\mathit{en-}\check{\alpha},\check{\alpha})$ the successive execution of $\mathit{en-}\check{\alpha}$ and $\check{\alpha}$.

\noindent We start with the following observations which follow directly from the definition of the  semantics of the actions:
\begin{enumerate}
	\item Every safe action $\check{\alpha}$ (see the first column of Table~\ref{tab:safeness}) in a run has a unique enabling action $\mathit{en-}\check{\alpha}$.
	\item if $\alpha$ enables $\check{\beta_1}$ and $\check{\beta_1}$ enables $\check{\beta_2}$ then $merge(\alpha,\check{\beta_1})$ enables $\check{\beta_2}$. This covers the cases where an action is both safe and safe-enabler. For instance, in the sequence $\mathit{nomatch-ctrl-fwd}$ which refers to the same \emph{PacketIn} message, $\mathit{ctrl}$ may be both.
	\item if $\alpha$ enables simultaneously $\check{\beta_1}, \check{\beta_2},\check{\beta_3}...$, then $merge(\alpha,\check{\beta_1})$ enables $\check{\beta_2}, \check{\beta_3}..$. This covers the case when a $\mathit{ctrl}$ action enables multiple safe $\mathit{fwd}$.
\end{enumerate}

\begin{thm}[Merging of safe actions]
	\label{thm:merge} Let $\mathcal{M}^\mathit{ample}_{(\lambda,\textsc{cp})} = (S_a, A, \hookrightarrow\mathrel{\mkern-14mu}\rightarrow, s_0, AP, L_a)$ be the optimised SDN network model from Thm.~\ref{thm:POR}.
	By merging safe actions with their unique enabling action, the transition system
	$\mathcal{M}_{(\lambda,\textsc{cp})}^{merge}  = (S_m, A_m, \hookrightarrow_m, s_0, AP, L_m)$
	is obtained, which is induced by the transition relation $\hookrightarrow_m$ defined by the following rules:

	\begin{itemize}[label=$\blacktriangleright$]
		\item recursively, for every safe-enabler action $\mathit{en-}\check{\alpha} \in A$:
		\\\\\\
		\begin{equation*}\label{rul:merge1}
		\infer[ ]{ \begin{matrix} \\ \vspace{-.5pc} \\
			s \xrightarrow[]{\mathit{merge}(\mathit{en-}\check{\alpha},\check{\alpha})}_m   u
			\text{ \raisebox{.5pc}{ \begin{rotate}{60} $\xhookrightarrowdbl[]{\xi_i}  t_i $\end{rotate}  }  }
			\!\!\!\!\!\!\!\!\!\!\! \text{ \raisebox{-.1pc}{ \begin{rotate}{-60} $\xhookrightarrowdbl[]{\psi_j}  u_j $\end{rotate}  }  }
			\end{matrix} ~~~
		}
		{
			\begin{matrix}
			s \xhookrightarrowdbl[]{\mathit{en-}\check{\alpha}} t     \!\! \text{ \raisebox{.7pc}{ \begin{rotate}{60} $\xhookrightarrowdbl[]{\xi_i}  t_i $\end{rotate}  }  }       \!\!\!\!\!\!    \xhookrightarrowdbl[]{\check{\alpha}} u
			\!\!\! \text{ \raisebox{-.1pc}{ \begin{rotate}{-60} $\xhookrightarrowdbl[]{\psi_j}  u_j $\end{rotate}  }  }
			\\\\\\ \end{matrix}
		} \
		\quad\quad
		\infer[ ]{ \begin{matrix} \\ \vspace{-.5pc} \\
			s \xrightarrow[]{\mathit{merge}(\mathit{en-}\check{\alpha},\check{\alpha})}_m   u
			\text{ \raisebox{.5pc}{ \begin{rotate}{60} $\xhookrightarrowdbl[]{\xi_i}  t_i $\end{rotate}  }  }
			\!\!\!\!\!\!\!\!\!\!\! \text{ \raisebox{-.1pc}{ \begin{rotate}{-60} $\xhookrightarrowdbl[]{\psi_j}  u_j $\end{rotate}  }  }
			\end{matrix} ~~~
		}
		{
			\begin{matrix}
			s \xrightarrow[]{\mathit{en-}\check{\alpha}}_m  t     \!\! \text{ \raisebox{.7pc}{ \begin{rotate}{60} $\xhookrightarrowdbl[]{\xi_i}  t_i $\end{rotate}  }  }       \!\!\!\!\!\!    \xhookrightarrowdbl[]{\check{\alpha}} u
			\!\!\! \text{ \raisebox{-.1pc}{ \begin{rotate}{-60} $\xhookrightarrowdbl[]{\psi_j}  u_j $\end{rotate}  }  }
			\\\\\\ \end{matrix}
		} \
		\end{equation*}
		\\\\\\
		\item for $\alpha \in A$ not safe-enabler and not safe:
		\begin{equation*}\label{rul:merge2}
		\infer{s \xrightarrow[]{\alpha}_m s' }{s \xhookrightarrowdbl[]{\alpha} s' }
		\end{equation*}
	\end{itemize}
	where
	$A_m= A\setminus\{  \mathit{en-}\check{\alpha}, \check{\alpha}  \} \cup \{ \mathit{merge}(\mathit{en-}\check{\alpha},\check{\alpha}) \}$,
	$S_m$ consists of those states that are reachable (under $\rightarrow_m$) from $s_0$, and $L_m(s) = L(s)$ for every $s \in S_m$.
	Actions $\xi_i, \psi_j$ are representatives for all enabled actions in states $t$ and $u$, respectively.
	%
	\ignore{
		$\mathcal{M}^\mathit{merge}_{(\lambda,\mathrm{CP})} = (S, A_m, \rightarrow_m, s_0, AP, L)$   where  and $ \rightarrow_m$ is defined as follows:
		\[ \infer[\mbox{\small ~$\textup{if}~pre\!-\!\check{\alpha}(\cdot) \in Enable(\check{\alpha}(\cdot))$  } ]{s \xrightarrow[]{\mathit{merge-}\check{\alpha}(\cdot)}_m s'' }{s \xhookrightarrowdbl[]{\mathit{pre-}\check{\alpha}(\cdot)} s'  \xhookrightarrowdbl[]{\check{\alpha}(\cdot)} s''  } \
		\qquad\qquad
		\infer{s \xrightarrow[]{\alpha(\cdot)}_m s' }{s \xhookrightarrowdbl[]{\alpha(\cdot)} s' }
		\]
	}
	Then, it holds that $\mathcal{M}^\mathit{merge}_{(\lambda,\textsc{cp})} \stutt \mathcal{M}^{\mathit{ample}}_{(\lambda,\textsc{cp})}$.
\end{thm}

\noindent Intuitively, the first two rules merge each enabler rule with its enablee, progressively: as per the observations 2 and 3 above, they are recursively invoked on the merged action of the reduced transition system from earlier steps.

\begin{proof}

	The proof is immediate from the fact that any safe action $\check{\alpha}$ can disable neither of $\xi_i, \psi_j$, so any $\xi_i, \psi_j$ remains enabled in $u$.
\end{proof}

}
\section{Conclusion}
\label{conclusion}

We have shown that an OpenFlow compliant SDN model, with the right optimisations, can be model checked to discover subtle real-world bugs. We proved that MOCS\ can capture real-world bugs in a more complicated semantics without sacrificing performance.

But this is not the end of the line. One could automatically compute equivalence classes of packets that cover all behaviours (where we still computed manually). To what extent the size of the topology can be restricted to find bugs in a given controller is another interesting research question, as is the analysis of the number and length of interleavings necessary to detect certain bugs. In our examples, all bugs were found in less than a second.

\section{Experimental Evaluation}
\label{experimental-evaluation}

In this section, we experimentally evaluate MOCS\ by comparing it with the state of the art, in terms of performance (verification throughput and memory footprint) and model expressivity. We have implemented MOCS\ in {\sc Uppaal} \cite{UPPAAL} as a network of parallel automata for the controller and network switches, which communicate asynchronously by writing/reading packets to/from queues that are part of the model discussed in \S \ref{sec:modelSDN}. As discussed in \S \ref{sec:optimisations}, this is implemented by directly manipulating the packet and rule indices.

Throughout this section we will be using three examples of network controllers: (1) A \emph{stateless firewall} (\S \ref{appendix:CP}-\ref{rq1-alg11}) requires the controller to install rules to network switches that enable them to decide whether to forward a packet towards its destination or not; this is done in a stateless fashion, i.e. without having to consider any previously seen packets. For example, a controller could configure switches to block all packets whose destination {\sc tcp}  port is {\sc ssh}. (2) A \emph{stateful firewall} (\S \ref{appendix:CP}-\ref{rq1-alg12}) is similar to the stateless one but decisions can take into account previously seen packets. A classic example of this is to allow bi-directional communication between two end-hosts, when one host opens a {\sc tcp} connection to the other. Then, traffic flowing from the other host back to the connection initiator should be allowed to go through the switches on the reverse path. (3) A \emph{MAC learning application} (\S \ref{appendix:CP}-\ref{rq1-alg13}) enables the controller and switches to learn how to forward packets to their destinations (identified with respective MAC addresses). A switch sends a \emph{PacketIn} message to the controller when it receives a packet that it does not know how to forward. By looking at this packet, the controller learns a mapping of a source switch (or host) to a port of the requesting switch. It then installs a rule (by sending a \emph{FlowMod} message) that will allow that switch to forward packets back to the source switch (or host), and asks the requesting switch (by sending a \emph{PacketOut} message) to flood the packet to all its ports except the one it received the packet from. This way, the controller eventually learns all mappings, and network switches receive rules that enable them to forward traffic to their neighbours for all destinations in the network.\\

\subsection{Performance Comparison}
\label{performance}

We measure MOCS's performance, and also compare it against Kuai \cite{Kuai}\footnote{Note that parts of Kuai's source code are not publicly available, therefore we implemented it's model in {\sc Uppaal}.} using the examples described above, and we investigate the behaviour of MOCS\ as we scale up the network (switches and clients/servers). We report three metrics: (1) \emph{verification throughput} in visited states per second, (2) number of visited states, and (3) required memory. We have run all verification experiments on an 18-Core iMac pro, 2.3GHz Intel Xeon W with 128GB DDR4 memory.

\noindent\textbf{Verification throughput. }We measure the verification throughput when running a single experiment at a time on one {\sc cpu} core and report the average and standard deviation for the first 30 minutes of each run.
In order to assess how MOCS's different optimisations affect its performance, we report results for the following system variants: (1) MOCS, (2) MOCS\ without POR, (3) MOCS\ without any optimisations (neither POR, state representation), and (4) Kuai. Figure~\ref{fig:throughput} shows the measured throughput (with error bars denoting standard deviation).

\begin{figure}[h]

	\captionsetup{width=.9\textwidth}
	\begin{subfigure}[b]{1\textwidth}
		\captionsetup{width=.8\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/thp_ML.pdf}
		\caption{MAC Learning Switch}
		\label{fig:thpML}
	\end{subfigure}\\\\
	%

	%
	\begin{subfigure}[b]{.61\textwidth}
		\captionsetup{width=1\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/thp_SSH.pdf}
		\caption{Stateless Firewall}
		\label{fig:thpSSH}
	\end{subfigure}%
	%
	\begin{subfigure}[b]{.39\textwidth}
		\captionsetup{width=.9\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/thp_FW.pdf}
		\caption{Stateful Firewall}
		\label{fig:thpFW}
	\end{subfigure}%
	\caption{Performance Comparison -- Verification Throughput}
	\label{fig:throughput}
	\vspace{-.3cm}
\end{figure}

For the MAC learning and stateless firewall applications, we observe that MOCS\ performs significantly better than Kuai for all different network setups and sizes\footnote{\textsf{S}$\times$\textsf{H} in Figures \ref{fig:throughput} to \ref{fig:memory} indicates the number of switches \textsf{S} and hosts \textsf{H}.}, achieving at least double the throughput Kuai does. The throughput performance is much better for the stateful firewall, too. This is despite the fact that, for this application, Kuai employs the unrealistic optimisation where the \emph{barrier} transition forces the immediate update of the forwarding state. In other words, MOCS\ is able to explore significantly more states and identify bugs that Kuai cannot (see \S \ref{subsec:expressivity}).

The computational overhead induced by our proposed PORs is minimal. This overhead occurs when PORs require dynamic checks through the safety predicates described in Table \ref{tab:safeness}. This is shown in Figure~\ref{fig:thpML}, where, in order to decide about the (in)visibility of $\mathit{fwd(sw,pk,pt)}$ actions, a lookup is performed in the history-array of packet \emph{pk}, checking whether the bit which corresponds to switch $sw'$, which is connected with port \emph{pt} of \emph{sw}, is set. On the other hand, if a POR does not require any dynamic checks, no penalty is induced, as shown in Figures~\ref{fig:thpSSH} and \ref{fig:thpFW}, where the throughput when the PORs are disabled is almost identical to the case where PORs are enabled. This is because it has been statically established at a pre-analysis stage that all actions of a particular type are always safe for any argument/state. It is important to note that even when computational overhead is induced, PORs enable MOCS\ to scale up to larger networks because the number of visited states can be significantly reduced, as discussed below.

In order to assess the contribution of the state representation optimisation in MOCS's performance, we measure the throughput when both PORs and state representation optimisations are disabled. It is clear that they contribute significantly to the overall throughput; without these the measured throughput was at least less than half the throughput when they were enabled.

\begin{figure}[h]

	\captionsetup{width=1\textwidth}
	\begin{subfigure}[b]{1\textwidth}
		\captionsetup{width=.8\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/stat_ml.pdf}
		\caption{MAC Learning Switch}
		\label{fig:statesML}
	\end{subfigure}\\\\
	%

	%
	\begin{subfigure}[b]{.75\textwidth}
		\captionsetup{width=1\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/stat_ssh.pdf}
		\caption{Stateless Firewall}
		\label{fig:statesSSH}
	\end{subfigure}%
	%
	\begin{subfigure}[b]{.25\textwidth}
		\captionsetup{width=1\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/stat_fw.pdf}
		\caption{Stateful Firewall}
		\label{fig:statesFW}
	\end{subfigure}%
	\caption{Performance Comparison -- Visited States (logarithmic scale)}
	\label{fig:states}
	\vspace{.4cm}
\end{figure}

\begin{figure}[h]

	\captionsetup{width=1\textwidth}
	\begin{subfigure}[b]{1\textwidth}
		\captionsetup{width=.8\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/mem_ml.pdf}
		\caption{MAC Learning Switch}
		\label{fig:memML}
	\end{subfigure}\\\\
	%

	%
	\begin{subfigure}[b]{.75\textwidth}
		\captionsetup{width=1\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/mem_ssh.pdf}
		\caption{Stateless Firewall}
		\label{fig:memSSH}
	\end{subfigure}%
	%
	\begin{subfigure}[b]{.25\textwidth}
		\captionsetup{width=1\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/mem_fw.pdf}
		\caption{Stateful Firewall}
		\label{fig:memFW}
	\end{subfigure}%
	\caption{Performance Comparison -- Memory Footprint (logarithmic scale)}
	\label{fig:memory}
	\vspace{-.3cm}
\end{figure}

\noindent\textbf{Number of visited states and required memory. }Minimising the number of visited states and required memory is crucial for scaling up verification to larger networks. The proposed partial order reductions (\S \ref{subsec:por}) and identification of packet equivalent classes aim at the former, while packet/rule indexing and bit packing aim at the latter (\S \ref{subsec:state:repr}). In Figure \ref{fig:states}, we present the results for the various setups and network deployments discussed above. We stopped scaling up the network deployment for each setup when the verification process required more than $24$ hours or started swapping memory to disk. For these cases we killed the process and report a topped-up bar in Figures \ref{fig:states} and \ref{fig:memory}.

For the MAC learning application, MOCS\ can scale up to larger network deployments compared to Kuai, which could not verify networks consisting of more than $2$ hosts and $6$ switches. For that network deployment, Kuai visited ${\sim}7$m states, whereas MOCS\ visited only ${\sim}193$k states. At the same time, Kuai required around $48$GBs of memory ($7061$ bytes/state) whereas MOCS\ needed ${\sim}43$MBs ($228$ bytes/state). Without the partial order reductions, MOCS\ can only verify tiny networks. The contribution of the proposed state representation optimisations is also crucial; in our experiments (results not shown due to lack of space), for the $6\times 2$ network setups (the largest we could do without these optimisations), we observed a reduction in state space (due to the identification of packet equivalence classes) and memory footprint (due to packet/rule indexing and bit packing) from ${\sim}7$m to ${\sim}200$k states and from ${\sim}6$KB per state to ${\sim}230$B per state.
For the stateless and stateful firewall applications, resp., MOCS\ performs equally well to Kuai with respect to scaling up.

\subsection{Model Expressivity}
\label{subsec:expressivity}

The proposed model is significantly more expressive compared to Kuai as it allows for more asynchronous concurrency.
To begin with, in MOCS, controller messages sent before a barrier request message can be interleaved with all other enabled actions, other than the control messages sent after the barrier. By contrast, Kuai always flushes all control messages until the last barrier in one go, masking a large number of interleavings and, potentially, buggy behaviour.
Next, in MOCS\, \emph{nomatch, ctrl} and \emph{fwd} can be interleaved with other actions.
In Kuai, it is enforced a mutual exclusion concurrency control policy through the \emph{wait}-semaphore: whenever a \emph{nomatch} occurs the mutex is locked and it is unlocked by the \emph{fwd} action of the thread \emph{nomatch-ctrl-fwd} which refers to the same packet; all other threads are forced to wait.
Moreover, MOCS\ does not impose any limit on the size of the \emph{rq} queue, in contrast to Kuai where only one packet can exist in it.
In addition, Kuai does not support notifications from the data plane to the controller for completed operations as it does not support reply messages and as a result any bug related to the fact that the controller is not synced to data-plane state changes is hidden.\footnote{There are further small extensions; for instance, in MOCS the controller can send multiple \emph{PacketOut} messages (as OpenFlow prescribes).}
Also, our specification language for states is more expressive than Kuai's, as we can use any property in LTL without ``next", whereas Kuai only uses invariants with a single outermost $\Box$.\\
The MOCS extensions, however, are conservative with respect to Kuai, that is we have the following theorem (without proof, which is straightforward):

\begin{thm}[MOCS\ Conservativity]
	\label{thm:inclusiveness}
	Let
	$\mathcal{M}_{(\lambda,\textsc{cp})}  = (S, A, \hookrightarrow, s_0, AP, L)$
	and
	$\mathcal{M}^{\mbox{\tiny{\textit{K}}}}_{(\lambda,\textsc{cp})}   = (S_K, A_K, \hookrightarrow_K, s_0, AP, L)$
	the original SDN models of MOCS\ and Kuai, respectively, using the same topology and controller.
	Furthermore, let $\mathit{Traces}( \mathcal{M}_{(\lambda,\textsc{cp})})$ and
	$\mathit{Traces}(\mathcal{M}^{\mbox{\tiny{\textit{K}}}}_{(\lambda,\textsc{cp})} )$
	denote the set of all initial traces in these models, respectively. Then,
	$
	\mathit{Traces}(\mathcal{M}^{\mbox{\tiny{\textit{K}}}}_{(\lambda,\textsc{cp})} )  \subseteq   \mathit{Traces}( \mathcal{M}_{(\lambda,\textsc{cp})})
	$.
	\end{thm}

\noindent For each of the extensions mentioned above, we briefly describe an example (controller program and safety property) that expresses a bug that is impossible to occur in Kuai.

\noindent\textbf{Control message reordering bug. }Let us consider a stateless firewall in Figure~\ref{fig:prop1} (controller is not shown), which is supposed to block incoming {\sc ssh} packets from reaching the server (see \S \ref{appendix:CP}-\ref{rq1-alg11}). Formally, the safety property to be checked here is $\Box (\forall \mathit{pkt}\, {\in}\,\mathit{S.rcvq} \,.\, \neg \mathit{pkt}.\mathrm{\textsc {ssh}})$. Initially, flow tables are empty. Switch $A$ sends a \emph{PacketIn} message to the controller when it receives the first packet from the client (as a result of a \emph{nomatch} transition). The controller, in response to this request (and as a result of a \emph{ctrl} transition), sends the following \emph{FlowMod} messages to switch $A$; rule \texttt{r1} has the highest priority and drops all {\sc ssh} packets, rule \texttt{r2} sends all packets from port 1 to port 2, and rule \texttt{r3} sends all packets from port 2 to port 1. If the packet that triggered the transition above is an {\sc ssh} one, the controller drops it, otherwise, it instructs (through a \emph{PacketOut} message) $A$ to forward the packet to $S$. A bug-free controller should ensure that \texttt{r1} is installed before any other rule, therefore it must send a barrier request after the \emph{FlowMod} message that contains \texttt{r1}. If, by mistake, the \emph{FlowMod} message for \texttt{r2} is sent before the barrier request, $A$ may install \texttt{r2} before \texttt{r1}, which will result in violating the given property.
MOCS\ is able to capture this buggy behaviour as its semantics allows control messages prior to the barrier to be processed in a interleaved manner.

\ignore{
\begin{figure}[ht]
	\centering
	\captionsetup{width=1\textwidth}
		\includegraphics[width=.45\linewidth]{figures/c_s_2.pdf}
		\caption{A network with two switches}
	\label{fig:prop2}
	\vspace{-.3cm}
\end{figure}
}

\vspace{-.3cm}
\begin{figure}[ht]
	\centering
	\captionsetup{width=1\textwidth}
	\begin{subfigure}[b]{.5\textwidth}
		\captionsetup{width=.8\textwidth}
		\centering
		\includegraphics[width=1\linewidth]{figures/c_s_2.pdf}
		\caption{}
		\label{fig:prop1}
	\end{subfigure}%
	%
	\quad \quad
	%
	\begin{subfigure}[b]{.4\textwidth}
		\captionsetup{width=.8\textwidth}
		\centering
		\includegraphics[width=.86\linewidth]{figures/fw2.pdf}
		\caption{}
		\label{fig:prop2}
	\end{subfigure}%
	\ignore{
		\begin{subfigure}[b]{.33\textwidth}
			\captionsetup{width=.8\textwidth}
			\centering
			\includegraphics[width=.6\linewidth]{figures/fw.pdf}
			\caption{}
			\label{fig:prop3}
		\end{subfigure}%
	}
	\caption{Two networks with  (a) two switches, and  (b) $n$ stateful firewall replicas}
	\label{fig:example:top}
	\vspace{-.3cm}
\end{figure}

\ignore{
\resizebox{1\textwidth}{!}{%
	\begin{minipage}{1.8\textwidth}
\begin{algorithm}[H]
	\DontPrintSemicolon
	\SetKwInOut{Input}{Input}
	\SetKwInOut{Output}{Output}
	\SetKwFunction{FMain}{PacketIn\_handler}
	\SetKwProg{Fn}{void}{:}{}
	\SetAlgorithmName{Controller Program}{}

	\Fn{\FMain{\upshape{\texttt{p}}}}{

		\uIf{\upshape{\texttt{p.prot == SSH}}}{
			\texttt{drop(p)}
		}
		\Else{
			$\texttt{\textcolor{ForestGreen}{rule\_t} r1 = \big \{\{prio = 10\}, \{prot = SSH\}, \{in\_port = *\}, \{forward\_port = drop\}\big \}  }$

			$\mathrlap{\texttt{\textcolor{ForestGreen}{rule\_t} r2 = \big \{\{prio =  ~1\}, \{prot = *~~\},}}\hphantom{\texttt{rule\_t r1 = \big \{\{prio = 10\}, \{prot = SSH\}, }}  \texttt{\{in\_port = 1\}, \{forward\_port = 2  ~ \}\big \}  }$

			$\mathrlap{\texttt{\textcolor{ForestGreen}{rule\_t} r3 = \big \{\{prio =  ~1\}, \{prot = *~~\},}}\hphantom{\texttt{rule\_t r1 = \big \{\{prio = 10\}, \{prot = SSH\}, }}  \texttt{\{in\_port = 2\}, \{forward\_port = 1   ~~\}\big \}  }$\;

			\ForAll{\upshape{\texttt{sw}} $\in$ \upshape{\texttt{Switches}}}{

				\texttt{send\_message\_list}(\texttt{[add(r2),add(r1),b,add(r3)],sw})

			}
		}

	}
	\caption{With control messages reordering bug}
	\label{rq1-alg1}
\end{algorithm}
  \end{minipage}%

}

\noindent\textbf{Wrong nesting level bug. }Consider a correct controller program that enforces that server $S$ (Figure \ref{fig:prop1}) is not accessible through {\sc ssh}. Formally, the safety property to be checked here is $\Box (\forall \mathit{pkt}\, {\in}\, \mathit{S.rcvq} \,.\, \neg \mathit{pkt}.\mathrm{\textsc{ssh}})$. For each incoming \emph{PacketIn} message from switch $A$, it checks if the enclosed packet is an {\sc ssh} one and destined to $S$. If not, it sends a \emph{PacketOut} message instructing $A$ to forward the packet to $S$. It also sends a \emph{FlowMod} message to $A$ with a rule that allows packets of the same protocol (not {\sc ssh}) to reach $S$. In the opposite case ({\sc ssh}), it checks (a Boolean flag) whether it had previously sent drop rules for {\sc ssh} packets to the switches. If not, it sets flag to true, sends a \emph{FlowMod} message with a rule that drops {\sc ssh} packets to $A$ and drops the packet. Note that this inner block does not have an \texttt{else} statement.

A fairly common error is to write a statement at the wrong nesting level (\S \ref{appendix:CP}-\ref{rq1-alg2}). Such a mistake can be built into the above program by nesting the outer \texttt{else} branch in the inner \texttt{if} block, such that it is executed any time an {\sc ssh}-packet is encountered but the {\sc ssh} drop-rule has already been installed (i.e. flag \texttt{f} is true). Now, the {\sc ssh} drop rule, once installed in switch $A$, disables immediately a potential $\mathit{nomatch(A,p)}$ with $p.\mathrm{\textsc{ssh}}=true$ that would have sent packet $p$ to the controller, but if it has not yet been installed, a second incoming {\sc ssh} packet would lead to the execution of the \texttt{else} statement of the inner branch. This would violate the property defined above, as $p$ will be forwarded to $S$\footnote{Here, we assume that the controller looks up a static forwarding table before sending \emph{PacketOut} messages to switches.}.

MOCS\ can uncover this bug because of the correct modelling of the controller request queue  and the asynchrony between the concurrent executions of control messages sent before a barrier.
Otherwise, the second packet that triggers the execution of the wrong branch would not have appeared in the buffer before the first one had been dealt with by the controller. Furthermore, if all rules in messages up to a barrier were installed synchronously, the second packet would be dealt with correctly, so no bug could occur.

\ignore{
\resizebox{.9\textwidth}{!}{%
	\begin{minipage}{1.5\textwidth}
\MyBox{starta}{enda}{red}
\MyBox[-3ex]{startb}{endb}{gray}
\begin{algorithm}[H]

	\DontPrintSemicolon
	\SetKwInOut{Input}{Input}
	\SetKwInOut{Output}{Output}
	\SetKwFunction{FMain}{PacketIn\_handler}
	\SetKwProg{Fn}{void}{:}{}
	\SetAlgorithmName{Controller Program}{}

	\texttt{const \textcolor{ForestGreen}{int} SW} \textcolor{gray}{\tcc*[r]{No. of switches in network}}
	\texttt{const \textcolor{ForestGreen}{int} C} \textcolor{gray}{\tcc*[r]{No. of clients in network}}
	\texttt{\textcolor{ForestGreen}{port\_t} MAC\_table[SW][C]} \textcolor{gray}{\tcc*[r]{Array [SW] of array [C] of switch-ports}}
	\texttt{\textcolor{ForestGreen}{bool} f} $ \gets$ \texttt{\textcolor{violet}{\textbf{false}}} \textcolor{gray}{\tcc*[r]{a global flag to prevent resending same rules}}

	\Fn{\FMain{\upshape{\texttt{p}}}}{

		\texttt{\textcolor{ForestGreen}{rule\_t} rule[SW]} \textcolor{gray}{\tcc*[r]{Initialise an empty array for storage of rules}}
		\texttt{\textcolor{ForestGreen}{rule\_t} rule\_d } \textcolor{gray}{\tcc*[r]{Initialise a rule to be used to drop packet $p$}}

		\uIf{\upshape{\texttt{p.prot ==  SSH \textcolor{violet}{and} p.destIP == client\_3}}}{
			\tikzmark{startb}
			\uIf{\upshape{\texttt{!f}}}{

				$\mathrlap{\texttt{f}}\hphantom{\texttt{rule\_d.fwd\_port}}  \gets   \texttt{\textcolor{violet}{\textbf{true}}}  $ \textcolor{gray}{\tcc*[r]{$p$ is implicitly dropped by not sending a $fwd$}}

				$\mathrlap{\texttt{rule\_d.prio}}\hphantom{\texttt{rule\_d.fwd\_port}} \gets 	\texttt{1} $ \;
				$\mathrlap{\texttt{rule\_d.prot}}\hphantom{\texttt{rule\_d.fwd\_port}} \gets 	\texttt{p.prot} $ \;
				$\mathrlap{\texttt{rule\_d.destIP}}\hphantom{\texttt{rule\_d.fwd\_port}} \gets  \texttt{p.destIP}$ \;

				$\texttt{rule\_d.fwd\_port}	\gets 	\texttt{drop} $      \;

				\ForAll{\upshape{\texttt{sw}} $\in$ \upshape{\texttt{Switches}}}{
					\texttt{send\_message\_list}(\texttt{[add(rule\_d),barrier],sw})   \hfill \tikzmark{endb}

				}
			}
			\tikzmark{starta}
			\Else{

				$\texttt{fwd(p,p.loc.sw, MAC\_table[p.loc.sw][p.destIP])}$ \;
				\ForAll{\upshape{\texttt{sw}} $\in$ \upshape{\texttt{Switches}}}{
					$\mathrlap{\texttt{rule[sw].prio}}\hphantom{\texttt{rule[sw].fwd\_port}} \gets  \texttt{2} $ \;
					$\mathrlap{\texttt{rule[sw].prot}}\hphantom{\texttt{rule[sw].fwd\_port}} \gets  \texttt{p.prot} $ \;
					$\mathrlap{\texttt{rule[sw].destIP}}\hphantom{\texttt{rule[sw].fwd\_port}} \gets  \texttt{p.destIP} $ \;

					$\texttt{rule[sw].fwd\_port} \gets \texttt{MAC\_table[sw][p.destIP]} $	\;

					\texttt{send\_message}(\texttt{add(rule[sw]),sw}) \hfill \tikzmark{enda}
				}
			}
		}
		\Else{
			... \;
		}

	}

	\caption{Wrong nesting level}
	\label{rq1-alg2}
\end{algorithm}
  \end{minipage}%

}

\noindent\textbf{Inconsistent update bug. }OpenFlow's barrier and barrier reply mechanisms allow for updating multiple network switches in a way that enables \emph{consistent packet processing}, i.e., a packet cannot see a partially updated network where only a subset of switches have changed their forwarding policy in response to this packet (or any other event), while others have not done so. MOCS\ is expressive enough to capture this behaviour and related bugs. In the topology shown in Figure \ref{fig:prop1}, let us assume that, by default, switch $B$ drops all packets destined to $S$. Any attempt to reach $S$ through $A$ are examined separately by the controller and, when granted access, a relevant rule is installed at both switches (e.g. allowing all packets from $C$ destined to $S$ for given source and destination ports). Updates must be consistent, therefore the packet cannot be forwarded by $A$ and dropped by $B$. Both switches must have the new rules in place, before the packet is forwarded. To do so, the controller, (\S \ref{appendix:CP}-\ref{rq1-alg3}), upon receiving a \emph{PacketIn} message from the client's switch, sends the relevant rule to switch $B$ (\emph{FlowMod}) along with respective barrier (\emph{BarrierReq}) and temporarily stores the packet that triggered this update. Only after receiving \emph{BarrierRes} message from $B$, the controller will forward the previously stored packet back to $A$ along with the relevant rule. This update is consistent and the packet is guaranteed to reach $S$. A (rather common) bug would be one where the controller installs the rules to both switches and at the same time forwards the packet to $A$. In this case, the packet may end up being dropped by $B$, if it arrives and gets processed before the relevant rule is installed, and therefore the invariant
$\Box \big( [\mathit{drop(pkt,sw)}]  \,.\,  \neg (\mathit{pkt.dest = S)}  \big)$, where $[\mathit{drop(pkt,sw)}]$ is a quantifier that binds dropped packets (see definition in \S \ref{appendix:CP}-\ref{rq1-alg3}), would be violated. For this example, it is crucial that MOCS\ supports barrier response messages.

\ignore{
\subsubsection{Stateful Inspection Firewall}

 This controller program \cite{GENI,Kuai}  performs packets filtering and acknowledges the context of TCP connections.
For example, when a connection is initiated by a client (web browser) sending an HTTP request message to the web server (TCP port 80 is the standard port the server is listening on), the latter will initiate a return connection back to the client on an logical ephemeral TCP port (say 1030) that the client had created upon initiating the request, and which is allocated for short term use. The firewall application therefore should automatically open the ephemeral port for this return connection, and only then the server can access the client.
Such a connection need to be stored by the controller and is represented by a mapping between TCP/IP socket pairs. A socket is an endpoint consisting of the IP address and the TCP (or UDP) port number. Hence the controller needs to store records { \tt\{srcIP= $c_1$,
		\tt srcTCPpt= $p_1$,
		\tt destIP= $c_2$,
		\tt destTCPpt= $p_2$\tt\}}
that represent address and port of client (or \texttt{src}) and server (\texttt{dest}), respectively.
The controller holds this information in a so-called \emph{whitelist} (stored in variable \texttt{wl}). Packets are supposed to have corresponding fields \texttt{srcIP} , \texttt{srcTCPpt}, \texttt{destIP}, \texttt{destTCP} matching those of the whitelist entries.
If the controller receives a packet whose destination matches a permit entry in the stored whitelist of connections, then the controller all at once
\begin{inparaenum}[(i)]
	\item creates and sends to the switches two symmetrical access rules, $r_1$ and $r_2$ (with the source and destination being used interchangeably) for allowing bi-directional access (as shown in the trace below), followed by a barrier $b(xid)$,
	\item updates its connections table (state) accordingly, and
	\item forwards the packet to its destination socket.

\end{inparaenum}
If the packet does not match a whitelisted pattern, then a rule $r_{drop}$ that discards the packet is created and installed in the switch(es).
 \\
\resizebox{1\textwidth}{!}{%
	\begin{minipage}{1.8\textwidth}
		\begin{algorithm}[H]

			\DontPrintSemicolon
			\SetKwInOut{Input}{Input}
			\SetKwInOut{Output}{Output}
			\SetKwFunction{FMain}{PacketIn\_handler}
			\SetKwProg{Fn}{void}{:}{}
			\SetAlgorithmName{Controller Program}{}

				\texttt{const whitelist} == \{(c1, p1, c2, p2)\} \textcolor{gray}{\tcc*[r]{whitelisted connections}}
					\texttt{\textcolor{ForestGreen}{port\_t} MAC\_table[SW][C]} \textcolor{gray}{\tcc*[r]{Array [SW] of array [C] of switch-ports}}

			\Fn{\FMain{\upshape{\texttt{p}}}}{
				$\texttt{conn $\gets$ (p.srcIP, p.srcTCPpt, p.destIP , p.destTCPpt)}$\;
				\uIf{\upshape{\texttt{conn $\in$ whitelist}}}{
					\texttt{fwd(p, MAC\_table[p.sw][p.destIP], p.sw)}\;
					\texttt{ r1 $\gets$ \big \{\{srcIP $\gets$ p.srcIP~\},  \{srcTCPpt $\gets$ p.srcTCPpt~\}, \{destIP $\gets$ p.destIP\}, \{destTCPpt $\gets$ p.destTCPpt\}, \;
						~~~~~~~~\{fwd\_port $\gets$ MAC\_table[p.sw][p.destIP] \}, \{prio $\gets$ 2\} \big \}  }\;

					\texttt{ r2 $\gets$ \big \{\{srcIP $\gets$ p.destIP\}, \{srcTCPpt $\gets$ p.destTCPpt\}, \{destIP $\gets$ p.srcIP~\}, \{destTCPpt $\gets$ p.srcTCPpt~\},\;
						~~~~~~~~\{fwd\_port $\gets$ MAC\_table[p.sw][p.srcIP] \}, \{prio $\gets$ 2\} \big \}  }\;
					\ForAll{\upshape{\texttt{sw}} $\in$ \upshape{\texttt{Switches}}}{
						\texttt{send\_message(add(r1),sw)}\;
						\texttt{send\_message(add(r2),sw)}\;
						\texttt{send\_message(barrier(xid $\gets$ 1),sw)}
					}

				}
				\Else{
					\texttt{drop(p)}\;
					\texttt{ r\_drop $\gets$ \big \{\{srcIP $\gets$ p.srcIP~\},  \{srcTCPpt $\gets$ p.srcTCPpt~\}, \{destIP $\gets$ p.destIP\}, \{destTCPpt $\gets$ p.destTCPpt\},\;
						~~~~~~~~~~~~\{fwd\_port $\gets$ drop \}, \{prio $\gets$ 1\} \big \}  }\;
					\ForAll{\upshape{\texttt{sw}} $\in$ \upshape{\texttt{Switches}}}{
						\texttt{send\_message}(\texttt{add(r\_drop),sw})
					}
				}
			}
			\caption{PacketIn handler for the Stateful Firewall}
			\label{rq1-alg3}
		\end{algorithm}
	\end{minipage}%

\\
\resizebox{1\textwidth}{!}{%
	\begin{minipage}{1.8\textwidth}
		\begin{algorithm}[H]

			\DontPrintSemicolon
			\SetKwInOut{Input}{Input}
			\SetKwInOut{Output}{Output}
			\SetKwFunction{FMain}{Barrier\_reply\_handler}
			\SetKwProg{Fn}{void}{:}{}
			\SetAlgorithmName{Controller Program}{}

			\texttt{bool flows[C][ip\_port\_t][C][ip\_port\_t][SW]} \textcolor{gray}{\tcc*[r]{flows array is ghost variable for checking property}}

			\Fn{\FMain{\upshape{\texttt{xid, sw}}}}{
				\uIf{\upshape{\texttt{xid == 1}}}{
        			\texttt{flows[c1][p1][c2][p2][sw] $\gets$ \textcolor{violet}{\textbf{true}}}\;
					\texttt{flows[c2][p2][c1][p1][sw] $\gets$ \textcolor{violet}{\textbf{true}}}

				}
			}
			\caption{Barrier reply handler for the Stateful Firewall}
			\label{rq1-alg4}
		\end{algorithm}
	\end{minipage}%

\\

\noindent The safety property is as in \cite{Kuai} and asserts that \textit{no packet is denied access to its destination socket if it is whitelisted or another packet with swapped sockets, which is whitelisted, has already been granted access.}\\
Now consider the topology as in Fig.~\ref{fig:prop3} and that controller is started with whitelist \texttt{wl}  $= \{(c_1, p_1, c_2, p_2)\}$, and fix packets and rules as follows:

	\begin{minipage}{.6\textwidth}
{\scriptsize
	\begin{alignat*}{2}
	&\mathtt {
		pk_1 =
		\arraycolsep=1.4pt\def1{1}
		%
		\tiny \left\{\begin{array}{rl}
		\tt srcIP =&\tt c_1 \\
		\tt srcTCPpt=&\tt p_1\\
		\tt destIP =&\tt c_2 \\
		\tt destTCPpt=&\tt p_2
		\end{array} \right\}~
	}
	\mathtt {
		pk_2 =
		%
		\tiny \left\{ \begin{array}{rl}
		\tt	srcIP =& \tt c_2 \\
		\tt srcTCPpt=&\tt p_2\\
		\tt destIP =&\tt c_1 \\
		\tt destTCPpt=&\tt p_1
		\end{array} \right\}~
	}
 \mathtt {
		r_1 =
		%
		\tiny \left\{ \begin{array}{rl}
		\tt srcIP =&\tt c_1 \\
		\tt srcTCPpt=&\tt p_1\\
		\tt destIP =&\tt c_2 \\
		\tt destTCPpt=&\tt p_2\\
		\tt forward\_port=&\tt 2\\
		\tt prio=&\tt 2
		\end{array} \right\}~
	}
	\mathtt {
		r_2 =
		%
		\tiny \left\{ \begin{array}{rl}
		\tt srcIP =&\tt c_2 \\
		\tt srcTCPpt=&\tt p_2\\
		\tt destIP =&\tt c_1 \\
		\tt destTCPpt=&\tt p_1\\
		\tt forward\_pt=&\tt 1\\
		\tt prio=&\tt 2
		\end{array} \right\}
	}\\
&\mathtt {
	r_{drop} =
	%
	\tiny \left\{ \begin{array}{rl}
	\tt srcIP \neq&\tt c_1 \\
	\tt srcTCPpt\neq&\tt p_1\\
	\tt destIP \neq&\tt c_2 \\
	\tt destTCPpt\neq&\tt p_2\\
	\tt forward\_port=&\tt drop\\
	\tt prio=&\tt 1
	\end{array} \right\}
}
	\end{alignat*}
}
	\end{minipage}%
\iffalse
	\begin{minipage}{.4\textwidth}
		\centering
		\includegraphics[scale=.35]{figures/fwsingle.pdf}
		\caption{FW $1 \times 2$}
		\label{fig:fw1x2}
	\end{minipage}
\fi
\iffalse
{\scriptsize
\begin{alignat*}{2}
&\mathtt {
	pk_1 =
	\arraycolsep=1.4pt\def1{1}
	%
	\tiny \left\{\begin{array}{rl}
	\tt srcIP =&\tt c_1 \\
	\tt srcTCPpt=&\tt p_1\\
	\tt destIP =&\tt c_2 \\
	\tt destTCPpt=&\tt p_2
	\end{array} \right\},~
}
&\mathtt {
	pk_2 =
	%
	\tiny \left\{ \begin{array}{rl}
	\tt	srcIP =& \tt c_2 \\
	\tt srcTCPpt=&\tt p_2\\
	\tt destIP =&\tt c_1 \\
	\tt destTCPpt=&\tt p_1
	\end{array} \right\},~
}
&
\\
&\mathtt {
	r_1 =
	%
	\tiny \left\{ \begin{array}{rl}
	\tt srcIP =&\tt c_1 \\
	\tt srcTCPpt=&\tt p_1\\
	\tt destIP =&\tt c_2 \\
	\tt destTCPpt=&\tt p_2\\
	\tt forward\_port=&\tt 2\\
	\tt prio=&\tt 2
	\end{array} \right\},~
}
&\mathtt {
	r_2 =
	%
	\tiny \left\{ \begin{array}{rl}
	\tt srcIP =&\tt c_2 \\
	\tt srcTCPpt=&\tt p_2\\
	\tt destIP =&\tt c_1 \\
	\tt destTCPpt=&\tt p_1\\
	\tt forward\_pt=&\tt 1\\
	\tt prio=&\tt 2
	\end{array} \right\},~
}
&\mathtt {
	r_{drop} =
	%
	\tiny \left\{ \begin{array}{rl}
	\tt srcIP \neq&\tt c_1 \\
	\tt srcTCPpt\neq&\tt p_1\\
	\tt destIP \neq&\tt c_2 \\
	\tt destTCPpt\neq&\tt p_2\\
	\tt forward\_port=&\tt drop\\
	\tt prio=&\tt 1
	\end{array} \right\}
}
\end{alignat*}
}
\fi%

Then  trace in Fig.~\ref{fig:trace} witnesses a violation of the above correctness property:

\begin{figure}
\begin{align*}
\arraycolsep=1.4pt\def1{1}
&
\mbox{\Large\( 	s 	\)}^0
\xhookrightarrow []{  \tt nomatch(sw, pk_2)  }
\mbox{\Large\( 	s 	\)}^1
\xhookrightarrow []{  \tt ctrl(pk_2)  }
\mbox{\Large\( 	s 	\)}^2
\xhookrightarrow []{  \tt add(sw, r_{drop})}
\mbox{\Large\( 	s 	\)}^3
\xhookrightarrow []{  \tt nomatch(sw, pk_1)  }
\mbox{\Large\( 	s 	\)}^4
\xhookrightarrow []{  \tt ctrl(pk_1) }
\\
&
\mbox{\Large\( 	s 	\)}^5
\xhookrightarrow []{  \tt match(sw, pk_2, r_{drop})  }
\LARGE \textcolor{red}{\frownie}
\tag{C-E.g. 2}
\end{align*}
\caption{Violating trace for stateful firewall example}
\label{fig:trace}
\end{figure}

\begin{figure}
\begin{align*}
\arraycolsep=1.4pt\def1{1}
&
\mbox{\large\( 	s 	\)}^0_{

	\tiny \left[ \begin{array}{rl}
	\tt pIb =&\tt \{\} \\
	\tt sw.cb =&\tt [~]\\
	\tt sw.pOb =&\tt \{\}\\
	\tt flows=\top = &\tt \{\}
	\end{array} \right]
	%
}
\xhookrightarrow []{  \tt nomatch(sw, pk_1)  }
\mbox{\large\( 	s 	\)}^1_{

	\tiny \left[ \begin{array}{rl}
	\tt pIb =&\tt \{pk_1\} \\
	\tt sw.cb =&\tt [~]\\
	\tt sw.pOb =&\tt \{\}\\
	\tt flows=\top = &\tt \{\}
	\end{array} \right]
	%
}
\xhookrightarrow []{  \tt ctrl(pk_1)  }
\mbox{\large\( 	s 	\)}^2_{

	\tiny \left[ \begin{array}{rl}
	\tt pIb =&\tt \{\} \\
	\tt sw.cb =&\tt [\{r_1, r_2\}, b]\\
	\tt sw.pOb =&\tt \{pk_1\}\\
	%
	\tt flows=\top = &
	\left\{ \begin{array}{l}
			\tt (r_1,sw), \\
			\tt (r_2,sw)
	\end{array} \right\}
	%
	\end{array} \right]
	%
}
\xhookrightarrow []{  \tt nomatch(sw, pk_2)}
\\\\
&
\mbox{\large\( 	s 	\)}^3_{

	\tiny \left[ \begin{array}{rl}
	\tt pIb =&\tt \{pk_2\} \\
	\tt sw.cb =&\tt [\{r_1, r_2\}, b]\\
	\tt sw.pOb =&\tt \{pk_1\}\\
	\tt flows=\top = &
		\left\{ \begin{array}{l}
			\tt (r_1,sw), \\
			\tt (r_2,sw)
		\end{array} \right\}
	\end{array} \right]
	%
}
\xhookrightarrow []{  \tt ctrl(pk_2) }
\mbox{\large\( 	s 	\)}^4_{

	\tiny \left[ \begin{array}{rl}
	\tt pIb =&\tt \{\} \\
	\tt sw.cb =&\tt [\{r_1, r_2\}, b,\{r_{drop}\}]\\
	\tt sw.pOb =&\tt \{pk_1,pk_2\}\\
	\tt flows=\top = &
		\left\{ \begin{array}{l}
			\tt (r_1,sw), \\
			\tt (r_2,sw)
		\end{array} \right\}
	\end{array} \right]
	%
}
\xhookrightarrow []{ \tt fwd(sw, pk_2, drop) }
\LARGE \textcolor{red}{\frownie}
\tag{C-E.g. 1}
\end{align*}
\caption{What's this?}
\end{figure}
The behaviour exhibited in Fig.~\ref{fig:trace}  cannot be captured in \cite{Kuai} because of its $barrier$-action  semantics:
$barrier$ will always, in an utopian way,%
\footnote{In real-world SDNs, where the $\mbox{\scriptsize\( 	\tt barrier(sw)	\)} $-action semantics is consistent with the OpenFlow specification, a $\mbox{\scriptsize\( 	\tt barrier(sw)	\)} $ ensures the processing order of the controller messages only, and as such it should relaxingly be interleaved with all the actions other than $\mbox{\scriptsize\( 	\tt add(sw, rule_{(\bullet)})	\)} $ and $\mbox{\scriptsize\( 	\tt del(sw, rule_{(\bullet)})	\)} $.}
be executed in state $s^2$ as a matter of priority, which will disable the $\mbox{\small\( 	\tt nomatch(sw, pk_2)	\)} $ by pushing the $\mbox{\small\( 	\tt add(sw, r_2)	\)} $.
Hence, the states $s^3, s^4$ and $\textcolor{red}{\frownie}$ are unnaturally abstracted away hiding this behaviour.

Since in our semantics the control and forwarding states are not idealistically synchronised, we have to fix the controller  program such that the controller state be updated with any of the active connections
only after the respective rule has been installed in the switch.
For this, we used the barrier response message \emph{brepl} which is sent from the switch once both rules corresponding to a bi-directional access are installed.
Also, we improved the property slightly which is formulated as: \textit{if packet $p$ is dropped by a rule installed in a switch $sw$ implies that the connection (flow) asked by $p$ is not in the  whitelist}.
The property excludes the case of a packet being dropped through a $fwd$-message. The reason for this can be seen in \ref{ceg3} which is a admissible trace satisfying original property under our semantics.
Kuai is not able to observe this trace due to the hardwired merge of $nomatch-ctrl-fwd$ which has the effect that packets never actually stay in $pOb$.

\begin{align*}\label{ceg3}
\arraycolsep=1.4pt\def1{1}
&
\mbox{\Large\( 	s 	\)}^0
\xhookrightarrow []{  \tt nomatch(sw, pk_2)  }
\mbox{\Large\( 	s 	\)}^1
\xhookrightarrow []{  \tt ctrl(pk_2)  }
\mbox{\Large\( 	s 	\)}^2
\xhookrightarrow []{  \tt nomatch(sw, pk_1)  }
\mbox{\Large\( 	s 	\)}^3
\xhookrightarrow []{  \tt ctrl(pk_1) }
\mbox{\Large\( 	s 	\)}^4
\xhookrightarrow []{  \tt add(sw, r_1) }
\\
&
\mbox{\Large\( 	s 	\)}^5
\xhookrightarrow []{  \tt add(sw, r_2) }
\mbox{\Large\( 	s 	\)}^6
\xhookrightarrow []{  \tt reply(sw, xid) }
\mbox{\Large\( 	s 	\)}^7
\xhookrightarrow []{  \tt fwd(sw, pk_2, r_{drop})  }
\LARGE \textcolor{red}{\frownie}
\tag{C-E.g. 3}
\end{align*}
\begin{comment}
We revision and enhance in a more natural way the property: the property:......\\
\begin{inparaenum}[(1)]
	\item letting the controller being notified on every flow table update through the \texttt{barrier\_reply} message, and
	\item instructing the controller program to consult the $gV$ for the active connections.
\end{inparaenum}
This way, the controller program will check a consistent.
\end{comment}
}

\section{Introduction}
\label{introduction}

Software-Defined Networking (SDN) \cite{TheRoadToSDN} has brought about a paradigm shift in designing and operating computer networks. A logically centralised controller implements the control logic and `programs' the data plane, which is defined by flow tables installed in network switches. SDN enables the rapid development of advanced and diverse network functionality; e.g. in designing next-generation inter-data centre traffic engineering \cite{DevoFlow}, load balancing \cite{Plug-n-Serve}, firewalls \cite{SDNFirewall}, and Internet exchange points (IXPs) \cite{SDX}. SDN has gained noticeable ground in the industry, with major vendors integrating OpenFlow \cite{Openflow}, the de-facto SDN standard maintained by the Open Networking Forum, in their products. Operators deploy it at scale \cite{Google,Ananta}. SDN presents a unique opportunity for innovation and rapid development of complex network services by enabling all players, not just vendors, to develop and deploy control and data plane functionality in networks. This comes at a great risk; deploying buggy code at the controller could result in problematic flow entries at the data plane and, potentially, service disruption \cite{ERA,Batfish,NetTroub,vision} and security loopholes \cite{OF-RHM,DDoS}. Understanding and fixing such bugs is far from trivial, given the distributed and concurrent nature of computer networks and the complexity of the control plane \cite{shenker}.

With the advent of SDN, a large body of research on verifying network properties has emerged \cite{survey_NV}. Static network analysis approaches \cite{Anteater,HSA,NetSAT,FlowChecker,Flover,Dobrescu} can only verify network properties on a given fixed network configuration but this may be changing very quickly (e.g. as in \cite{hedera}). Another key limitation is the fact that they cannot reason about the controller program, which, itself, is responsible for the changes in the network configuration. Dynamic approaches, such as \cite{VeriFlow,Plotkin,Libra,Deltanet,Netplumber,AtomicPredicates}, are able to reason about network properties as changes happen (i.e. as flow entries in switches' flow tables are being added and deleted), but they cannot reason about the controller program either. As a result, when a property violation is detected, there is no straightforward way to fix the bug in the controller code, as these systems are oblivious of the running code. Identifying bugs in large and complex deployments can be extremely challenging.

Formal verification methods that include the controller code in the model of the network can solve this important problem. Symbolic execution methods, such as \cite{SymNet,Nice,Dobrescu,NetSMC,BUZZ,VeriCon2,SyNET}, evaluate programs using symbolic variables accumulating path-conditions along the way that then can be solved logically. However, they suffer from the path explosion problem caused by loops and function calls which means verification does not scale to larger controller programs (bug finding still works but is limited). Model checking SDNs is a promising area even though only few studies have been undertaken \cite{NetSMC,SDNactors,Nice,Sethi,Kuai,McClurg}. Networks and controller can be naturally modelled as transition systems. State explosion is always a problem but can be mitigated by using abstraction and optimisation techniques (i.e. partial order reductions). At the same time, modern model checkers \cite{Spin,UPPAAL,NuSMV,Alloy,JAVAPathFinder} are very efficient.

{\sc n}et{\sc smc} \cite{NetSMC} uses a bespoke \emph{symbolic} model checking algorithm for checking properties given a subset of computation tree logic that allows quantification only over all paths. As a result, this approach scales relatively well, but the requirement that only one packet can travel through the network at any time is very restrictive and ignores race conditions. {\sc nice} \cite{Nice} employs model checking but only looks at a limited amount of input packets that are extracted through symbolically executing the controller code. As a result, it is a bug-finding tool only. The authors in \cite{Sethi} propose a model checking approach that can deal with dynamic controller updates and an arbitrary number of packets but require manually inserted non-interference lemmas that constrain the set of packets that can appear in the network. This significantly limits its applicability in realistic network deployments. Kuai \cite{Kuai} overcomes this limitation by introducing model-specific partial order reductions (PORs) that result in pruning the state space by avoiding redundant explorations. However, it has limitations explained at the end of this section.

In this paper, we take a step further towards the full realisation of model checking real-world SDNs by introducing MOCS\ (MOdel Checking for Software defined networks)\footnote{A release of MOCS\ is publicly available at \url{https://tinyurl.com/y95qtv5k}}, a highly expressive, optimised SDN model which we implemented in {\sc Uppaal}\footnote{{\sc Uppaal} has been chosen as future plans include extending the model to timed actions like e.g.\ timeouts. Note that the model can be implemented in any model checker.}
 \cite{UPPAAL}. MOCS, compared to the state of the art in model checking SDNs, can model network behaviour more realistically and verify larger deployments using fewer resources. The main contributions of this paper are:

\noindent\textbf{Model Generality}. The proposed network model is closer to the OpenFlow standard than previous models (e.g.\ \cite{Kuai})
to reflect commonly exhibited behaviour between the controller and network switches.
 More specifically, it allows for race conditions between control messages and includes a significant number of  OpenFlow interactions, including barrier response messages. In our experimentation section, we present families of elusive bugs that can be efficiently captured by MOCS.

\noindent\textbf{Model Checking Optimisations}. To tackle the state explosion problem we propose context-dependent \emph{partial order reductions}  by considering the concrete control program and specification in question. We establish the soundness of the proposed optimisations\shortversion{\footnote{Proofs appear in an extended version \url{http://sro.sussex.ac.uk/id/eprint/87495}.}}. Moreover, we propose \emph{state representation optimisations}, namely packet and rule indexing, identification of packet equivalence classes and bit packing, to improve performance. We evaluate the benefits from all proposed optimisations in \S \ref{experimental-evaluation}.\\

Our model has been inspired by Kuai \cite{Kuai}. According to the contributions above, however, we consider MOCS\ to be a considerable improvement. We model more OpenFlow messages and interactions, enabling us to check for bugs that \cite{Kuai} cannot even express (see discussion in \S\ref{subsec:expressivity}). Our context-dependent PORs systematically explore possibilities for optimisation. Our optimisation techniques still allow MOCS\ to run at least as efficiently as Kuai, often with even better performance.

\section{Software-Defined Network Model}
\label{sec:modelSDN}

A key objective of our work is to enable the verification of network-wide properties in real-world SDNs. In order to fulfil this ambition, we present an extended network model to capture complex interactions between the SDN controller and the network. Below we describe the adopted network model, its state and transitions.

\subsection{Formal Model Definition}
\label{semantics}

The formal definition of the proposed SDN model is by means of an action-deterministic transition system. We parameterise the model by the underlying network topology $\lambda$ and the controller program {\sc cp} in use, as explained further below (\S\ref{model-components}).

\begin{defn}
\label{def:SDNmodel}
 An SDN model is a 6-tuple
 $\mathcal{M}_{(\lambda,\textsc{cp})} = (S, s_0, A, \hookrightarrow, AP, L)$, where $S$ is the set of all states the SDN may enter, $s_0$ the initial state, $A$ the set of actions which encode the events the network may engage in,
$\hookrightarrow \subseteq S \times A \times S$ the transition relation describing which execution steps the system undergoes as it perform actions,
$AP$ a set of atomic propositions describing relevant state properties, and $L: S \to 2^{AP}$ is a labelling function, which relates to any state $s\in S$ a set $L(s) \in 2^{AP}$ of those atomic propositions that are true for $s$. Such an SDN model is composed of several smaller systems, which model network components (hosts, switches and the controller) that communicate via queues and, combined, give rise to the definition of $\hookrightarrow$. The states of an SDN transition system are 3-tuples $(\pi, \delta, \gamma)$, where $\pi$ represents the state of each host, $\delta$ the state of each switch, and $\gamma$ the controller state. The components are explained in \S\ref{model-components} and the transitions $\hookrightarrow$ in \S\ref{transitions}.
\end{defn}
Figure~\ref{model} illustrates a high-level view of OpenFlow interactions (left side), modelled actions and queues (right side).

\begin{figure}[h]
	\captionsetup{width=.9\textwidth}
	\begin{center}
		\includegraphics[scale=1]{figures/model.pdf}
		\caption{A high-level view of OpenFlow interactions using OpenFlow specification terminology (left half) and the modelled actions (right half). A red solid-line arrow depicts an action which, when fired, (1) dequeues an item from the queue the arrow begins at, and (2) adds an item in the queue the arrowhead points to (or multiple items if the arrow is double-headed). Deleting an item from the target queue is denoted by a reverse arrowhead. A forked arrow denotes multiple targeted queues.}
		\label{model}
	\end{center}
\end{figure}

\subsection{SDN Model Components}
\label{model-components}
Throughout we will use the common `dot-notation' (\texttt{\_.\_}) to refer to components of composite gadgets (tuples), e.g.\ queues of switches, or parts of the state. We use obvious names for the projections functions like $s.\delta.sw.pq$ for the packet queue of the switch \emph{sw} in state $s$. At times we will also use $t_1$ and $t_2$ for the first and second projection of tuple $t$.

\noindent\textbf{Network Topology. }A location $\mathit{(n, pt)}$ is a pair of a node (host or switch) $n$ and a port $pt$. We describe the network topology as a bijective function $\lambda: (\mathit{Switches} \cup \mathit{Hosts}) \times \mathit{Ports} \rightarrow (\mathit{Switches} \cup \mathit{Hosts}) \times \mathit{Ports}$ consisting of a set of directed edges $\langle \mathit{(n, pt), (n', pt')} \rangle$, where $\mathit{pt'}$ is the input port of the switch or host $n'$ that is connected to port $\mathit{pt}$ at host or switch $n$. \emph{Hosts}, \emph{Switches} and \emph{Ports} are the (finite) sets of all hosts, switches and ports in the network, respectively. The topology function is used when a packet needs to be forwarded in the network. The location of the next hop node is decided when a \emph{send}, \emph{match} or \emph{fwd} action (all defined further below) is fired. Every SDN model is w.r.t.\ a fixed topology $\lambda$ that does not change.

\noindent\textbf{Packets. }Packets are modelled as finite bit vectors and transferred in the network by being stored to the queues of the various network components. A $packet \in \mathit{Packets}$ (the set of all packets that can appear in the network) contains bits describing the proof-relevant header information and its location $loc$.

\noindent\textbf{Hosts. }Each $\mathit{host} \in \mathit{Hosts}$, has a packet queue (\emph{rcvq}) and a finite set of ports which are connected to ports of other switches. A host can send a packet to one or more switches it is connected to (\emph{send} action in Figure \ref{model}) or receive a packet from its own $rcvq$ (\emph{recv} action in Figure \ref{model}). Sending occurs repeatedly in a non-deterministic fashion which we model implicitly via the $(0,\infty)$ abstraction at switches' packet queues, as discussed further below.

\noindent\textbf{Switches. }Each $\mathit{switch} \in \mathit{Switches}$, has a flow table $\mathit{(ft)}$, a packet queue $\mathit{(pq)}$, a control queue $\mathit{(cq)}$, a forwarding queue $\mathit{(fq)}$ and one or more ports, through which it is connected to other switches and/or hosts. A flow table $\mathit{ft} \subseteq \mathit{Rules}$ is a set of forwarding rules (with $\mathit{Rules}$ being the set of all rules). Each one consists of a tuple $\mathit{(priority, pattern, ports)}$, where $\mathit{priority} \in \mathbb{N}$ determines the priority of the rule over others, $\mathit{pattern}$ is a proposition over the proof-relevant header of a packet, and $\mathit{ports}$ is a subset of the switch's ports.

 Switches match packets in their packet queues against rules (i.e. their respective $\mathit{pattern}$) in their flow table (\emph{match} action in Figure \ref{model}) and forward packets to a connected device (or final destination), accordingly. Packets that cannot be matched to any rule are sent to the controller's request queue (\emph{rq}) (\emph{nomatch} action in Figure \ref{model}); in OpenFlow, this is done by sending a \emph{PacketIn} message. The forwarding queue \emph{fq} stores packets forwarded by the controller in \emph{PacketOut} messages. The control queue stores messages sent by the controller in \emph{FlowMod} and \emph{BarrierReq} messages. \emph{FlowMod} messages contain instructions to add or delete rules from the flow table (that trigger \emph{add} and \emph{del} actions in Figure~\ref{model}). \emph{BarrierReq} messages contain barriers to synchronise the addition and removal of rules.

 MOCS\ conforms to the OpenFlow specifications and always execute instructions in an interleaved fashion obeying the ordering constraints imposed by barriers.

\noindent\textbf{OpenFlow Controller. }The controller is modelled as a finite state automaton embedded into the overall transition system.
A controller program {\sc cp}, as used to parametrise an SDN model, consists of $(\mathit{CS},\mathit{pktIn},\mathit{barrierIn})$.
It uses its own local state $\mathit{cs}\in \mathit{CS}$, where $\mathit{CS}$ is the finite set of control program states. Incoming \emph{PacketIn} and \emph{BarrierRes} messages from the SDN model are stored in separate queues ($\mathit{rq}$ and $\mathit{brq}$, respectively) and trigger \emph{ctrl} or \emph{bsync} actions (see Figure~\ref{model}) which are then processed by the controller program in its current state.
The controller's corresponding handler, \emph{pktIn} for \emph{PacketIn} messages and \emph{barrierIn} for \emph{BarrierRes} messages, responds by potentially changing its local state and sending messages to a subset of \emph{Switches}, as follows. A number of \emph{PacketOut} messages -- pairs of (\emph{pkt, ports}) -- can be sent to a subset of \emph{Switches}. Such a message is stored in a switch's forward queue and instructs it to forward packet \emph{pkt} along the ports \emph{ports}. The controller may also send any number of \emph{FlowMod} and \emph{BarrierReq} messages to the control queue of any subset of \emph{Switches}. A \emph{FlowMod} message may contain an \textit{add} or \textit{delete} rule modification instruction. These are executed in an arbitrary order by switches, and \textit{barriers} are used to synchronise their execution. Barriers are sent by the controller in \emph{BarrierReq} messages. OpenFlow requires that a response message (\emph{BarrierRes}) is sent to the controller by a switch when a barrier is consumed from its control queue so that the controller can synchronise subsequent actions.
Our model includes a \emph{brepl} action that models the sending of a \emph{BarrierRes} message from a switch to the controller's barrier reply queue (\emph{brq}), and a \emph{bsync} action that enables the controller program to react to barrier responses.

\noindent\textbf{Queues. }All queues in the network are modelled as \emph{finite} state. Packet queues $\mathit{pq}$ for switches are modelled as multisets, and we adopt $(0,\infty)$ abstraction \cite{01infty}; i.e.\ a packet is assumed to appear either zero or an arbitrary (unbounded) amount of times in the respective multiset. This means that once a packet has arrived at a switch or host, (infinitely) many other packets of the same kind repeatedly arrive at this switch or host. Switches' forwarding queues \emph{fq} are, by contrast, modelled as sets, therefore if multiple identical packets are sent by the controller to a switch, only one will be stored in the queue and eventually forwarded by the switch. The controller's request $\mathit{rq}$ and barrier reply queues \emph{brq} are modelled as sets as well.
Hosts' receive queues $\mathit{rcvq}$ are also modelled as sets. Controller queues $cq$ at switches are modelled as a finite sequence of sets of control messages (representing add and remove rule instructions), interleaved by any number of barriers. As the number of barriers that can appear at any execution is finite, this sequence is finite.

\subsection{Guarded Transitions}
\label{transitions}

Here we provide a detailed breakdown of the transition relation $ s \xhookrightarrow[]{  \alpha(\vec{a})  } s'$ for each action $\alpha(\vec{a}) \in A(s)$, where $A(s)$ the set of all enabled actions in $s$ in the proposed model (see Figure \ref{model}). Transitions are labelled by action names $\alpha$ with arguments $\vec{a}$. The transitions are only enabled in state $s$ if $s$ satisfies certain conditions called \emph{guards} that can refer to the arguments $\vec{a}$. In guards, we make use of predicate $\mathit{bestmatch(sw,r,pkt)}$ that expresses that $r$ is the highest priority rule in $\mathit{sw.ft}$ that matches $\mathit{pkt}$'s header.
Below we list all possible actions with their respective guards.

\renewcommand{\labelitemi}{$\bullet$}

	\noindent $\boldsymbol{\mathit{send(h,pt,pkt)}}$. Guard: $\mathit{true}$. This transition models packets arriving in the network in a non-deterministic fashion. When it is executed, $\mathit{pkt}$ is added to the packet queue of the network switch connected to the port $\mathit{pt}$ of host $h$ (or, formally, to $\lambda(\mathit{h,pt})_1.\mathit{pq}$, where $\lambda$ is the topology function described above). As described in \S\ref{subsec:state:repr}, only relevant representatives of packets are actually sent by end-hosts. This transition is unguarded, therefore it is always enabled.
	%
	%

	\noindent $\boldsymbol{\mathit{recv(h, pkt)}}$. Guard: $\mathit{pkt} \in \mathit{h.rcvq}$. This transition models hosts receiving (and removing) packets from the network and is enabled if $\mathit{pkt}$ is in $h$'s receive queue.

	%
	%

	\noindent $\boldsymbol{\mathit{match(sw,pkt,r)}}$. Guard: $\mathit{pkt} \in \mathit{sw.pq} \wedge r\in \mathit{sw.ft} \wedge
\mathit{bestmatch(sw,r,pkt)}$.
	This transition models matching and forwarding packet $\mathit{pkt}$ to zero or more next hop nodes (hosts and switches), as a result of highest priority matching of rule $r$ with $\mathit{pkt}$. The packet is then copied to the packet queues of the connected hosts and/or switches, by applying the topology function to the port numbers in the matched rule; i.e. $\lambda(\mathit{sw,pt})_1.\mathit{pq}, \forall \mathit{pt} \in \mathit{r.ports}$. Dropping packets is modelled by having a special `drop' port that can be included in rules. The location of the forwarded packet(s) is updated with the respective destination (switch/host, port) pair; i.e.\ $\lambda(\mathit{sw,pt})$. Due to the $(0,\infty)$ abstraction, the packet is not removed from $\mathit{sw.pq}$.
	%
	%

	\noindent $\boldsymbol{\mathit{nomatch(sw,pkt)}}$. Guard: $\mathit{pkt} \in \mathit{sw.pq}  \wedge \nexists r\in \mathit{sw.ft}~.~
\mathit{bestmatch(sw,r,pkt)}$. This transition models forwarding a packet to the OpenFlow controller when a switch does not have a rule in its forwarding table that can be matched against the packet header. In this case, $\mathit{pkt}$ is added to \emph{rq} for processing. $\mathit{pkt}$ is not removed from $\mathit{sw.pq}$ due to the supported $(0,\infty)$ abstraction.
	%
	%

	\noindent $\boldsymbol{\mathit{ctrl(pkt, cs)}}$. Guard: $\mathit{pkt} \in \mathit{controller.rq}$. This transition models the execution of the packet handler by the controller when packet $\mathit{pkt}$, that was previously sent by switch $\mathit{pkt.loc}_1$, is available in \emph{rq}. The controller's packet handler function $\mathit{pktIn(pkt.loc}_1, \mathit{pkt, cs)}$ is executed which, in turn
	\begin{inparaenum}[(i)]
		\item reads the current controller state \emph{cs} and changes it according to the controller program,
		\item adds a number of rules, interleaved with any number of barriers, into the \emph{cq} of zero or more switches, and
		\item adds zero or more forwarding messages, each one including a packet along with a set of ports, to the \emph{fq} of zero or more switches.

	\end{inparaenum}
	%
	%

	\noindent $\boldsymbol{\mathit{fwd(sw, pkt, ports)}}$. Guard: $\mathit{(pkt,ports)} \in \mathit{sw.fq}$. This transition models forwarding packet $\mathit{pkt}$ that was previously sent by the controller to $sw$'s forwarding queue $\mathit{sw.fq}$. In this case, $\mathit{pkt}$ is removed from $\mathit{sw.fq}$ (which is modelled as a set), and added to the $\mathit{pq}$ of a number of network nodes (switches and/or hosts), as defined by the topology function $\lambda(\mathit{sw,pt})_1.\mathit{pq}, \forall \mathit{pt} \in \mathit{ports}$. The location of the forwarded packet(s) is updated with the respective destination (switch/host, port) pair; i.e.\ $\lambda(\mathit{n,pt})$.

	%

	\noindent $\boldsymbol{\mathit{FM(sw, r)}}$, where $\mathit{FM}\in \{\mathit{add, del}\}$. Guard: $(\mathit{FM,r}) \in \mathit{head(sw.cq)}$.
	 These transitions model the addition and deletion, respectively, of a rule in the flow table of switch \emph{sw}.
	 They are enabled when one or more \emph{add} and \emph{del} control messages are in the set at the head of the switch's control queue. In this case, $r$ is added to -- or deleted from, respectively -- $\mathit{sw.ft}$ and the control message is deleted from the set at the head of \emph{cq}. If the set at the head of \emph{cq} becomes empty it is removed. If then the next item in \emph{cq} is a barrier, a \emph{brepl} transition becomes enabled (see below).

	%

	\noindent $\boldsymbol{\mathit{brepl(sw, xid)}}$. Guard: $\mathit{b(xid)} = \mathit{head(sw.cq)}$. This transition models a switch sending a barrier response message, upon consuming a barrier from the head of its control queue; i.e.\ if $\mathit{b(xid)}$ is the head of \emph{sw.cq}, where $\mathit{xid} \in \mathbb{N}$ is an identifier for the barrier set by the controller, $\mathit{b(xid)}$ is removed and the barrier reply message $\mathit{br(sw, xid)}$ is added to the controller's \emph{brq}.

	%

	\noindent $\boldsymbol{\mathit{bsync(sw, xid, cs)}}$. Guard: $\mathit{br(sw, xid)} \in \mathit{controller.brq}$.
	 This transition models the execution of the barrier response handler by the controller when a barrier response sent by switch $sw$ is available in \emph{brq}. In this case, $\mathit{br(sw, xid)}$ is removed from the \emph{brq}, and the controller's barrier handler $\mathit{barrierIn(sw,xid,cs)}$ is executed which, in turn
		\begin{inparaenum}[(i)]
		\item reads the current controller state $cs$ and changes it according to the controller program,
		\item adds a number of rules, interleaved with any number of barriers, into the $cq$ of zero or more switches, and
		\item adds zero or more forwarding messages, each one including a packet along with a set of ports, to the \emph{fq} of zero or more switches.
	\end{inparaenum}

\noindent\textbf{An example run}. In Figure \ref{tab:transitions}, we illustrate a sequence of MOCS transitions through a simple packet forwarding example. The run starts with a \textit{send} transition; packet \textit{p} is copied to the packet queue of the switch in black. Initially, switches' flow tables are empty, therefore \textit{p} is copied to the controller's request queue (\textit{nomatch} transition); note that \textit{p} remains in the packet queue of the switch in black due to the $(0,\infty)$ abstraction. The controller's packet handler is then called (\textit{ctrl} transition) and, as a result, (1) \textit{p} is copied to the forwarding queue of the switch in black, (2) rule $r_1$ is copied to the control queue of the switch in black, and (3) rule $r_2$ is copied to the control queue of the switch in white. Then, the switch in black forwards \textit{p} to the packet queue of the switch in white (\textit{fwd} transition). The switch in white installs $r_2$ in its flow table (\textit{add} transition) and then matches \textit{p} with the newly installed rule and forwards it to the receive queue of the host in white (\textit{match} transition), which removes it from the network (\textit{recv} transition).

\begin{figure}[h]
	\centering
	\vspace{.4cm}
	\includegraphics[width=1\linewidth]{figures/transitionsExample.pdf}
	\caption{Forwarding $p$ from $\protect\blacklaptop$ to $\protect\whitelaptop$. Non greyed-out icons are the ones whose state changes in the current transition.}
	\label{tab:transitions}
\end{figure}

\ignore{

	\begin{table}[h]
		\centering
		\caption{Rules in MOCS\ that are different from Kuai \cite{Kuai}}
		\label{fig:changedrules}
		\scriptsize
		\begin{tabular}{lr}
			\toprule\\[-2mm]

			$\small (\pi, \delta, \gamma) \xhookrightarrow[]{nomatch(sw,pkt)} (\pi, \delta', \gamma')$ & \begin{minipage}{6.5cm} \centering where $\gamma'.rq {=} \gamma.rq \cup \{(sw,pkt)\}$ and $\delta'  {=}  delPkt(\delta,\{(sw,pkt)\}) $ \end{minipage}\\[0.2cm]
			\midrule\\[-2mm]
			$\small (\pi, \delta, \gamma) \xhookrightarrow[]{fwd(sw,pkt,pts)} (\pi', \delta', \gamma)$  &  \begin{minipage}{6cm} \centering where $\pi' {=} addPkt(\pi, FwdToC(sw,pkt,pts))$, $\delta''  {=}  delFwdMsg(\delta, sw, (pkt,pts))$ and $\delta' = addPkt(\delta'', FwdToSw(sw,pkt,pts))$ \end{minipage}\\[0.4cm]
			\midrule\\[-2mm]
			$\small (\pi, \delta, \gamma) \xhookrightarrow[]{ctrl(sw,pkt,cs)} (\pi, \delta', \gamma')$ &  \begin{minipage}{6.5cm} \centering where $\gamma'.rq {=} \gamma.rq \setminus \{pkt\}$,  $pktIn(sw, pkt, \gamma.cs)  {=}  (\eta, msg, \gamma'.cs)$, $\delta''  {=}  addFwdMsg(\delta, sw, msg)$, and $\delta'  {=}  addCtrlCmd(\delta'', \eta)$ \end{minipage} \\[0.5cm]
			\midrule\\[-2mm]
			$\small (\pi, \delta, \gamma) \xhookrightarrow[]{brepl(sw,xid)} (\pi, \delta', \gamma')$

			& \begin{minipage}{6.5cm} \centering where $\delta'  {=}  \delta(sw).cq[0] \ominus \llceil b(xid) \rrceil$ and $\gamma'.brq  {=}  \gamma.brq \cup \{br(sw, xid)\}$ \end{minipage}\\[0.2cm]
			\midrule\\[-2mm]
			$\small (\pi, \delta, \gamma) \xhookrightarrow[]{bsync(sw,xid,cs)} (\pi, \delta', \gamma')$ & \begin{minipage}{6cm} \centering where   $barrierIn(sw, xid, \gamma.cs)  {=}  (\eta, msg, \gamma'.cs)$, $\delta''  {=}  addFwdMsg(\delta, sw, msg)$,  $\delta'  {=}  addCtrlCmd(\delta'', \eta)$ and $\gamma'.brq  {=}  \gamma.brq \setminus \{br(sw, xid)\}$  \end{minipage}\\
			[.5cm]
			\bottomrule
		\end{tabular}
		\vspace{-.7cm}
	\end{table}
}

\subsection{Specification Language}
\label{spec}

In order to specify properties of packet flow in the network, we use LTL formulas without ``next-step" operator $\bigcirc$\footnote{This is the largest set of formulae supporting the partial order reductions used in \S\ref{sec:optimisations}, as stutter equivalence does not preserve the truth value of formulae with the $\bigcirc$.}, where atomic formulae denoting properties of states of the transition system, i.e.\ SDN network.
In the case of safety properties, i.e.\ an invariant w.r.t.\ states, the LTL$_{\setminus \{\bigcirc\}}$ formula is of the form $\Box \varphi$, i.e.\ has only an outermost $\Box$ temporal connective.

Let $P$ denote unary predicates on packets which encode a property of a packet based on its fields.
An atomic \textit{state condition} (proposition) in $\mathit{AP}$ is either of the following: (i) existence of a packet $\mathit{pkt}$ located in a packet queue ($pq$) of a switch or in a receive queue (\emph{rcvq}) of a host that satisfies $P$ (we denote this by
$\exists \mathit{pkt} {\in} \mathit{n.pq}\,.\, \mathit{P(pkt)}$ with $n\in  \mathit{Switches}$, and $\exists \mathit{pkt} {\in} \mathit{h.rcvq}\,.\, \mathit{P(pkt)}$ with $h\in \mathit{Hosts}$)\footnote{Note that these are \emph{atomic} propositions despite the use of the existential quantifier notation.};
(ii) the controller is in a specific \emph{controller} state $q\in \mathit{CS}$, denoted by a unary predicate symbol $Q(q)$ which holds in system state $s \in S$ if $q = s.\gamma.cs$.
The specification logic comprises first-order formula with equality on the finite domains of switches, hosts, rule priorities, and ports which are \emph{state-independent} (and decidable).

For example,
$\exists \mathit{pkt} {\in} \mathit{sw.pq}\,.\, \mathit{P(pkt)}$
represents the fact that the packet predicate $P(\_)$ is true for at least one packet $\mathit{pkt}$ in the \emph{pq} of switch $sw$.
For every atomic packet proposition $\mathit{P(pkt)}$, also its negation $\neg \mathit{P(pkt)}$ is an atomic proposition for the reason of simplifying syntactic checks of formulae in Table~\ref{tab:safeness} in the next section. Note that universal quantification over packets in a queue is a derived notion. For instance, $\forall \mathit{pkt} {\in} \mathit{n.pq}\,.\, \mathit{P(pkt)}$ can be expressed as $ \nexists \mathit{pk} {\in} \mathit{n.pq}\,.\, \neg \mathit{P(pkt)}$.
Universal and existential quantification over switches or hosts can be expressed by finite iterations of ${\wedge}$ and ${\vee}$, respectively.

In order to be able to express that a condition holds when a certain event happened, we add to our propositions instances of \emph{propositional dynamic logic} \cite{DL1,DL2}.
Given an action $\alpha(\cdot)\in A$ and a proposition $P$ that may refer to any variables in $\vec{x}$, $[\alpha(\vec{x})]P$ is also a proposition and $[\alpha(\vec{x})]P$ is true if, and only if,
after firing transition $\alpha(\vec{a})$ (to get to the current state), $P$ holds with the variables in $\vec{x}$ bound to the corresponding values in the actual arguments $\vec{a}$.
With the help of those basic modalities one can then also specify that more complex events occurred. For instance, dropping of a packet due to a \emph{match} or \emph{fwd} action can be expressed by $[\mathit{match(sw,pkt,r)}](r.\mathit{fwd\_port}=\texttt{drop}) \land [\mathit{fwd(sw,pkt,pt)}](\mathit{pt}=\texttt{drop})$. Such predicates derived from modalities are used in \S \ref{appendix:CP}-\ref{rq1-alg3}.

The meaning of temporal LTL operators is standard depending on the trace of a transition sequence $s_0 \xhookrightarrow{\alpha_1} s_1 \xhookrightarrow{\alpha_2} \ldots$.
The trace $L(s_0)L(s_1)\ldots L(s_i)\ldots$ is defined as usual.
For instance, trace $L(s_0)L(s_1)L(s_2)\ldots$ satisfies invariant $\Box \varphi$ if each $L(s_i)$ implies $\varphi$.

\section{Model Checking}
\label{sec:optimisations}

In order to verify desired properties of an SDN, we use its model as described in Def.~\ref{def:SDNmodel}
and apply model checking. In the following we propose optimisations that significantly improve the performance of model checking.

\subsection{Contextual Partial-Order Reduction}
\label{subsec:por}

\emph{Partial order reduction} (POR) \cite{representatives} reduces the number of interleavings (traces) one has to check. Here is a reminder of the main result (see \cite{Baier2008}) where we use a stronger condition than the regular (\emph{C4}) to deal with cycles:

\begin{thm}[Correctness of POR]
Given a finite transition system $\mathcal{M} = (S, A, \hookrightarrow, s_0, AP, L)$ that is action-deterministic and without terminal states, let $A(s)$ denote the set of actions in $A$ enabled in state $s\in S$.
Let $\mathit{ample}(s) \subseteq A(s)$ be a set of actions for a state $s\in S$ that satisfies the following conditions:
\begin{enumerate}[label=C\arabic*]
\item (Non)emptiness condition: $\varnothing  \neq \mathit{ample}(s) \subseteq A(s)$.
\item Dependency condition: Let $s \xhookrightarrow[]{\alpha_1} s_1...\xhookrightarrow[]{\alpha_n} s_n \xhookrightarrow[]{\beta} t$ be a run in $\mathcal{M}$. If $\beta \in A  \setminus \mathit{ample}(s)$ depends on $\mathit{ample}(s)$, then $\alpha_i \in \mathit{ample}(s)$ for some $0 < i \leq n$, which means that in every path fragment of $\mathcal{M} $, $\beta$ cannot appear before some transition from $\mathit{ample}(s)$ is executed.
\item Invisibility condition: If $\mathit{ample}(s) \neq A(s)$ (i.e., state $s$ is not fully expanded), then every $\alpha \in \mathit{ample}(s)$ is invisible.
\item Every cycle in $\mathcal{M}^{\mathit{ample}}$ contains a state $s$ such that $\mathit{ample}(s)=A(s)$
\end{enumerate}
\label{ample}
where $\mathit{\mathcal{M}^{\mathit{ample}} = (S_a, A, \hookrightarrow\mathrel{\mkern-14mu}\rightarrow, s_0, AP, L_a) }$ is the new, optimised, model defined as follows:
let
$S_a \subseteq S$ be the set of states reachable from the initial state $s_0$ under $\hookrightarrow\mathrel{\mkern-14mu}\rightarrow$, let $L_a(s) = L(s)$ for all $s \in S_a$ and define $\hookrightarrow\mathrel{\mkern-14mu}\rightarrow\,    \subseteq S_a\times A\times S_a$ inductively by the rule
\[
\frac {s~ \xhookrightarrow[]{ \alpha}    ~s'}{ s~ \stackrel{~\alpha~}{\hookrightarrow\mathrel{\mkern-14mu}\rightarrow}    s'  }
\qquad   \textup{if }\  \alpha \in \mathit{ample}(s)  \]
If $\mathit{ample}(s)$ satisfies conditions (C1)-(C4) as outlined above, then for each path in $\mathcal{M} $ there exists a stutter-trace equivalent path in $\mathcal{M}^{\mathit{ample}} $, and vice-versa, denoted $\mathcal{M}   \stutt \mathcal{M}^{\mathit{ample}} $. 	\label{thm1}
\end{thm}
The intuitive reason for this theorem to hold is the following: Assume an action sequence $\alpha_i . . . \alpha_{i+n}\beta$ that reaches the state $s$, and $\beta$ is \textit{independent} of $\{\alpha_i, . . . \alpha_{i+n}\}$. Then, one can permute $\beta$ with $\alpha_{i+n}$ through $\alpha_i$ successively $n$ times. One can therefore construct the sequence $\beta\alpha_i . . . \alpha_{i+n}$ that also reaches the state $s$. If this shift of $\beta$ does not affect the labelling of the states with atomic propositions ($\beta$ is called \emph{invisible} in this case), then it is not detectable by the property to be shown and the permuted and the original sequence are equivalent w.r.t.\ the property and thus don't have to be checked both.
One must, however, ensure, that in case of loops (infinite execution traces) the ample sets do not \emph{preclude} some actions to be fired altogether, which is why one needs (\emph{C4}).

The more actions that are both stutter and provably independent (also referred to as \textit{safe actions} \cite{Peled95}) there are, the smaller the transition system, and the more efficient the model checking.
One of our contributions is that we attempt to identify \emph{as many safe actions as possible} to make PORs more widely applicable to our model.

The PORs in \cite{Kuai} consider only dependency and invisibility of \emph{recv} and \emph{barrier} actions, whereas we explore systematically all possibilities for applications of Theorem~\ref{thm1} to reduce the search space.
When identifying safe actions, we consider (1) the actual controller program {\sc cp}, (2) the topology $\lambda$ and (3) the state formula $\varphi$ to be shown invariant, which we call the \emph{context} {\sc ctx} of actions.
It turns out that two actions may be dependent in a given context of abstraction while independent in another context, and similarly for invisibility, and we exploit this fact. The argument of the action thus becomes relevant as well.

\begin{defn}[Safe Actions] \label{def:safe} Given a context {\sc ctx} $= (\textsc{cp},\lambda,\varphi)$, and SDN model $\mathcal{M}_{(\lambda,\textsc{cp})} = (S, A, \hookrightarrow, s_0, AP, L)$, an action $\alpha(\cdot)\in A(s)$ is called `safe' if it is independent of any other action in $A$ and invisible for $\varphi$.
We write safe actions $\check{\alpha}(\cdot)$.
\end{defn}
\begin{defn}[Order-sensitive Controller Program]
	\label{def:ord-sens}
	A controller program {\sc cp} is order-sensitive if there exists a state $s\in S$ and two actions $\alpha,~\beta$ in $\{ \mathit{ctrl}(\cdot), \mathit{bsync}(\cdot)  \}$ such that $\alpha,\beta \in A(s)$
and $s\xhookrightarrow[]{\alpha} s_1 \xhookrightarrow[]{\beta} s_2$ and $s\xhookrightarrow[]{\beta} s_3 \xhookrightarrow[]{\alpha} s_4$ with $s_2\neq s_4$.
\end{defn}

\begin{defn} \label{def:unobservableAction}
Let $\varphi$ be a state formula. An action $\alpha \in A$ is called `$\varphi$-invariant' if
$s\models \varphi$ iff $\alpha(s)\models \varphi$ for all $s\in S$ with $\alpha\in A(s)$.
\end{defn}

\begin{lemma}\label{lemma:safe} For transition system $\mathcal{M}_{(\lambda,\textsc{cp})} = (S, A, \hookrightarrow, s_0, AP, L)$ and a formula $\varphi\in \text{LTL}_{ \setminus \{\bigcirc \}}$,

$\alpha \in A  \text{ is safe   }~\mathrm{iff}~  \bigwedge\nolimits^3_{i=1} \mathit{Safe}_i(\alpha)$,
	where $\mathit{Safe}_i$, given in Table \ref{tab:safeness}, are per-row.
	%

\end{lemma}
\longversion{
\begin{proof}
\vspace{-0.2cm}	See Appendix \ref{appendix:proofs}.
\end{proof}}
\begin{table}[h]
	\scriptsize
	\begin{center}
		\caption{Safeness Predicates}
		\label{tab:safeness}
		\begin{tabular}{m{2.9cm}|m{4.4cm}|m{4.8cm}}
			\toprule
			\multicolumn{1}{c|}{\textbf{Action}} & \multicolumn{1}{c|}{\textbf{Independence} }& \multicolumn{1}{c}{\textbf{Invisibility}}\\
			\multicolumn{1}{c|}{$\mathit{Safe}_1(\alpha)$} & \multicolumn{1}{c|}{$\mathit{Safe}_2(\alpha)$ } & \multicolumn{1}{c}{$\mathit{Safe}_3(\alpha)$} \\
			\midrule
			$\alpha =\mathit{ctrl(pk, cs)}$ &  {\sc cp} is not order-sensitive
			& \texttt{if} $Q(q)$ occurs in $\varphi$, where $q \in \mathit{CS}$, \texttt{then}   $\alpha$ is $\varphi$-invariant.\\

			\midrule
			$\alpha = \mathit{bsync(sw, xid, cs)}$ &   {\sc cp} is not order-sensitive   &  \texttt{if}  $Q(q)$

			occurs in $\varphi$, where $q \in \mathit{CS}$, \texttt{then}  $\alpha$ is $\varphi$-invariant.\\
			\midrule
			$\mathit{\alpha = fwd(sw, pk, \mathit{ports})}$ & \multicolumn{1}{c|}{$\top$} &  \texttt{if}  $\exists pk {\in} b.q\,.\, P(pk)$ occurs in $\varphi$, for any $b\in \{sw\}\cup \{ \lambda(sw,p)_1\ |\ p\in \mathit{ports} \}$ and $q \in \{\mathit{pq,recvq}\}$, \texttt{then}    $\alpha$ is $\varphi$-invariant.\\

			\midrule
			$\alpha =  \mathit{brepl(sw, xid)}$ & \multicolumn{1}{c|}{$\top$} & \multicolumn{1}{c}{$\top$}\\
			\midrule
			$\alpha = \mathit{recv(h, pk)}$ & \multicolumn{1}{c|}{$\top$} &  \texttt{if}  $\exists pk {\in} \mathit{h.rcvq}\,.\, \mathit{P(pk)}$ occurs in $\varphi$, \texttt{then}   $\alpha$ is  $\varphi$-invariant.\\
			\bottomrule
		\end{tabular}
	\end{center}
	\vspace{-.3cm}
\end{table}

\begin{thm}[POR instance for SDN]
\label{thm:POR}
Let $(\textsc{cp}, \lambda, \varphi)$ be a context such that $\mathcal{M}_{(\lambda,\textsc{cp})} = (S, A, \hookrightarrow, s_0, AP, L)$ is an SDN network model from Def.~\ref{def:SDNmodel};
and let safe actions be as in Def.~\ref{def:safe}. Further, let $\mathit{ample}(s)$ be defined by:
\[
\mathit{ample}(s)= \left\{ \begin{array}{ll}
\{\alpha\in A(s)\ |\ \alpha \text{ safe } \} & \text{if } \{\alpha\in A(s)\ |\ \alpha \text{ safe } \} \neq \emptyset\\
A(s) &\text{otherwise}
\end{array}
\right.
\]
Then, $\mathit{ample}$ satisfies the criteria of Theorem~\ref{ample} and thus $\mathcal{M}_{(\lambda,\textsc{cp})}       \stutt      \mathcal{M}^{\mathit{ample}}_{(\lambda,\textsc{cp})}$ \footnote{Stutter equivalence here implicitly is defined w.r.t.\  the atomic propositions appearing in $\varphi$,  but this suffices as we are just interested in the validity of $\varphi$.}
\end{thm}
\begin{proof}
	$ $\newline
	\vspace{-.4cm}
	\begin{enumerate}[label=\textit{C\arabic*}]
		\item The (non)emptiness condition is trivial since by definition of $\mathit{ample}(s)$ it follows that $\mathit{ample}(s) = \varnothing $ iff $A(s) = \varnothing $.
		\item By assumption $\beta \in A  \setminus \mathit{ample}(s)$ depends on $\mathit{ample}(s)$. But with our definition of $\mathit{ample}(s)$ this is impossible as all actions in
		 $\mathit{ample}(s)$ are safe and by definition independent of all other actions.

		%
		\item The validity of the invisibility condition is by definition of $\mathit{ample}$ and safe actions.
		\item

		We now show that every cycle in $\mathcal{M}_{(\lambda,\textsc{cp})}^{\mathit{ample}}$ contains a fully expanded state $s$, i.e.\  a state $s$ such that $\mathit{ample}(s)=A(s)$.

		\label{cycle}
 By definition of $\mathit{ample}(s)$ in Thm.~\ref{thm:POR} it is equivalent to show that there is no cycle in $\mathcal{M}_{(\lambda,\textsc{cp})}^{\mathit{ample}}$ consisting of safe actions only.
		We show this by contradiction, assuming such a cycle of only safe actions exists.
		There are five safe action types to consider: \emph{ctrl}, \emph{fwd}, \emph{brepl}, \emph{bsync} and \emph{recv}.
		Distinguish two cases.

	 	 \emph{Case 1. A sequence of safe actions of same type}. Let us consider the different safe actions:
     		\begin{itemize}
			 \item Let $\rho$ an execution of $\mathcal{M}_{(\lambda,\textsc{cp})}^{\mathit{ample}}$ which consists of only one type of \emph{ctrl}-actions:
				$$\rho = s_1 \xhookrightarrowdbl{\mathit{ctrl}(\mathit{pkt}_1,\mathit{cs}_1)} s_2 \xhookrightarrowdbl{\mathit{ctrl}(\mathit{pkt}_2,\mathit{cs}_2)} ... s_{i-1} \xhookrightarrowdbl{\mathit{ctrl}(\mathit{pkt}_{i-1},\mathit{cs}_{i-1})}  s_i$$
				Suppose $\rho$ is a cycle.

				According to the \emph{ctrl} semantics, for each transition $s \xhookrightarrowdbl{\mathit{ctrl(pkt,cs)}} s' $,
				where $s = (\pi, \delta, \gamma)$, $s' = (\pi', \delta', \gamma')$, it holds that $\mathit{\gamma'.rq} = \mathit{\gamma.rq}\setminus \{\mathit{pkt}\}$ as we use sets to represent \emph{rq} buffers.
				Hence, for the execution $\rho$ it holds $\gamma_i.\mathit{rq} = \gamma_1.\mathit{rq}\setminus \{\mathit{pkt}_1, \mathit{pkt}_2,...\mathit{pkt}_{i-1}\}$ which implies that $s_1 \neq s_i$. Contradiction.
		%
			\item 		 Let $\rho$ an execution which consists of only one type of \emph{fwd}-actions: similar argument as above since \emph{fq}-s are represented by sets and thus forward messages are removed from \emph{fq}.
			\item 		 Let $\rho$ an execution which consists of only one type of \emph{brepl}-actions: similar argument as above since control messages are removed from \emph{cq}.

			\item 		 Let $\rho$ an execution which consists of only one type of \emph{bsync}-actions: similar argument as above, as barrier reply messages are removed from \emph{brq}-s  that are represented by sets.

			\item 		 Let $\rho$ an execution which consists of only one type of \emph{recv}-actions: similar argument as above, as packets are removed from $\mathit{rcvq}$ buffers that are represented by sets.
      		   \end{itemize}

	 	  \emph{Case 2. A sequence of different safe actions}.

		Suppose there exists a cycle with mixed safe actions starting in $s_1$ and ending in $s_i$.
		Distinguish the following cases.

		\begin{longenum}
			\item There exists at least a \emph{ctrl} and/or a \emph{bsync} action in the cycle. According to the effects of safe transitions, the \emph{ctrl} action will change to a state with smaller \emph{rq} and the \emph{bsync} will always switch to a state with smaller \emph{brq}. It is important here that \emph{ctrl} does not interfere with \emph{bsync} regarding \emph{rq, brq}, and no safe action of other type than \emph{ctrl} and \emph{bsync} accesses \emph{rq} or \emph{brq}. This implies that $s_1 \neq s_i$. Contradiction.
			\item Neither \emph{ctrl}, nor \emph{bsync} actions in the cycle.
			\begin{longenum}
				\item There is a \emph{fwd} and/or \emph{brepl} in the cycle: \emph{fwd} will always switch to a state with smaller \emph{fq} and \emph{brepl} will always switch to a state with smaller \emph{cq} (\emph{brepl} and \emph{recv} do not interfere with \emph{fwd}). This implies that $s_1 \neq s_i$. Contradiction.
				\item There is neither \emph{fwd} nor \emph{brepl} in the cycle. This means that only \emph{recv} is in the cycle which is already covered by the first case.
			\end{longenum}
	       \end{longenum}
 	\end{enumerate}
\end{proof}

\noindent
Due to the definition of the transition system via ample sets, each safe action is immediately executed after its enabling one. Therefore, one can merge every transition of a safe action with its precursory enabling one.
Intuitively, the semantics of
the merged action is defined as the successive execution of
its constituent actions. This process can be repeated if there is a chain of safe actions; for instance, in the case of ${s \xhookrightarrowdbl[]{\mathit{nomatch(sw,pkt)}}s' \xhookrightarrowdbl[]{\mathit{ctrl(pkt,cs)}} s'' \xhookrightarrowdbl[]{\mathit{fwd(sw,pkt,ports)}} s'''}$
where each transition enables the next and the last two are assumed to be safe. These transitions can be merged into one, yielding a stutter equivalent trace as the intermediate states are invisible (w.r.t.\ the context and thus the property to be shown) by definition of safe actions.

\subsection{State Representation}
\label{subsec:state:repr}

Efficient state representation is crucial for minimising MOCS's memory footprint and enabling it to scale up to relatively large network setups.

\noindent\textbf{Packet and Rule Indexing. }In MOCS, only a single instance of each packet and rule that can appear in the modelled network is kept in memory. An index is then used to associate queues and flow tables with packets and rules, with a single bit indicating their presence (or absence). This data structure is illustrated in Figure \ref{fig:ds-layout}.
 For a data packet, a value of $1$ in the $pq$ section of the entry indicates that infinite copies of it are stored in the packet queue of the respective switch. A value of $1$ in the \emph{fq} section indicates that a single copy of the packet is stored in the forward queue of the respective switch. A value of $1$ in the $\mathit{rq}$ section indicates that a copy of the packet sent by the respective switch (when a \emph{nomatch} transition is fired) is stored in the controller's request queue. For a rule, a value of $1$ in the \emph{ft} section indicates that the rule is installed in the respective switch's flow table. A value of $1$ in the $\mathit{cq}$ section indicates that the rule is part of a \emph{FlowMod} message in the respective switch's control queue.

\begin{figure}[h]
	\centering
	\captionsetup{width=1\textwidth}
		\vspace{-.3cm}
	\includegraphics[width=1\linewidth]{figures/rule-ds.pdf}
	\caption{Packet (left) and rule (right) indices}
	\label{fig:ds-layout}
	\vspace{-.3cm}
\end{figure}

The proposed optimisation enables scaling up the network topology by minimising the required memory footprint. For every switch, MOCS\ only requires a few bits in each packet and rule entry in the index.

\noindent\textbf{Discovering equivalence classes of packets. }Model checking with all possible packets including all specified fields in the OpenFlow standard would entail a huge state space that would render any approach unusable. Here, we propose the discovery of equivalence classes of packets that are then used for model checking. We first remove all fields that are not referenced in a statement or rule creation or deletion in the controller program. Then, we identify packet classes that would result in the same controller behaviour. Currently, as with the rest of literature, we focus on simple controller programs where such equivalence classes can be easily identified by analysing static constraints and rule manipulation in the controller program. We then generate one representative packet from each class and assign it to all network switches that are directly connected to end-hosts; i.e. modelling clients that can send an arbitrarily large number of packets in a non-deterministic fashion. We use the minimum possible number of bits to represent the identified equivalence classes. For example, if the controller program exerts different behaviour if the destination {\sc tcp} port of a packet is $22$ (i.e.\ destined to an {\sc ssh} server) or not, we only use a 1-bit field to model this behaviour.

\noindent\textbf{Bit packing. }We reduce the size of each recorded state by employing bit packing using the \texttt{int32} type supported by {\sc Uppaal}, and bit-level operations for the entries in the packet and rule indices, as well as for the packets and rules themselves.

redpajama_set_name: RedPajamaArXiv