## 7 The TFL-Free Property
### Algorithm for TFL-Free SDN Updating
#### 7.2.1 Algorithm Overview
When analyzing Definition 5, we can interpret that a TFL occurs in the data plane due to the violation of the causal order delivery of the relevant OpenFlow message _FlowMod_, and consequently, a packet or a flow of packets starts to loop between the underlying switches. Thus, and in order to prove that the algorithm is TFL-free, it is sufficient to demonstrate that there is no data packet flow that holds with the conditions specified in the TFL pattern of Definition 5. To accomplish the proof, we focus on the packet \(pkt\) that triggers the TFL pattern. The following theorem proves this observation. The algorithm guarantees that \(\
exists\) a data packet \(pkt_{k}\in pflow_{\tau}\mid\ pflow_{\tau}\
cong match_{\lambda}\), such that (i) \(SdM(m^{\prime})\ \to\ FwdP(pkt_{k})\) and (ii) \(DlvMP(pkt_{k},t_{i})\ \to\ DlvMP(m,t_{i}^{\prime})\) where \(m,m^{\prime}\
cong match_{\lambda}\) and \(SdM(m)\ \to\ SdM(m^{\prime})\). Let us assume that the Algorithm 1 and the Algorithm 2 store knowledge of the latest message/packet \(mp\in MP\) sent from the same process \(p_{i}\in P\) to another process, through a local matrix named \(ForDelivered_{i}\) that has the same structure as the delivery matrix (for more details, see the structure description subsection). Therefore, for this proof, we consider this additional instruction in both mentioned algorithms: (6)\(ForDelivered_{i}[i,j]=t\). This hypothetical instruction allows building a matrix that considers the message(s)/packet(s) that belong(s) to the causal history of a message/packet \(mp\) and that has (have to be delivered before \(mp\) to a process \(p_{j}\). Thus, if \(ForDelivery_{i}[i,j]\) is less than or equal to \(Delivery_{j}[i,j]\), this means that all message(s)/packet(s) that causally depend(s) on \(mp\) has (have) already been delivered to \(p_{j}\). On the other hand, if \(ForDelivery_{i}[i,j]\) is greater than \(Delivery_{j}[i,j]\), this means that some of the message(s)/packet(s) that causally depend(s) on \(mp\) has (have) not been delivered to \(p_{j}\). This is proven by contradiction. Let us assume that there is a packet \(pkt_{k}\in pflow_{\tau}\), such that:

1. \(SdM(m)\ \to\ FwdP(pkt_{k})\) According to Definition 5, this is by transitivity since \(SdM(m)\ \to\ SdM(m^{\prime})\) and \(SdM(m^{\prime})\ \to\ FwdP(pkt_{k})\), such that \(m\) and \(pkt_{k}\) have \(rp_{i}\) as a common destination. 2. \(DlvMP(pkt_{k},t_{i})\ \to\ DlvMP(m,t_{i}^{\prime})\)

The existence of a \(pkt_{k}\) under the mentioned Conditions 1 and 2 implies that \(ForDelivery_{cp}[cp,rp_{i}]\ >\ Delivery_{rp_{i}}[cp,rp_{i}]\) when \(rp_{i}\) receives \(pkt_{k}\). However, and based on the proof of [6], this cannot occur as the algorithm allows the delivery of \(pkt_{k}\) to \(rp_{i}\) only when \(ForDelivery_{cp}[cp,rp_{i}]<=Delivery_{rp_{i}}[cp,rp_{i}]\), which contradicts the initial assumption. ## 8 Scenario Description

We present the example of Figure 6 to illustrate how our algorithm works. This example shows two independent updating processes within the same topology. Note that updating processes in OpenFlow-based SDNs are independent as forwarding decisions are flow-based: each packet flow is determined by match fields, as well as by update messages disseminated by the controller to update the forwarding tables of switches. The two updating processes shown in Figure 6 are distinguished by means of two different colors, corresponding to a \(match_{1}\) in purple and a \(match_{2}\) in blue. In both examples, data packets that interleave with the update messages sent from the controller (\(cp\)) (the \(cp\) is not depicted in Figure 6) and installed into the switches \(source\), \(S_{1},S_{2},\ldots,S_{n}\) (\(rp_{src},rp_{1},rp_{2},\ldots,rp_{n}\)) may enter into TFLs between all intermediate switches \(rp_{1},rp_{2},\ldots,rp_{n}\). For brevity, only the update forwarding process corresponding to \(match_{1}\) is explored. However, and for completeness, Table 1 and Tables 1 and 2 in Appendix 0.A include the information related to both matches.