AllSynth: Transiently Correct Network Update Synthesis Accounting for Operator Preferences

Abstract

The increasingly stringent dependability requirements on communication networks as well as the need to render these networks more adaptive to improve performance, demand for more automated approaches to operate networks. We present AllSynth, a symbolic synthesis tool for updating communication networks in a provably correct and efficient manner. AllSynth automatically synthesizes network update schedules which transiently ensure a wide range of policy properties (expressed in the LTL logic), also during the reconfiguration process. In particular, in contrast to existing approaches, AllSynth symbolically computes and compactly represents all feasible solutions. At its heart, AllSynth relies on a novel, two-level and parameterized use of BDDs which greatly improves performance. Indeed, AllSynth not only provides formal correctness guarantees and outperforms existing state-of-the-art tools in terms of generality, but often also in terms of runtime as documented by experiments on a benchmark of real-world network topologies.

1 Introduction

A more automated operation of communication networks is considered one of the most important research problems in networking today, for two main reasons. First, communication networks and their configurations are highly complex, forcing operators to become “masters of complexity” [24]; many major Internet outages over the last years were caused by human errors [5, 12, 15]. Today’s manual approach hence stands in stark contrast to the increasingly stringent dependability requirements on communication networks, which are a critical infrastructure of our digital society. Second, network traffic is not only growing explosively but also features much temporal and spatial structure [4, 6, 48]; this introduces a significant potential to improve operational efficiency by rendering networks more adaptive towards the actual traffic patterns they serve.

Motivated by the vision of more automated networks [17], over the last years, great efforts were made in laying the foundations for automated network verification, and in designing synthesis tools [3, 16, 27, 42, 45]. Furthermore, motivated by the benefits of more adaptive network operations, e.g., to improve availability and performance [28], automated tools for consistently updating network configurations have been developed [11, 23, 38, 43, 46] which overcome the limitations of existing hand-crafted algorithms [2, 34, 37]. However, the computation of provably consistent network update schedules remains challenging, due to the required performance and expressiveness. The performance requirements are multidimensional: network update schedules should not only be quickly computable but also account for operator preferences, like requiring that certain switches or routers are updated first. However, existing approaches only provide one update sequence that may not be preferred by the network operator.

Our Contributions. We present an automated network update synthesis tool, AllSynth, that computes and represents in a compact BDD form all correct update sequences that respect various logical properties expressible in linear temporal logic (LTL) [41] like reachability, waypointing and service chaining. AllSynth comes with formal correctness guarantees and for situations in which provably no simple update schedule exists, it can make suggestions for alternative solutions (where the same switch is updated multiple times).

Despite being more general, AllSynth significantly outperforms state-of-the-art tools in terms of runtime on all non-trivial real-world networks from the standard Topology Zoo benchmark [29]. The update synthesis problem solved by AllSynth is NP-hard, even if restricted to preserving the basic loop-freedom and waypointing properties [34]. To combat the complexity of the problem, AllSynth exploits a novel two-level use of binary decision diagrams (BDDs) [32] to compactly encode not only the network topology and policy invariant, but also the set of all correct update sequences.

The fact that AllSynth computes all feasible update sequences enables future use cases for the tool, such as finding an optimal schedule, providing multiple alternative solutions and filtering based on operator requirements (e.g. some switches must be updated before the rest or in a certain order). The source code of AllSynth and all our experimental artefacts are available at [31].

Related Work. Motivated by the benefits of adaptive and software-defined (i.e., programmable) communication networks [30], as well as the increasingly stringent dependability requirements, the question of how to correctly update network configurations has received much attention over the last years. A recent survey summarizes over one hundred approaches [19].

In their seminal work, Reitblatt et al. [43] showed that a strong per-packet consistency can be achieved using packet versioning during reconfigurations. Their approach, which was subsequently studied intensively in the literature [8, 10, 20, 25, 26, 33, 40], has the drawback that it requires packet header modifications and additional memory at the nodes: switches and routers need to store forwarding rules for each version.

A clever alternative approach, introduced by Mahajan and Wattenhofer [37], schedules batches of updates over time, where the set of updates within a batch can take effect in any order without harming consistency. This approach has also been explored extensively already [2, 14, 21, 34,35,36, 47], however, it can only be used to provide a subset of the consistency properties of [43]. This in turn motivated hybrid approaches such as FLIP [46]. Interestingly, similar to AllSynth, FLIP also supports alternative solutions in case a simple update cannot be found. However, in contrast to FLIP which relies on a heuristic algorithm, AllSynth only presents alternative solutions in case a simple solution provably does not exist. Furthermore, while FLIP resorts to a packet tagging alternative (which consumes header space and switch memory), AllSynth is light-weight and fully symbolic approach aiming at updating nodes multiple times.

The need for supporting more general or even customizable consistency properties [49] as well as more automated synthesis approaches [18, 23, 39] has already received attention in the literature as well. However, our approach is the first one that is using the BDD-based technology for the synthesis and representation of all correct network updates. The competing tool NetSynth [38] for update synthesis is relying on an incremental enumeration of candidates of update sequences that are then verified by external model checkers, like NuSMV [13], and the tool terminates as soon as the first correct update sequence is found.

2 A Model for Update Synthesis

Before we formally define our problem, we shall provide an intuitive motivation for the update synthesis problem. In Fig. 1 we see a simple network with four nodes (routers). Packets from the source node s are forwarded to the destination node d along the solid edges (links) that represent the initial routing configuration. The network operator aims to change this routing to an alternative one represented by the dashed edges. The task is to schedule the order of node updates (changing the forwarding function at the updated node from the solid edge to the dashed one) so that in every intermediate routing configuration we preserve the reachability between s and d and at the same time always visit the waypoint node $v_1$ (representing for example a firewall).

Fig. 1.

Update synthesis problem

If the node s is updated first, the new routing will follow the path $s, v_2, d$ which preserves the reachability property but not the waypointing. On the other hand, if we first update the node $v_2$, we create an undesirable forwarding loop $s, v_2, v_1, v_2, v_1, \ldots$ which breaks the reachability property. Hence the only option is to update first the node $v_1$, after which we have a correct forwarding path $s, v_1, d$ satisfying both reachability and waypointing. After this we can update the node $v_2$ because this update does not change the forwarding path and lastly, we update the node s that completes the update sequence from the initial to the final routing. We are now ready to provide the formalization of the update synthesis problem.

We model the network as a multigraph, allowing us to describe multiple connections between nodes (i.e., switches or routers, which are treated as synonyms in the following); these connections can have different quantitative attributes (e.g. latency). Henceforth, we adopt graph-theory terminology and refer to such connections or links as edges.

Definition 1 (Network Topology)

A network topology is a directed multigraph $G = (V,E,\mathsf {src},\mathsf {tgt})$ where V is the set of nodes, E is the set of edges and $\mathsf {src},\mathsf {tgt}:E \rightarrow V$ are respectively the source and target functions.

In order to route traffic from a node $v_0$ to a node $v'$, each node v has a forwarding rule that specifies an appropriate outgoing edge e such that $\mathsf {src}(e)=v$. This rule can be per-flow or apply to multiple flows; in the following, we do not explicitly distinguish between the two scenarios. Not all nodes need to have defined their forwarding edge (e.g. the target node $v'$ or the nodes that are not involved in packet forwarding from $v_0$ to $v'$). We capture this formally by the notion of a routing configuration.

Definition 2 (Routing Configuration)

A routing configuration, or routing for short, in a network topology $G = (V,E,\mathsf {src},\mathsf {tgt})$ is a partial function $\rho :V \rightharpoonup E$ such that $\mathsf {src}(\rho (v)) = v$ for all $v \in V$ where $\rho (v)$ is defined.

For a given network topology $G = (V,E,\mathsf {src},\mathsf {tgt})$ with the source node $v_0 \in V$, a routing configuration $\rho$ defines a unique sequence of edges (a path) that is finite if the routing is loop free; otherwise it is infinite. In the finite case, the path is given by $\pi = e_0e_1\cdots e_n$ such that $\rho (\mathsf {tgt}(e_{i-1})) = e_{i}$ for all i, $0 \le i \le n$, where by convention $\mathsf {tgt}(e_{-1})=v_0$ and where $\rho (\mathsf {tgt}(e_n))$ is undefined. The corresponding sequence of traversed nodes is then $\overline{\pi } = \mathsf {src}(e_0)\mathsf {src}(e_1)\cdots \mathsf {src}(e_n) \mathsf {tgt}(e_n)$. In the infinite case, the path is given by $\pi = e_0e_1\cdots$ such that $\rho (\mathsf {tgt}(e_{i-1})) = e_{i}$ for all $i \ge 0$ where as before $\mathsf {tgt}(e_{-1})=v_0$. The sequence of traversed nodes is given by the infinite sequence $\overline{\pi } = \mathsf {src}(e_0)\mathsf {src}(e_1)\cdots$. If $\overline{\pi }=v_0 v_1 \ldots$ is a (finite or infinite) sequence of nodes then we refer to its suffix $v_i v_{i+1} \ldots$ by $\overline{\pi }_i$ and to the initial node $v_0$ by $\overline{\pi }[0]$. For a node $v_0 \in V$ and routing $\rho$, we let $\pi _{\rho }(v_0)$ denote the unique (finite or infinite) path induced by $\rho$ from the source node $v_0$ and let $\overline{\pi }_{\rho }(v_0)$ be the corresponding sequence of traversed nodes.

2.1 Routing Policies

We shall now define an LTL-based logic [41] that allows us to describe the policy of acceptable routings (both statically and transiently).

Definition 3 (Policy Syntax)

For a network topology $G = (V, E, \mathsf {src}, \mathsf {tgt})$, a policy $\varphi$ is constructed according to the following LTL-based abstract syntax, where $v \in V$:

$$ \varphi :\,\!:= \mathsf {true}\mid v \mid \lnot \varphi \mid \varphi \wedge \varphi \mid \mathsf {NoLoop}\mid X\,\varphi \mid \varphi \,U\,\varphi \ . $$

In addition to the classical LTL operators, our logic includes a loop freedom predicate. We now give the formal semantics of our logic, interpreted both on infinite and finite paths [22].

Fig. 2.

Encoding of standard policies where $v,d \in V$, $\emptyset \not =W \subseteq V$ and $\omega \in V^*$

Definition 4 (Policy Semantics)

For a network topology $G = (V,E,\mathsf {src},\mathsf {tgt})$, satisfaction of a policy $\varphi$ by a path $\pi \in E^* \cup E^{\omega }$, written $\pi \models \varphi$, holds iff the corresponding sequence of traversed nodes $\overline{\pi }$ satisfies $\overline{\pi } \models \varphi$, defined inductively on the structure of $\varphi$ as follows:

$$\begin{aligned}&\overline{\pi } \models \mathsf {true}\,\,&\,&\text { always} \quad \quad&\,&\overline{\pi } \models v \,\,&\,&\text { iff }\,\, \overline{\pi }[0] = v\\&\overline{\pi } \models \lnot \varphi \,\,&\,&\text { iff }\,\, \overline{\pi } \not \models \varphi \quad \quad&\,&\overline{\pi } \models \varphi _1 \wedge \varphi _2 \,\,&\,&\text { iff }\,\, \overline{\pi } \models \varphi _1 \text { and } \overline{\pi } \models \varphi _2\\&\overline{\pi } \models \mathsf {NoLoop}\,\,&\,&\text { iff }\,\, \overline{\pi } \text { is finite} \quad \quad&\,&\overline{\pi } \models X\,\varphi \,\,&\,&\text { iff } \,\, \overline{\pi }_1 \models \varphi \\&\overline{\pi } \models \varphi _1\,U\,\varphi _2 \quad&\,&\text { iff }\,\, \exists j \forall i < j. \overline{\pi }_j \models \varphi _2&\,&\text { and } \overline{\pi }_i \models \varphi _1.&\,&\end{aligned}$$

We now formulate some standard routing policies as presented in Fig. 2. The simplest policy, $\mathsf {Reach}(d)$, specifies that the destination node d must eventually be reached while $\mathsf {Waypoint}(v,d)$ asks that any path reaching the destination d must necessarily pass through waypoint node v. For multiple alternative waypoints, $\mathsf {MultiWaypoint}(W,d)$ specifies that any path reaching destination d must necessarily pass through either of the waypoints in W. Finally, $\mathsf {Service}(\omega ,d)$ ensures that the sequence of waypoints in $\omega$ is visited in this fixed order.

2.2 Update Synthesis

In the following we assume a fixed network topology $G = (V,E,\mathsf {src},\mathsf {tgt})$. An update $u \in E \cup V$ on G under a current routing configuration $\rho$ specifies that the source node of edge u (if $u \in E$) must now forward its traffic along u or that the routing for the node u (if $u \in V$) is set to undefined. We write $\rho ^u$ for the new routing configuration, defined for any $v \in V$ as

$$ \rho ^u(v) = {\left\{ \begin{array}{ll} u &{} \text {if } u \in E \text { and } v = \mathsf {src}(u) \\ undefined &{} \text {if } u=v \\ \rho (v) &{} \text {otherwise.} \end{array}\right. } $$

We inductively extend this notation to sequences of updates by letting $\rho ^{\varepsilon } = \rho$ and $\rho ^{wu} = (\rho ^{w})^u$ for any $w \in (E\cup V)^*$ and $u \in E\cup V$. An update sequence may in general contain an arbitrary number of updates that change multiple times the routing of the same node, however an important set of update sequences is the class of simple update sequences, meaning that each update changes the routing for a given node v from its initial routing $\rho _i(v)$ directly to its final routing $\rho _f(v)$.

Definition 5 (Simple Updates)

Let $\rho _f$ be the final routing. An update u is simple if $\rho _f(\mathsf {src}(u)) = u$ whenever $u \in E$ and $\rho _f(\mathsf {src}(u))$ is undefined whenever $u \in V$. A simple update sequence is then a sequence of simple updates, where each update appears at most once.

A basic property of simple update sequences is that any reordering results in the same final routing configuration i.e., if w is a simple update sequence and $w'$ is any permutation of w, then $\rho ^w = \rho ^{w'}$ for any routing $\rho$.

Although any reordering of a simple update sequence yields the same final routing configuration, the intermediate routing configurations induced by each update may not respect a given policy invariant. This is also the case for general update sequences. We therefore say that an update sequence is correct with respect to a policy $\varphi$ and a node v, if the unique path from v induced by any intermediate routing configuration satisfies $\varphi$.

Definition 6 (Update Correctness)

An update sequence $w \in (E \cup V)^*$ on network topology G with initial routing configuration $\rho$ is correct with respect to source node $v_0$ and a policy $\varphi$, if $\pi _{\rho ^{w'}}(v_0) \models \varphi$ for any prefix $w'$ of w.

The network update synthesis problem is thus the problem of constructing a correct update sequence that updates an initial routing to a desired final routing.

Definition 7 ((Simple) Update Synthesis Problem)

Given a topology G, an initial routing configuration $\rho _i$, a final routing configuration $\rho _f$, source node $v_0 \in V$ and a policy $\varphi$, the simple update synthesis problem asks to construct a simple update sequence w that is correct with respect to $v_0$ and $\varphi$ such that $\rho _i^w = \rho _f$. The update synthesis problem omits the requirement that the constructed update sequence is simple.

In the following, we let $P = (G,\rho _i,\rho _f,v_0,\varphi )$ denote a (simple) update synthesis problem and say that a constructed update sequence w that satisfies the conditions above is a solution. For any simple update synthesis problem P, the set of solutions is always finite. This is not the case for the general problem as there may be infinitely many (longer and longer) solutions.

While much prior work focused on simple update problems, there are examples which are only solvable with a general solution (as supported by our approach). To see this, consider the network topology in Fig. 3a with initial and final routings visualised respectively as solid and dashed lines in Fig. 3b. We fix the source node s and the policy $\varphi = \mathsf {Waypoint}(v_2,d) \wedge \mathsf {Reach}(d)$ requiring that waypoint $v_2$ must be visited before reaching d. An update of any node v from the initial to the final routing violates $\varphi$—either by introducing a loop or it bypasses the waypoint. Hence there is no correct simple update sequence. However, the update sequence that first updates s to route to $v_2$, followed by the update of the nodes $v_1$, $v_2$ and $v_3$ and finally updating s again to route to $v_3$ is a correct update sequence.

2.3 Simple Update Sequence Reordering

In case of simple update sequences, we shall now argue that for routing policies that (i) include the preservation of reachability between the source and a target, and (ii) for which it holds that once a packet is delivered, no further routing is defined from the target node, we can reorder certain updates in the sequence without invalidating the correctness of the sequence. More specifically, we shall show that if a node routing is to be changed from undefined to some concrete edge, we can safely schedule such updates (in any order) to the very beginning of the update sequence. Similarly, all nodes that change their current routing into undefined can be scheduled (again in arbitrary order) at the end of the update sequence.

Fig. 3.

Update synthesis problem with only a general solution

Lemma 1

Let w be a solution to a simple update synthesis problem $P = (G,\rho _i,\rho _f,v_0,\varphi )$ where $\varphi = \mathsf {Reach}(d) \wedge \varphi '$ for any policy $\varphi '$ and where $\rho _i(d)$ and $\rho _f(d)$ are undefined.

• 1. If $w = w_1\circ u \circ w_2$ where $u \in E$ is an update s.t. $\rho _i(\mathsf {src}(u))$ is undefined then $u \circ w_1 \circ w_2$ is a solution to P.

• 2. If $w = w_1\circ u \circ w_2$ where $u \in V$ updates the routing in u to undefined then $w_1 \circ w_2 \circ u$ is a solution to P.

Fig. 4.

Counter example for $\mathsf {Waypoint}(v_2,d)$; initial/final routing is in solid/dashed lines

Lemma 1 can be used to identify all nodes that have an undefined forwarding function in $\rho _i$ and schedule them to the beginning of the update sequence. Symmetrically, all updates that change a node forwarding to an undefined value (in the routing $\rho _f$), can be placed at the end of the update sequence. This may simplify the synthesis of the update sequence by analysing only the nodes that have a defined forwarding function both in the initial and final routing.

The requirement in Lemma 1 that the policy must enforce at least the reachability of d is essential, as illustrated in Fig. 4 where $e_2 \circ e_3 \circ e_4$ is a correct update sequence preserving $\mathsf {Waypoint}(v_2,d)$. This is because until the last update, the destination d is not reachable and hence the waypointing policy trivially holds. However, even though the routing of $v_1$ is undefined in the initial routing, moving the update $e_4$ to the beginning of the update sequence creates a transient forwarding following the path $e_1e_4$ and violates $\mathsf {Waypoint}(v_2,d)$.

Fig. 5.

AllSynth workflow

3 The AllSynth Tool and the Synthesis Algorithm

The diagram in Fig. 5 illustrates the main components of AllSynth. The inputs to AllSynth are the network topology G, a policy of interest $\varphi$, as well as the initial routing $\rho _i$ and final routing $\rho _f$ from the node $v_0$.

From the input network topology G, a BDD representation of the edges in G is combined with the input policy $\varphi$ and a source node $v_0$ to produce a BDD representing all routing configurations $\rho$ where the unique path $\pi _{\rho }(v_0)$ satisfies $\varphi$. This BDD is then in turn combined with the initial and final routing configurations $\rho _i$ and $\rho _f$, to construct a BDD representation of all correct update sequences.

We shall now present our algorithmic solution to the update synthesis problem, based on a symbolic encoding of routing configurations using BDDs. This encoding allows for an efficient fixed-point computation of those routing configurations that satisfy a given routing policy, and subsequently to find a correct update sequence solving the synthesis problem.

Boolean decision diagrams [32] are data structures for the compact representation of a Boolean function. A BDD is a rooted directed acyclic graph (DAG), with nonleaf nodes labeled by Boolean variables, and leaf nodes labeled with 0 (false) or 1 (true). Each node that is labelled by a variable has two outgoing edges, a solid one representing the true assignment to the variable and a dotted one for the false assignment. By following the paths from the root to the leaf labelled with 1, we obtain all satisfying Boolean assignments. BDDs were introduced by Lee [32] and later Bryant [9] presented their reduced ordered version (ROBDD), where the ordering between the Boolean variables are fixed along each path from the root to a leaf, and isomorphic parts are combined. We show how to exploit ROBDDs for solving the update synthesis problem.

First, let us recall how to encode subsets of a finite set S using Boolean expressions—hence ROBDDs. The encoding is relative to a given enumeration $s_0, s_1, s_2, \ldots s_{|S|-1}$ of S and it is based on $n=\left\lceil {\log (|S|)}\right\rceil$ Boolean variables $\mathbf {x}=x_1, x_2, \ldots , x_n$. Now, any truth assignment $\mu$ to $\mathbf {x}$ may be seen as a binary encoding of a natural number $n(\mu )\in \mathbb {N}$ and hence an encoding of the $n(\mu )$’th element $s_{n(\mu )}\in S$. We shall use the short notation $s(\mu )$ for the element $s_{n(\mu )}$ as well as the notation $\mathbf {x}(s)$ to denote a Boolean expression over $\mathbf {x}$ encoding the singleton-set $\{s\}$. Now any Boolean expression $t(\mathbf {x})$ over $\mathbf {x}$ may be seen as encoding the subset $[\![ t(\mathbf {x})]\!]=\{\, s_{n(\mu )} \,|\, \mu \,\,\mathrm {satisfies}\,\, t(\mathbf {x})\, \}\subseteq S$.

Example 1

Consider the network topology in Fig. 6a with the nodes $V=\{v_0,v_1,v_2,v_3\}$ enumerated by the given indices. We encode any subset of V by a Boolean expression over two Boolean variables $x_1, x_2$—note that the encoding of e.g. $\{v_1\}$ is $\mathbf {x}(v_1)=\lnot x_1 \wedge x_2$ as the binary encoding of $v_1$ is 01. Conversely, the subset identified by the Boolean expression $t\equiv \lnot x_1 \vee \lnot x_2$ is $[\![ t]\!] = \{ v_0, v_1, v_2 \}$ as the binary encoding of $v_0, v_1$, $v_2$ are 00, 01, 10, respectively.

Fig. 6.

Running example and encoding of the transition function

BDD Encoding of Routing Configurations. Let $G = (V,E,\mathsf {src},\mathsf {tgt})$ be a network topology and let $v\in V$. We denote by $E_v$ the set of edges having v as a source-node, i.e. $E_v= \{e \in E \mid \mathsf {src}(e) = v\}$. Now, a routing configuration $\rho :V \rightharpoonup E$ is isomorphic to indicating for each node v whether $\rho (v)$ is defined and if so to identify an element from $E_v$. For the Boolean encoding of (sets of) elements from $E_v$ we use, as described above, $\left\lceil {\log (|E_v|)}\right\rceil$ Boolean variables $\mathbf {z}_v$. To indicate the definedness of $\rho (v)$, we use an additional Boolean variable $z^d_v$. To encode the possible transitions between nodes v and $v'$ enabled by a given routing configuration $\rho$, we use Boolean variables $\mathbf {x}$ for encoding the source node v and equally many Boolean variables $\mathbf {y}$ for encoding the target node $v'$. The following Boolean expression T encodes the possible transitions:

$$ T(\mathbf {x},\mathbf {z}_{v_0},\ldots ,\mathbf {z}_{v_k}, z_{v_0}^d, \ldots , z_{v_k}^d, \mathbf {y})= \bigvee _{v\in V} \bigvee _{e\in E_v} \big ( \mathbf {x}(v)\wedge \mathbf {z}_v(e)\wedge z_v^d\wedge \mathbf {y}(\mathsf {tgt}(e))\big ) $$

where $V=\{v_0,\ldots ,v_k\}$.

Example 2

Reconsidering the network topology from Fig. 6a, we shall use three Boolean variables $z_1, z_2$, $z_3$ for encoding routing configurations in terms of their choice of successor-node from $v_0, v_1$ and $v_2$¹. Using the encoding of nodes from Example 1, the possible transitions between nodes are given by the Boolean expression T in Fig. 6c. The resulting unique ROBDD in Fig. 6b with only 11 non-leaf nodes illustrates the compactness of the ROBDD data structure (the missing edges lead to 0). The highlighted path encodes the transition (routing) from $v_0$ to $v_1$ under the initial routing. Here the chosen ordering of the Boolean variables is crucial. Alternative orderings, e.g. with the $\mathbf {z}$ variables being tested first respectively last results in ROBDDs with 25 respectively 17 non-leaf nodes.

BDD Encoding of Routing Policies. Now let $G = (V,E,\mathsf {src},\mathsf {tgt})$ be a network topology and let $\varphi$ be a routing policy expressed in the LTL logic of Definition 3. Using Boolean variables $\mathbf {x}$ for encoding nodes and Boolean variables $\mathbf {z}$ for encoding routing configurations², we shall construct an ROBDD $B_\varphi (\mathbf {x},\mathbf {z})$ such that: $(v,\rho )\in [\![ B_\varphi (\mathbf {x},\mathbf {z})]\!]$ if and only if $\pi _\rho (v)\models \varphi$ where $\pi _\rho (v)$ is the unique path starting in the node v following the the routing configuration $\rho$.

Definition 8

Let $G = (V,E,\mathsf {src},\mathsf {tgt})$ be a network topology and $\varphi$ a routing policy. We define the ROBDD $B_\varphi (\mathbf {x},\mathbf {z})$ inductively on $\varphi$ as follows:

$$\begin{aligned} B_{\mathsf {true}}(\mathbf {x},\mathbf {z})&= 1 \\ B_{v}(\mathbf {x},\mathbf {z})&= \mathbf {x}(v)\\ B_{\lnot \varphi }(\mathbf {x},\mathbf {z})&=\lnot B_\varphi (\mathbf {x},\mathbf {z}) \\ B_{\varphi _1 \wedge \varphi _1}(\mathbf {x},\mathbf {z})&= B_{\varphi _1}(\mathbf {x},\mathbf {z})\wedge B_{\varphi _2}(\mathbf {x},\mathbf {z})\\ B_{\mathsf {NoLoop}}(\mathbf {x},\mathbf {z})&\overset{\underset{\mathrm {min}}{}}{=}\forall \mathbf {y}.(T(\mathbf {x},\mathbf {z},\mathbf {y})\rightarrow B_\mathsf {NoLoop}(\mathbf {y},\mathbf {z})) \\ B_{X\varphi }(\mathbf {x},\mathbf {z})&= \exists \mathbf {y}.\big (T(\mathbf {x},\mathbf {z},\mathbf {y}) \wedge B_{\varphi }(\mathbf {y},\mathbf {z})\big )\\ B_{\varphi _1U\varphi _2}(\mathbf {x},\mathbf {z})&\overset{\underset{\mathrm {min}}{}}{=}B_{\varphi _2}(\mathbf {x},\mathbf {z}) \vee \big (B_{\varphi _1}(\mathbf {x},\mathbf {z}) \wedge \exists \mathbf {y}.\big (T(\mathbf {x},\mathbf {z},\mathbf {y})\wedge B_{\varphi _1U\varphi _2}(\mathbf {y},\mathbf {z})\big )\big ) \end{aligned}$$

Fig. 7.

Increasing approximants $B_{\mathsf {Reach}(v_3)}^n$

In the above definition we exploit that ROBDDs are closed under Boolean operations as well as Boolean quantification. In the cases $\mathsf {NoLoop}$ and $\varphi _1\,U\,\varphi _2$, the changes of Boolean variables used in the parameter lists in the right-hand sides are obtained by simple substitution of variables, an operation that may efficiently be performed on ROBDDs. Finally, note that the definitions of $B_\mathsf {NoLoop}$ and $B_{\varphi _1\,U\,\varphi _2}$ are given as minimal fixed points. These fixed points, e.g. $B_\mathsf {NoLoop}$, are obtained after a finite number of applications of the corresponding right-hand sides on increasing approximations $B^n_\mathsf {NoLoop}$, starting with $B^0_\mathsf {NoLoop}=0$, and terminating when $B^{n+1}_\mathsf {NoLoop}=B^n_\mathsf {NoLoop}$.

Lemma 2

We have $(v,\rho )\in [\![ B_\varphi (\mathbf {x},\mathbf {z})]\!]\,\,\text{ if } \text{ and } \text{ only } \text{ if }\,\, \pi _\rho (v)\models \varphi$.

Example 3

Consider the network topology from Fig. 6a with the routing policy $\mathsf {Reach}(v_3)$. Given the LTL-definition of $\mathsf {Reach}(v_3)$, the ROBDD $B_{\mathsf {Reach}(v_3)}$ is given by the limit of the following inductively defined sequence: $B_{\mathsf {Reach}(v_3)}^{n+1}(\mathbf {x},\mathbf {z})=\mathbf {x}(v_3) \vee \exists . \mathbf {y}. \big ( T(\mathbf {x},\mathbf {z},\mathbf {y})\wedge B_{\mathsf {Reach}(v_3)}^n(\mathbf {y},\mathbf {z})\big )$ with $B_{\mathsf {Reach}(v_3)}^0=0$. Figure 7 provides some of the approximants with $B_{\mathsf {Reach}(v_3)}^4$ found to be the least fixed point.

We shall denote by $B^*_\varphi (\mathbf {z})$ the ROBDD $\exists \mathbf {x}. B_\varphi (\mathbf {x},\mathbf {z})\wedge \mathbf {x}(v_0)$, where $v_0 \in V$ is the source node. Rather than using BDDs for model-checking that individual routing configurations satisfy a given policy $\varphi$ one by one, $B^*_\varphi (\mathbf {z})$ characterizes exactly in one single ROBDD the full set of routing configurations satisfying $\varphi$.

Example 4

Recall the network topology from Fig. 6a and the Boolean encoding of routing configurations and nodes from Example 2. Now consider the routing policies $W=\mathsf {Waypoint}(v_2,v_3)$ and $R=\mathsf {Reach}(v_3)$. The resulting ROBDDs for $B^*_{R}, B^*_W$ and $B^*_{W\wedge R}$ are given in Fig. 8. It can be concluded that there are 6, 6 respectively 4 routing configurations satisfying the policies R, W respectively $R\wedge W$. Moreover, both $\rho _i$ and $\rho _f$ satisfy all three policies.

Fig. 8.

Encoding of different routing policies

BDD Encoding of Update Sequences. Again let $G = (V,E,\mathsf {src},\mathsf {tgt})$ be a network topology and let $\varphi$ be a routing policy, with $\rho _i$ respectively $\rho _f$ being initial respectively final routing configuration. We shall show how to symbolically synthesize correct (simple) update sequences using BDD encodings. The basis of the synthesis is the ROBDD $B^*_\varphi (\mathbf {z})$ encoding all routing configurations that are correct with respect to $\varphi$ using Boolean variables $\mathbf {z}=\mathbf {z}_{v_0} \ldots \mathbf {z}_{v_k},z_{v_0}^d,\ldots ,z_{v_k}^d$. For simple updates it suffices to use single Boolean variables $z_{v_j}$, with $z_{v_j}$ encoding $\rho _i(v_j)$ and $\lnot z_{v_j}$ encoding $\rho _f(v_j)$, i.e. in case $\rho _f(v_j)\not =\rho _i(v_j)$. To encode a simple update between configurations $\rho$ and $\rho '$ we shall use Boolean variables $\mathbf {z}$ for encoding $\rho$ and a corresponding (distinct) sequence of Boolean variables $\mathbf {zz}$ for encoding $\rho '$. The following Boolean expression $U_\varphi ^s$ encodes the set of possible simple updates that preserve correctness with respect to $\varphi$.

$$ U_\varphi ^s(\mathbf {z},\mathbf {zz}) = B^*_\varphi (\mathbf {z}) \wedge B^*_\varphi (\mathbf {zz}) \wedge \exists i.\,\big [ z_{v_i}\wedge \lnot zz_{v_i}\wedge \bigwedge _{j\not =i}z_{v_j}= zz_{v_j} \big ] $$

Note that in this simple update the routing configuration changes for exactly one node $v_i$ from the setting in the initial configuration $\rho _i$, encoded as $z_{v_i}$, to the setting in final configuration $\rho _f$, encoded as $\lnot zz_{v_i}$. In the general case, the update can change the setting of any node arbitrarily, as given by the following Boolean expression $U_\varphi$.

$$ U_\varphi (\mathbf {z},\mathbf {zz}) = B^*_\varphi (\mathbf {z}) \wedge B^*_\varphi (\mathbf {zz}) \wedge \exists i.\,\big [ \mathbf {z}_{v_i}\not =\mathbf {zz}_{v_i}\wedge \bigwedge _{j\not =i}\mathbf {z}_{v_j}=\mathbf {zz}_{v_j} \big ] $$

Lemma 3

We have $(\rho ,\rho ') \in [\![ U_{\varphi }(\mathbf {z},\mathbf {zz})]\!]$ (resp. $[\![ U^s_{\varphi }(\mathbf {z},\mathbf {zz})]\!]$) iff $\rho \ne \rho '$ and there exists an update (resp. simple update) u such that $\rho ^u = \rho '$, $\pi _{\rho }(v_0) \models \varphi$ and $\pi _{\rho '}(v_0) \models \varphi$, where $v_0$ is the given source node.

To enable synthesis of correct (simple) update sequences, the following recursively defined ROBDD is key.

$$\begin{aligned} R^s_\varphi (\mathbf {z},\mathbf {zz}) \overset{\underset{\mathrm {min}}{}}{=}\mathbf {z}(\rho _f) \vee \exists \mathbf {zzz}. \big ( \,U^s_\varphi (\mathbf {z},\mathbf {zz}) \wedge R^s_\varphi (\mathbf {zz},\mathbf {zzz}) \big ) \end{aligned}$$

(1)

Fig. 9.

Encoding of all correct simple update-steps (a–c); unique update sequence (UUS) for $W\wedge R$ (d)

The expression encodes the set of simple updates that preserve correctness with respect to $\varphi$ while ensuring reachability of the final routing configuration.

Lemma 4

We have $(\rho ,\rho ')\in [\![ R^s_\varphi (\mathbf {z},\mathbf {zz})]\!]$ iff there exists a correct simple update sequence $w = u_0u_1\cdots u_k$ with respect to $\rho$ and $\varphi$ such that $\rho ' = \rho ^{u_0}$ and $\rho ^w = \rho _f$.

All correct, simple update sequences of length N may now be characterized by the following Boolean expression, where $\mathbf {z}^i$ are (distinct) Boolean variables encoding the routing configuration after i updates:

$$\begin{aligned} S^s_{\varphi }(\mathbf {z}^0,\ldots ,\mathbf {z}^N) = \mathbf {z}^0(\rho _i) \wedge \mathbf {z}^{N}(\rho _f) \wedge \bigwedge _{i=0}^{N-1} R_\varphi ^s(\mathbf {z}^i, \mathbf {z}^{i+1}) \end{aligned}$$

(2)

Theorem 1

We have $(\rho _0, \rho _1, \ldots , \rho _N) \in [\![ S^s_{\varphi }(\mathbf {z}^0,\ldots ,\mathbf {z}^N)]\!]$ iff there exists a simple correct update sequence $w = u_0u_1\cdots u_{N-1}$ with respect to $\varphi$ and $\rho _0$ such that $\rho _{k+1} = \rho _k^{u_k}$ for all k with $0 \le k < N$, $\rho _0 = \rho _i$ and $\rho _N = \rho _f$.

For the synthesis in the general case: simply replace $U^s_\varphi$ in (1) with $U_\varphi$ to get a ROBDD $R_\varphi$ characterizing (general) update sequences leading to $\rho _f$. Now, replace $R^s_\varphi$ with $R_\varphi$ in (2) to get a characterization of all correct (general) update sequences of length N.

Example 5

Consider again the network topology from Fig. 6a and the routing policies $W=\mathsf {Waypoint}(v_2,v_3)$ and $R=\mathsf {Reach}(v_3)$. The full sets of correct simple update-steps with respect to W, R and $W\wedge R$ are given by the ROBDDs $R^s_W, R^s_R$ and $R^s_{W\wedge R}$ given in Fig. 9(a–c). Instantiating Eq. (2) with these ROBDDs reveals that there are 3, 3 respectively 1 correct simple update sequences of length 3 with respect to the routing policies W, R respectively $W\wedge R$.

The unique simple update sequence for $W\wedge R$ (ignoring the initial and final routing configurations) is given by the ROBDD in Fig. 9(d)³. Here the values suggested for the first three Boolean variables $z_1^1,z_2^1,z_3^1$ indicate that the routing configuration after the first update is given by the edges $(v_0,v_2), (v_1,v_2),(v_2,v_3)$. Similarly, the values of the last three Boolean variables $z_1^2,z_2^2,z_3^2$ indicate the edges $(v_0,v_2),(v_1,v_3),(v_2,v_3)$ as the configuration after the second update. Note, that in case there is no correct (simple) update sequence the resulting ROBDD becomes empty (just consisting of the node false).

4 Implementation and Evaluation

Our tool AllSynth is implemented in Python and relies on a Cython wrapper [1] of the CUDD [44] package for manipulation of ROBDD. From a given network topology with the initial and final routing, the tool produces either a simple or general update sequence satisfying a given policy, as well as the information about the number of possible solutions. As all such correct solutions are symbolically represented in a compact way as an ROBDD, it is possible to generate alternative solutions without any additional computational effort.

We evaluate AllSynth against two state-of-the-art update synthesis tools, NetSynth [38] and FLIP [46]. NetSynth can compute only a simple update sequence or inform the user that there is no solution; the synthesis of general update sequences is not supported. FLIP can synthesise sequences of steps (groups of switches or routers) in which order the network can be updated, however, if such a sequence does not exist, the tool may introduce additional forwarding rules and use tagging of packets. As NetSynth and FLIP do not support general update sequences, compare the running times only for simple updates.

All experiments are executed on Ubuntu 14.04 cluster with 2.3 GHz AMD Opteron 6376 processors with 2 h timeout and 14 GB memory limit. A reproducibility package is available in [31].

We consider a scalable synthetic topology and the standard benchmark of 261 real-world network topologies from the Topology Zoo dataset [29]. The class of synthetic topologies, referred to as diamond topologies, are overtaken from the NetSynth evaluation benchmark [38] and are formed by disjoint initial and final routing paths that only share the initial and final node. The size of the problem is defined to be the sum of the lengths of the two paths—we include instances of sizes up to 2000. The Topology Zoo instances are five times sequentially concatenated in order to obtain larger topologies where the size of the update problems ranges from 20 to 679. We display the 50 most difficult instances of the problem.

We consider three classes of update policies: $\mathsf {Reach}(d)$, $\mathsf {MultiWaypoint}(W,d)$ and $\mathsf {Service}(\omega ,d)$. For $\mathsf {MultiWaypoint}(W,d)$, we let every 5th node on both the initial and final path be included in W. For $\mathsf {Service}(\omega ,d)$, the sequence $\omega$ is generated by including every 5th node that is traversed by both the initial and final path. Because the diamond update problem consists of two disjoint paths, the service chaining policy is not considered here. The policy language of NetSynth is identical to our LTL-based specifications and hence it is able to directly express all these properties. On the other hand, the policy input to FLIP enumerates all admissible subpaths that are considered, in logical disjunction. The encoding of the service chaining policy then entails an exhaustive enumeration of all paths that satisfy the service chaining policy and we therefore do not include FLIP in our service chaining experiments.

Fig. 10.

Experimental results

Results. The experiments are summarized in a number of so-called cactus plots [7] in Fig. 10, where for each method all instances of the problem are independently sorted from the fastest to the slowest one and plotted on the x-axis, and the y-axis (note the logarithmic scale) shows the increasing running time. If some curve does not reach to the right end of the plot, this means that the corresponding tool is not able to solve the remaining instances within the given timeout and memory limit. While cactus plots do not provide instance-to-instance runtime comparison, they provide an overall performance evaluation of the different tools.

For the experiments on the collection of real networks from the Topology Zoo presented in Figs. 10a and 10b, we notice that none of the tools has difficulty solving the synthesis of the plain reachability policy and it takes less than 10 s for all instances—here our approach has a slight margin. For waypointing, while FLIP is performing well on small instances, it shows a noticeable penalty once it reaches the most difficult problems where its running time quickly deteriorates and it is as the only tool not able to solve some of the largest instances. We maintain about one order of magnitude advantage over NetSynth (NS), which is the case also for service chaining.

Results for diamond topologies are given in Figs. 10c and 10d. We observe that for reachability our computation of all solutions is almost one order of magnitude faster than FLIP and several orders of magnitude faster than NetSynth (both tools terminate as soon as they find the first correct update sequence). For waypointing, we still significantly outperform NetSynth and we are almost comparable with FLIP which shows better performance at the largest instances.

In conclusion, our experiments demonstrate that AllSynth, based on the symbolic BDD technology, not only significantly outperforms state-of-the-art tools on all non-trivial real-world networks, but also provides higher generality. Indeed, AllSynth computes all solutions, compared to only one solution returned by NetSynth or a more general sequence of update steps generated by FLIP. This aspect is important for the practical usage by network operators as it allows them to iteratively choose the most suitable update sequence.

5 Conclusion

We presented an efficient approach for synthesizing correct update sequences for software-defined networks. In contrast to existing tools, our approach is fully symbolic and relies on BDD technology. As a result, we are able to represent all solutions to the update synthesis problem in a succinct binary tree, preserving generic routing policies (e.g., service chaining) that can be described in the LTL logic. Our prototype implementation of AllSynth outperforms the state-of-the-art tools NetSynth and FLIP in many scenarios (e.g., on the real-world Internet topologies), while at the same time extending the generality.

Our experiments focused on the generation of simple update sequences (at most one update per flow per switch), similar to the methodology used in NetSynth and FLIP. AllSynth however also supports a novel generalization where a switch can be updated several times. This is particularly useful for the instances of the update synthesis problem that do not have any simple solution. In this case, NetSynth does not provide any alternative (and in fact does not terminate even on relatively small negative instances); FLIP may degrade to a two-phase commit strategy that is less preferable as it requires the duplication of forwarding rules as well as additional packet header space. AllSynth instead tries to suggest a general update sequence that does not require packet tagging.