## 7 The TFL-Free Property
### Modeling the TFL Pattern from a Causal Perspective  
In this subsection, we analyze the TFL phenomenon during OpenFlow-based SDN updates by using the scheme of the happened-before relation (See Definition 1). Figure 4 illustrates the generic scenario in which an out-of-order execution of messages/packets leads to a TFL during updates. In this scenario, the topology is composed of an OpenFlow controller and \(n\) OpenFlow switches. According to our network model (see Section 5), the set of processes for this scenario is \(P=\{cp,rp_{src},rp_{1},rp_{2},\dots,rp_{n},rp_{dst}\}\) where \(cp\) is the OpenFlow controller, \(rp_{src}\) and \(rp_{dst}\) represent, respectively, the \(Source\) and the \(Destinations\)switches, and \(rp_{1}\), \(rp_{2},\dots,rp_{n}\) represent the intermediateswitches \(S_{1},S_{2},\dots,S_{n}\). Initially, each intermediate routing process \(rp_{i}\), except \(rp_{n}\), contains an entry \(r\) directing a \(pflow\in PFLOW\) to its \(rp_{i+1}\) (see the solid lines in Figure 4a). Due to a network policy change, \(pflow\) should be forwarded from \(rp_{n}\) to \(rp_{1}\) (see the dashed lines in Figure 4a). To this end, the \(cp\) starts by instructing each \(rp_{i}\), except \(rp_{n}\), to delete the entry directing \(pflow\) to its \(rp_{i+1}\) and then instructs again each \(rp_{i}\), except \(rp_{1}\), to install an entry directing \(pflow_{\tau}\) to its \(rp_{n-1}\). In an OpenFlow-based SDN, the \(cp\) has to send \(2\times(n-1)\) controller-to-switch OpenFlow messages of type _FlowMod_. For brevity, and as it is sufficient to express the generality of the phenomenon, Figure 4b depicts only one message (Message (1) depicted in the dashed line) for deleting the rule in \(rp_{1}\) and all the other messages (from (2) to (n)) for adding the new forwarding path from \(rp_{n}\) to \(rp_{1}\). The communication diagram of Figure 5, which corresponds to the generic scenario of Figure 4b, is used to characterize the phenomenon. As shown, the \(cp\) starts by sending to \(rp_{1}\) a \(FlowMod\) message \(m_{1}=(cp,1,(match,delete),rp_{1})\) of command type \(delete\) and \(match\) as a match, where \(pflow\)\(\hat{=}\)\(match\), and then, it sends to \(rp_{2}\) a \(FlowMod\) message \(m_{2}=(cp,2,(match,add),rp_{2})\) of command type \(add\) and also to \(m_{1}\), \(match\) as a match, as it is about forwarding the same packet flow \(pflow\). The rest of the OpenFlow messages from \(m_{i}\) to \(m_{j}\) (represented in Figure 4b by Messages (3),..., (n)) are sent to their corresponding \(rp\) to add the entries directing \(pflow\) from \(rp_{n}\) to \(rp_{1}\). Upon the reception of the messages, and due to the asynchronous communication between the controller and all the underlying switches, \(rp_{n}\), \(rp_{n-1}\),...and \(rp_{2}\) receive their messages and install the entries while packets \(pkt_{i}\in pflow\) hit \(rp_{n}\), directing them to \(rp_{1}\) (see Figure 5). Hence, \(pkt_{n}\) enters \(rp_{1}\) before \(m_{1}\) is delivered to \(rp_{1}\) (see Figure 5). Consequently, \(pkt_{n}\) matches the entry \(r\) already installed in \(rp_{1}\) directing all \(pkt_{i}\in pflow\) to \(rp_{2}\). Finally, \(rp_{1}\) ends by redirecting \(pkt_{n}\) to \(rp_{2}\) (see the solid line between \(S_{1}\) and \(S_{2}\) in Figure 4b), which generates a TFL. Indeed, the fact that \(pkt_{n}\) is delivered to \(rp_{1}\) and went back through \(rp_{1}\) means that \(pkt_{n}\) has already entered into a TFL. Figure 4: The generic Transient Forwarding Loop (TFL) scenario: (**a**) initial and final forwarding paths; (**b**) a sequence of messages to redirect a \(pflow\) from \(S_{n}\) to \(S_{1}\) ends with a TFL. We define below an abstraction of the TFL pattern in SDN, as a specification of Lamport's happened-before relation to express the phenomenon from a causal perspective. **Definition 5**.