## 7 The TFL-Free Property
### Algorithm for TFL-Free SDN Updating
#### 7.2.1 Algorithm Overview  
Throughout an update, an OpenFlow-based SDN expresses message/packet-passing between processes \(P\), specifically, between the controller process \(P_{cp}\) and the set of routing processes \(P_{rp}\), or between \(P_{rp}\) themselves. Therefore, we distributed the algorithm over the \(P_{cp}\) and the set of \(P_{rp}\). It can be summarized as follows:  
* Input: The algorithm takes the list of all OpenFlow update messages and ingoing data packets as input. As described in Section 5, updates are _match_-based performed, i.e., update messages and in-fly data packets are grouped and processed by match. This allows updates of different matches to be executed concurrently without the risk of harming the TFL-free property. * Condition: Let \(match_{\lambda}\in MATCH\) be a match. All matched OpenFlow messages of type delete should be disseminated from the \(P_{cp}\) to the \(P_{rp}\) before all OpenFlow messages of type add. * Execution model: All OpenFlow update messages are asynchronously disseminated from \(P_{cp}\) to \(P_{rp}\). No upper bound on messages/data packets transmission delay is required. \(P_{cp}\) never waits for an acknowledgment message from \(P_{rp}\) once a message is delivered, and clocks of all entities are not in synchronization with each other, that is the execution model is fully asynchronous. Figure 5: The communication diagram corresponding to Figure 4.  
* Data structures: At a process-level, each process \(p_{i}\in P\) maintains a vector of control information \(CI_{i}\) to store direct dependency information between the set of messages/packets \(MP\) with respect to the corresponding _match_. Furthermore, each \(rp_{i}\in P_{rp}\) maintains a matrix \(Delivery_{i}\) to track dependency information (see the data structures' subsection below for more details) when an \(rp\) receives an \(mp\in MP\). We will also make reference to the state of the delivery matrix structure when a process \(p_{i}\) sends an \(mp\), denoted as \(ForDelivery_{i}\). * Functionally: The algorithm is implemented at the time of sending an OpenFlow message \(m\in M\) from the \(P_{cp}\), and/or at the time of forwarding a data packet \(pkt\in PKT\) from an \(rp\in P_{rp}\), and/or at the time of receiving an \(mp\in MP\) by a routing process \(rp\in P_{rp}\). At the sending of an OpenFlow message from the \(P_{cp}\), and besides the message \(m\), the algorithm encapsulates into the message a vector \(CI_{cp}\) containing control information on the send message events that directly depend on it (see Algorithm 1). Similarly, an outgoing packet \(pkt\) in the data plane piggybacks a vector \(CI_{rp}\) that carries control information of the OpenFlow message/packet send events that directly depend on it (see Algorithm 2). At the reception of an \(mp\), and based on the control information encapsulated into \(CI_{mp}\), the receiver \(rp_{j}\) decides if it can deliver \(mp\) or if it should wait for the reception of another/other \(mp^{\prime}\)(s) to then be able to deliver \(mp\) (see Algorithm 3). * Ensured properties: Based on the algorithm functionality, neither an OpenFlow message nor a packet, which share the same match, will be delivered out of causal order, ensuring the per-match causal order delivery property (see Definition 3). In Section 7.3, we prove that the presented algorithm ensures the TFL-free property. **Input:** The set of OpenFlow update messages  
**Condition:**\(\forall m\in M:(m=(cp,t_{cp},(match_{\lambda},delete),rp_{d}{}^{1})\to m^{ \prime}=(cp,t_{cp}^{\prime},(match_{\lambda},add),rp_{d}))\)  
1: \(t_{cp}:=0\), \(CI_{cp}[j]=\{\}\)\(\forall j:1\ldots N\)  
2: **for all** OpenFlow messages \(\hat{=}\)\(match_{\lambda}\)**do**  
3: \(t_{cp}:=t_{cp}+1\)  
4: \(m=(cp,t_{cp},OpenFlow\_message,rp_{i})\)  
5: \(SdM(m,CI_{cp})\)  
6: \(CI_{cp}[i]:=(cp,t_{cp})\)  
**Algorithm 2** : Switch-to-switch packet forwarding.