ABSTRACT REPRESENTATION FOR CONTROL PLANES (ARC)
- Batfish (http://www.batfish.org): a git repository forked from the
Batfish code repository is included as a submodule of this git repository;
run `git submodule update --init` to clone the forked Batfish code repository
into the `libs/batfish` directory
- graphviz: only required for rendering graphs output by ARC
- Gurobi (version 6.5 or newer): only required for equivalence testing;
academic users can obtain a free single-user license
- Java JDK (version 8 or newer)
1. Clone the ARC git repository
git clone https://bitbucket.org/uw-madison-networking-research/arc.git
2. Obtain the Batifish source code
git submodule update --init
3. (Optional) Copy or symlink the `gurobi.jar` file from the lib directory of your Gurobi installation to the `projects/arc/lib` directory
The compiled program is loated in the `target/` directory (within `projects/arc/`); all requisite libraries are copied into a `lib/` subdirectory within the `target/` directory.
Create a directory containing a snapshot of the configurations from all routers in the network whose control plane you want to analyze. Example configurations for toy networks are included in the configs/examples directory. ARC currently only supports configurations from Cisco devices.
Run ARC (from the `projects/arc/target` directory) using the following command:
java -cp *:lib/* edu.wisc.cs.arc.Driver -configs <CONFIGS-DIR>
`CONFIGS-DIR` is the path to a directory containing the configuration files for all devices in the network whose ARC should be generated/analyzed.
To produce visual representations of the ETGs contained in an network's ARC, as well as the network's routing instances and (inferred) physical topology, include the `-graphs <GRAPH-DIR>` option. With this option, ARC will output graph files that be rendered using graphviz. You can use the following command to render all graphs produced by ARC:
To only render the base ETG (i.e., an ETG from which per-traffic-class ETGs are derived), instance graph, and physical topology graph, include the `-b` argument before the GRAPH-DIR when running the script.
To verify a particular invariant, include the appropriate `-v` argument (e.g., `-vab` to verify always blocked) when running ARC. To run all verifiers, include the `-vall` argument.
To see all options for ARC, use the `-help` argument:
java -cp *:lib/* edu.wisc.cs.arc.Driver -help
The `projects/arc/scripts/` directory contains a variety of scripts that can aid in running ARC over many networks and parsing ARC's output.
Generating FAT Tree Topology
2. Run FAT Tree generation code (from the `projects/fattree/target` directory) using the following command:
java -cp *:lib/* CreateFATTreeTopology -help
The `-help` argument shows all options for creating FAT Tree topology.