Cantor meets Scott:
Semantic Foundations for Probabilistic Networks

Virtual Machine (recommended):

1. Download one of the VM images mentioned above.
2. Start VirtualBox on your host machine.
3. Import ProbNetKAT VM by selecting "File" -> "Import Appliance", and selecting the downloaded VM image.
4. Allocate the VM as much RAM as possible (at least 2GB). A single processor should suffice (recommended: 2).
5. You may need to turn on virtualization extensions in your BIOS to enable 64-bit virtualization.
6. When the VM starts up, the probnetkat user should be automatically logged in. (username: probnetkat, password: probnetkat).
7. Open a terminal and follow ~/README.md for instructions.

Source code

• lib/Frenetic_ProbNetKAT_Interpreter.ml: Implements ProbNetKAT's denotational semantics.
• lib/Frenetic_ProbNetKAT_TE.ml: A traffic engineering framework to translate topology, traffic matrices and routing schemes into ProbNetKAT programs. It also has ProbNetKAT queries to compute certain statistics.
• lib/Frenetic_ProbNetKAT_Routing.ml, lib/Routing_Frt.ml, lib/Routing_Mw.ml, lib/Routing_Raecke, lib/Routing_Rrt.ml, lib/Routing_Types.ml: Implement routing algorithms and other helper functions for traffic engineering.

Replicating results

Running experiments

1. We will run the traffic engineering experiments on 4-cycle and Abilene topologies. The input topologies (4cycle.dot and abilene.dot) and traffic matrices (4cycle.dem and abilene.dem) are in frenetic/examples directory.
2. The commands to run the experiments are in a bash script:

   cd ~/frenetic
   sh ./run_popl_experiments.sh 

	#!/bin/bash
	iter=6
	echo "NOTE: Running each iteration for ${iter} iterations."
	echo "Set it to 13 to replicate plots from paper. (Slower)"
	echo "Press any key to continue..."
	read tmp
	echo "Running experiment for.."
	echo "Fig 1(b). 4cycle topology"
	./Frenetic_ProbNetKAT_TE.native 4cycle -ecmp -spf -out 4cycle_intro -iter ${iter}
	echo "Fig 1(c). 4cycle topology with link failure"
	./Frenetic_ProbNetKAT_TE.native 4cycle -ecmp -spf -break-a 1 -break-b 2 -out 4cycle_intro_break_1_2 -iter ${iter}
	echo "Fig 5(c,d,g). Abilene topology"
	./Frenetic_ProbNetKAT_TE.native abilene -ecmp -ksp -multi -raeke -out abilene -iter ${iter}
	echo "Fig 5(e,f). Abilene topology with faulty links"
	./Frenetic_ProbNetKAT_TE.native abilene -lfp 0.1 -ecmp -ksp -multi -raeke -out abilene_fail_0.1 -iter ${iter}
	echo "Fig 5(h). Random walk on 4-cycle topology"
	./Frenetic_ProbNetKAT_TE.native 4cycle -ecmp -rw -out 4cycle_loop -iter ${iter}

view raw run_popl_experiments.sh hosted with ❤ by GitHub
3. It may take up to 10 minutes to complete the experiments.
4. Note that the script runs experiments with less iterations (for testing quickly) than those shown in the paper. You may change the number of iterations (variable iter) in the script to match those shown in the paper, but it will need longer time to run and more RAM.
5. If you get an out of memory error, you can either re-run the experiments after allocating more RAM, or decreasing the number of iterations.
6. The VMs also contain the original data and plots from the paper in ~/paper_data/.

Visualizing results

1. Once the above experiments are done, the results can be visualized using the scripts in ~/frenetic/plot/:

   cd ~/frenetic/plot
   sh ./regenerate_plots.sh 

2. The graphs will be generated in corresponding directories in ~/frenetic/data/
3. Figures corresponding to those in paper:
   1. Figure 1(b) : evince ~/frenetic/data/4cycle_intro/Max\ Congestion-line.pdf
   2. Figure 1(c) : evince ~/frenetic/data/4cycle_intro_break_1_2/Throughput-bar.pdf
   3. Figure 5(b) : evince ~/frenetic/plot/heatmap.pdf
   4. Figure 5(c) : evince ~/frenetic/data/abilene/Max\ Congestion-line.pdf
   5. Figure 5(d) : evince ~/frenetic/data/abilene/Throughput-line.pdf
   6. Figure 5(e) : evince ~/frenetic/data/abilene_fail_0.1/Max\ Congestion-line.pdf
   7. Figure 5(f) : evince ~/frenetic/data/abilene_fail_0.1/Throughput-line.pdf
   8. Figure 5(g) : evince ~/frenetic/data/abilene/Mean\ Latency-line.pdf
   9. Figure 5(h) : evince ~/frenetic/data/4cycle_loop/Throughput-line.pdf