Experiments for "Automata Theoretic Approach to Verification of MPLS Networks under Link Failures"

<strong>Prerequisites:</strong> A 2020 linux distribution on an x86_64 platform python3 installation with os, sys, json and statistics packages installed for computation of timing statistics pdflatex for visualization of reachability matrices <strong>Contents:</strong> The <em>bin</em> folder contains the pre-compiled binaries for our tool and the backend verifier for pushdown-systems, <em>moped.</em> The <em>sources</em> folder contains a snapshot of source-code used for producing the tool binary, namely AalWiNes, also found at https://github.com/DEIS-Tools/AalWiNes in release v0.92.J (337f1e4c44f8bce2060897b88e706f7ceca38319) PDAAAL, used for pushdown-system manipulation, also found at https://github.com/DEIS-Tools/PDAAAL in release v0.2.2.J (ed1e7fbb4cacd6ffb240a514cfe8472f83d91f60) The <em>nested</em> folder contains scripts and models for reproducing the results of Table IV The <em>nn-net</em> folder contains scripts and models for constructing reachability-matrices (Table V to Table XII) and operator specific queries Within the <em>nn-net</em> folder, you also find a mapping from alphabetical naming of NORDUnet routers in the paper to numericals <em>(nn-net/index-alpha-map.txt)</em> <strong>P-Rex vs HSA (Table IV)</strong> We here re-use the HSA-timings computed in https://doi.org/10.1145/3281411.3281432 The timings for our tool can be obtained by the following commands <pre><code class="language-bash">cd nested ./compute_nested.sh | grep "#"</code></pre> which should compute a sequence of lines in the terminal equal to <pre><code class="language-bash">### Running N0 with aalwines ### Memory: 27064 Kb Time 0.02 seconds ### Running N1 with aalwines ### Memory: 37404 Kb Time 0.03 seconds ### Running N2 with aalwines ### Memory: 47704 Kb Time 0.03 seconds ### Running N3 with aalwines ### Memory: 57784 Kb Time 0.04 seconds ### Running N4 with aalwines ### Memory: 68368 Kb Time 0.04 seconds ### Running N5 with aalwines ### Memory: 78468 Kb Time 0.05 seconds ### Running N6 with aalwines ### Memory: 88980 Kb Time 0.06 seconds </code></pre> <strong>Operator Queries</strong> The experiments on the queries of the operators can be computed via the commands <pre><code class="language-bash">cd nn-net ./compute_operator.sh </code></pre> which should complete less than 10 minutes. The traces and timings are outputted directly to the terminal. <strong>Reachability Matrices (Table V to Table XII)</strong> This package folder comes pre-populated with the raw computation results. Notice that the <em>compute_grid.sh</em> command will invalidate these results. To compute the full set of reachability tables, you can use the following commands <pre><code class="language-bash">cd nn-net ./make_queries.sh ./compute_grid.sh</code></pre> Notice, however, that this computation in total takes more than two days to complete on a single core. To reduce the size of the experiment, clear the contents of the <em>query</em> sub-folder an modify the <em>make_queries.sh</em> file by commenting out unwanted queries and parameter-combinations. To obtain a matrix, the command <pre><code class="language-bash">./make_grid.sh aalwines IP IP 0 &gt; ip_ip.tex pdflatex ip_ip.tex</code></pre> which generated the IP IP matrix with 0 failures.<br> For the second argument, the following values are supported <em>IP, MPLS</em> while the third argument can also attain the value of <em>ANY</em>. The fourth argument gives the number of link failures. Timing information for the reachability-matrices can be obtained by <pre><code class="language-bash">python3 ./timing_stats.py aalwines 3 IP_IP_UNDER_0</code></pre> where the third argument determines the reduction-type used, and the fourth argument gives the specific query and engine mode used. In the given example we attain the statistics for reduction-mode 3 for the IP-IP matrix using under-approximation on zero link-failures. The <em>pre-reduction</em> and <em>post-reduction</em> elements of the output give the size of the constructed pushdown system before (and after) reduction respectively.