# An Extensible Automated Failure Localization Framework Using NetKAT, Felix, and SDN Traceroute
## 4 Use-Cases
### Performance
#### 4.4.1 Performance of the Path Matrix Component  
The Path matrix holds a mapping of links and host pairs. The framework discovers this mapping by executing queries in Felix. Thus, the number of steps required for adding information about a new link to the Path matrix is the following:  
\[T_{1}^{\text{PM}}=T_{\text{query}}^{\text{Felix}}+\underbrace{T_{\text{ insert}}^{\text{PM}}}_{\mathcal{O}(1)} =\mathcal{O}(T_{\text{query}}^{\text{Felix}}).\]  
According to [12], Felix execution depends on the number of compiled terms. These come from the five supplied descriptions: network in- and outputs, topology and policy, as well as a query. This latter always specifies long-path type queries. In a general case, where more than one link is specified by the query, the number of terms is given by the following formula where \(l\) signifies the number of links in the query:  
\[|\text{terms}|=|\text{in}|+(|p|+|t|)+l(|p|+|t|+2)+(|p|+|t|)+|p|+|\text{out}| \leq(2+l)(|p|+|t|)+2(n+l).\]  
For the initialization phase, where the framework uses only a single link, the above can be simplified to:  
\[|\text{terms}|=3(|p|+|t|)+2(n+1)=\mathcal{O}(|p|+|t|+n).\] \begin{table}
\begin{tabular}{c c} \hline \hline \(e\) & the number of links in the network \\ \hline \multirow{2}{*}{\(d\)} & the length of the longest forwarding path in the network if it acts according to specifications. \\  & This is the diameter (i.e., the longest among all shortest paths) \\  & when the network follows shortest path forwarding \\ \hline \multirow{2}{*}{\(d_{\text{PHY}}\)} & the length of the longest forwarding path in the physical network, \\  & i.e., \(d_{\text{PHY}}=d\) if it follows specifications \\ \hline \(n\) & the number of hosts in the network \\ \hline \(h\leq n^{2}\) & the number of tested host pairs in the network \\ \hline \(\tau\) & the execution time of an operation \\ \hline \(T\) & the number of steps an operation takes \\ \hline \(|t|\) & the number of the terms describing the network topology \\ \hline \(|p|\) & the number of the terms describing the network policy \\ \hline \(|\text{in}|\) and \(|\text{in}|\) & the number of the terms describing network inputs and output respectively \\ \hline \hline PM & Path matrix \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Summary of notations for performance analysis. To complete the initialization phase, the framework needs to query every link then transform the resulting list. The step count of this operation is given by the following formula:  
\[T_{FS}^{PM}\leq e\cdot T_{l}^{PM}+e\cdot h=e\cdot(T_{l}^{PM}+h).\]  
This operation can take a significant amount of time but can be done offline before starting network testing. Since primary and backup paths can also be defined using the same NetKAT network specification, when a failure occurs, there is no need to redo the Path matrix initialization step. As testing the live network progresses with checking a host pair, the framework uncovers the state of the each link (\(d_{\text{PHY}}\) at most) on the path between the two hosts. Consequently, the framework updates the Path matrix with these states. The following formula gives the number of steps required by this operation. As operations in both terms work on lists, the number of steps required by the update operation is dependent on \(d_{\text{PHY}}\), the length of the longest forwarding path in the physical network:  
\[T_{\text{update}}^{\text{PM}}\leq\underbrace{T_{\text{find host pair}}^{\text{PM}}}_{\mathcal{O}(1)}+\sum_{n=1}^{d_{\text{PHY}}}\underbrace{T_{\text{set test result}}}_{\mathcal{O}(1)}=\mathcal{O}(d_{\text{PHY}}).\]  
Reading test cases executes in \(\mathcal{O}(h)\) steps, while reading test summaries needs \(\mathcal{O}(e)\) steps. Verifying if a single link is part of the path takes \(T_{\text{lm}}^{\text{PM}}=\mathcal{O}(d)\) steps, as this search covers paths given by the network specification. Path matrix read and write operations can be shortened when the construct is implemented as two hash tables.