This file documents how to use Effpi to replicate the claims in the following paper:
Building and testing Effpi requires many dependencies, listed here (but we also provide a preconfigured virtual machine: see below).
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:
From the root directory of the Effpi source code, try:
sbt ";plugin/assembly;examples/compile"
The expected outcome is:
sbt will download all its project dependencies (not listed above), including the Dotty compiler and runtime. This might take some time, depending on your Internet connection speed;
then, it will try to compile some examples, also leveraging the mCRL2 model checker;
you should not see any error, but
you should see some warnings, like "the property does not hold" and "match may not be exhaustive": this is OK.
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:
you should see some messages describing three philosophers trying to have dinner, while sharing three forks;
after a while, the philosophers should deadlock;
then, after 30 seconds, the program will timeout, throwing an exception.
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.
Here we show how to reproduce Figures 8 and 9 in the PLDI'19 paper.
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
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.
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:
the reduced benchmarks do not include the number of states (replaced by "∞") because, to compute it, mCRL2 might require a lot of RAM (often too much for a virtual machine). If you want to include the number of states:
build.sbt with an editor;pluginOpts, replace the last
argument false with true (for
details, see the comments before the definition
of pluginOpts);sbt "pluginBenchmarks/compile" (as
above);the reduced benchmarks do not include the two longest cases (variants of Ring, 15 elements). To enable them:
plugin-benchmarks/src/main/scala/,
rename the files with extension .scala-disabled
into .scalasbt "pluginBenchmarks/compile" (as
above);the reduced benchmarks only perform 2 repetitions, instead of 10. To enable and perform 10 repetitions:
build.sbt with an editor;pluginOpts, replace the
argument Some(2) with None (for
details, see the comments before the definition
of pluginOpts);sbt "pluginBenchmarks/compile" (as
above).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