Effpi: Instructions

This file documents how to use Effpi to replicate the claims in the following paper:

Getting Started

Software Dependencies

Building and testing Effpi requires many dependencies, listed here (but we also provide a preconfigured virtual machine: see below).

Virtual Machine

We have prepared a preconfigured virtual machine, based on a minimal Ubuntu installation, plus all software dependencies above (and more):

The download size is around 1.9 GB; once imported on VirtualBox, the virtual machine should use around 10 GB of disk space.

NOTE: the virtual machine does not contain the Effpi source code. After launching the VM, you will need to clone the following Git repository:

Kick-the-Tires

From the root directory of the Effpi source code, try:

sbt ";plugin/assembly;examples/compile"

The expected outcome is:

If the above works, then you can quickly try the runtime, by executing:

sbt "examples/runMain effpi.examples.diningphilo.Main"

This is a deadlocking implementation of Dijkstra's dining philosophers problem. The expected outcome is:

Step-by-Step Instructions

Here we provide the basic instructions for replicating the main measurements and claims in the PLDI'19 paper. Then, we provide pointers for further exploration.

Replicating the Main Measurements

Here we show how to reproduce Figures 8 and 9 in the PLDI'19 paper.

Reproducing Figure 8 (Runtime Benchmarks)

Figure 8 supports the claim that, although Effpi is a research prototype, its peformance appears viable, when compared with Akka.

First, you need to invoke a setup script (this is only needed before running the benchmarks for the first time):

./scripts/setup-runtime-benchmarks.sh

The script above will download some more dependencies, and set up an SQLite database (in a file callsed benchmarks.db), that will contain the benchmarking results.

Then, you can build and execute the benchmarks, by running (note the optional parameter N):

./scripts/exec-runtime-benchmarks.sh [N]

Above, the optional parameter N is the number of repetitions. The default is 1: it takes around 3.5 hours on the virtual machine, running on an Intel i7@2.40GHz with 4 GB of RAM.

For a full benchmark, you can run ./scripts/exec-runtime-benchmarks.sh 10 (where 10 is the number of repetitions used for Figure 8 in the paper; note that it would likely take over 20 hours on the VM).

NOTE: depending on the amount of available RAM in your system, some benchmarks might crash, due to out-of-memory errors. This is expected, and the benchmarking scripts handle such cases gracefully.

Finally, you can create plots like the ones in Figure 8, by running:

./scripts/plot-runtime-benchmarks.sh

You should be able to see the plots for execution time and memory under the directories scripts/graphs/time and scripts/graphs/memory, respectively. You can browse them by invoking:

thunar scripts/graphs/time
thunar scripts/graphs/memory

Reproducing Figure 9 (Verification Benchmarks)

Figure 9 measures the verification of protocols with many interacting components, and a rather large number of states. The claim is that, by such numbers, "our model checking approach appears viable: it can provide (quasi)real-time verification results, suitable for interactive error reporting on an IDE".

There is an easy way to perform a reduced version of the verification benchmarks (taking around 30 minutes on an Intel i7@3.60GHz):

sbt "pluginBenchmarks/compile"
./scripts/collectPluginBenchmarks > plugin-benchmarks.csv

If you want to reproduce the full verification benchmarks, see below.

To view the resulting plugin-benchmarks.csv file, you can e.g. copy&paste it in http://convertcsv.com/csv-to-html.htm.

Performing Full Verification Benchmarks

The command above produces a reduced version of the verification benchmarks. The full benchmarks take around 20 hours on an Intel i7@3.60GHz with 16GB of RAM. The differences are:

Further Exploration

The Effpi documentation contains more information: its overall architecture, and various examples (including those in the paper).

To generate and browse the documentation, you can execute (from the root of the Effpi source code):

cd docs
make html
firefox _build/html/index.html