Models and Tools for Sequential Consistency Violation Checking

Files

All models, together with scripts and tools to perform sequential consistency violation checking, are available here.

Sequential consistency checking with SEQCON-ANALYSER

To use SEQCON-ANALYSER, first, a state space needs to be generated for a given SLCO model.

Producing mCRL2 models and state spaces

To set up the sequential consistency violation checker, Python 3 is required, together with the packages TextX and Jinja2. We suggest to use a Linux installation, but it should be possible to set up everything for Windows as well. With this setup, it is possible to convert an SLCO model example.slco (for instance from the experiments folder) to an mCRL2 model using the slco2mcrl2-seqcon.py script (in the folder python-textx-jinja2), as follows:

python3 slco2mcrl2-seqcon.py example.slco

Once an mCRL2 model has been produced, its state space can be generated. For this, a version of the mCRL2 toolset has to be installed, which can be obtained from here. For faster state space generation, make sure to configure the compilation of the toolset with the experimental tools enabled.

Basic state space generation

The easiest, but not necessarily the fastest, way to generate the state space of a model, is by first linearising the model:

mcrl22lps example.mcrl2 example.lps

And then generating the state space in the ".aut" format:

lps2lts example.lps example.aut

Faster state space generation

Faster state space generation, as reported in the paper, can be performed by first preprocessing the model in the linearisation phase. For this, there are scripts available in the bin folder of the package. Open the model and look for Sort data structures with a name of the form "Int" followed by a number. If there are no such structures, run the following:

lps-simplify example.mcrl2

If there is one such structure, say "Int2", run:

lps-simplify-unfold example.mcrl2 Int2

If there are multiple such structures, there are scripts "lps-simplify-unfold2" and "lps-simplify-unfold3" to unfold multiple structures in one run. When such a script is called, the structures need to be listed after the model name, for instance:

lps-simplify-unfold2 example.mcrl2 Int2 Int4

After linearisation, there will now be a file named tmp.lps in the current folder. This LPS can be used to generate a state space as mentioned above under "Basic state space generation".

Checking sequential consistency

Once a state space has been generated, the SEQCON-ANALYSER tool can be used for postprocessing. Once it has been compiled (run make in the C++ folder), it can be executed as follows:

seqcon-analyser example.aut -w MEMMODEL

with MEMMODEL being either TSO, PSO, or ARM. By default, it is set to TSO. Another optional argument is -a, which selects atomicity checking. The tool will report the number of fences (and the number of locks, in case of atomicity checking) that is needed to make the behaviour of the program SC-serialisable. Furthermore, it will report the time needed to perform the analysis, minus the time for reading the state space from disk.

Sequential consistency checking with MUSKETEER

The tool, together with instructions on how to compile it and use it, can be found here. In the experiments folder, in each subfolder, suitable C files can be found, which can be analysed with MUSKETEER. First, make sure to convert a file to a goto-program, as explained on the MUSKETEER page. For the experiments, we used the time command to measure runtimes. Make sure to use the --no-loop-duplication option when analysing the Anderson cases. Otherwise, the results will be wrong.

Sequential consistency checking with REMMEX

The REMMEX tool is included in the package, and scripts are available in the bin folder to ease launching the tool. Make sure Java is installed. In the experiments folder, suitable ".txt" files are available as input for the REMMEX tool. To run sequential consistency checking, REMMEX requires that an error state is defined. For each model example.txt, a suitable error state is given in the file example.txt.cfg (except for the Elevator2 models, see the paper). The tool can then be launched as follows:

remmex-check example.txt MEMMODEL "CFG FILE CONTENTS"

Make sure to give the contents of the CFG file between quotes. MEMMODEL can be either PSO or TSO. The remmex-check script will report the time needed for the analysis, and the number of fences placed.