Cantor meets Scott:
Semantic Foundations for Probabilistic Networks

Downloads

Experimental Platform

We used a Dell R620 server (2x Intel Xeon E5-2650 v2 processors, 64GB RAM) running Ubuntu 14.04.1 (x86_64).

Installation

There are two options for installing and testing ProbNetKAT:

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.

From source:

  1. Install OCaml and OPAM:
    2. sudo apt-get install ocaml opam m4 build-essential pkg-config python-pip
sudo pip install matplotlib
  2. Configure OPAM:
    3. opam init -y
opam switch 4.02.3
eval `opam config env`
  3. Install dependencies:
    4. opam pin add ocamlgraph 1.8.6
opam install core async oasis cstruct tcpip
  4. Checkout code
    5. git clone -b probnetkat https://github.com/frenetic-lang/frenetic
  5. Build
    6. cd frenetic
oasis setup
make

Source code

The source code is available on GitHub in probnetkat branch of Frenetic. The relevant files are:
  • 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
  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