Multi-core saturation experiments
This repository hosts the experimental scripts for multi-core saturation.
You can contact the main author of this work at firstname.lastname@example.org.
Information on the experiments are found in the submitted paper.
Compiling the sources
Installing the Debian packages, R packages and compiling the necessary sources is done by running
The script will compile and install Meddly, Sylvan and LTSmin.
Running the compile script ensures that all binaries that are built end up in the
Ultimately the script will run multi-core saturation with the force order on the Petri net running example presented in the paper.
I.e. the commandline that is automatically run is
tools/pnml2lts-sym --saturation=sat -rf pnml/example.pnml.
This means the last few lines that are shown when running
pnml2lts-sym: state space has 5 states, 12 nodes.
When this output is visible the compilation step has been completed successfully.
Reproducing the experiments (simple version)
The following steps use the simple versions of the benchmark scripts for maximal 4 workers.
- First extract the models in the
tar Jxf models.tar.xz.
- For a very simple example, run
./generate.py HouseConstruction-PT-010twice. The first time generates the LDD files from the PNML input files, the second time generates the BDD and MDD files from the LDD input files.
- You can repeatedly run
./generate.py .*mddto generate more input files, if generating a file takes too long, just interrupt and restart, as the order in which the script tries to generate input files is randomized.
./exp-simple.py runto run experiments on the LDD, BDD, MDD files in the
mccdirectory, on 1, 2, 4 cores. This corresponds to the
bdd-satmethods in the paper. The default timeout is 60 seconds so this should not take too long. You can change this in
exp-simple.pyif you want a different timeout.
./exp-simple.py csv > results-simple.csvto get the results in a CSV format.
./analyse-simple.rto produce the tables and Figures for the paper (Figures in the 'tex' files).
Reproducing the experiments (16-core and 48-core versions)
generate.py as the preprocessing step to generate LDD and BDD files from the models.
generate.py can be configured with a timeout value (in the file itself).
generate.py (without parameters) to generate all files, one by one.
generate.py list to get the list of files the script generates.
generate.py todo to get the list of files not yet generated and did not timeout.
generate.py <REGEXP> to generate all files matching the given input.
You can use this to quickly generate files in parallel on a cluster.
generate-slurm.sh does this, use
sbatch -N... -p... generate-slurm.sh.
Each time you run
generate.py without parameters, it will start with a random file to generate.
If you just want to quickly generate some files, just repeatedly run
generate.py and interrupt
with CTRL-C if it takes too long.
exp48.py are configured to run on 16-core machines and 48-core machines respectively.
For a simple small example, you can generate some LDD files with
generate.py and then use
exp-simple.py run to run "simple" experiments.
exp-simple.py cache you can populate a cache file but this is optional.
exp-simple.py report you get a report of the status of all experiments.
exp-simple.py csv you get a CSV file of the results.
The log files of the 16-core machine cluster are in logs-cluster.tar.gz and the log files of the 48-core machine experiments are in logs-48.tar.gz. The generated CSV files are in results.csv (for the 16-core cluster) and results48.csv
To analyse these results we used R and have provided two R scripts
The compile script
compile_sources.sh takes care of installing R and the dependencies for running both R scripts.
The R scripts generate the tables and numbers that we used in the empirical evaluation.
Running a Promela example
To run the Promela example of the GARP protocol run the commandline
tools/prom2lts-sym Promela/garp_1b2a.prm --saturation=sat -rf.
After approximately a minute LTSmin should output
prom2lts-sym: state space has 385000995634 states, 487405 nodes.