sl_modelcheck
sl_modelcheck
is a model checker for SL with arbitrary inductive predicates.
The tool and the theory behind it is described in the [POPL16] paper.
Compiling
If you are simply looking for the latest version of sl_modelcheck
, have a look at Installation.
If you want to try out the original version underpinning the [POPL16] paper, then you can download an archive including x86_64 binaries and the original benchmark suite at the POPL16 GitHub release.
Running
sl_modelcheck.native
will print out instructions for use.
Our tool also includes a script that may be used to harvest models from programs
at runtime using the Archer extension that enables python scripting of GDB. Our
harvester script harvest_heap.py
may be found in the utils/
and
utils/gdb_harvester subdirectories
.
Running the script without options will produce some help text explaining its usage. The script expects as its first argument the path to an executable file from which models are to harvested. It then expects subsequent argument triples which are to consist of:
- a breakpoint description;
- a comma-separated list of variables from which to start walking the heap;
- a path where the files containing the harvested models are to saved.
Benchmarks in [POPL16]
The benchmarks/slmc/
subdirectory contains all the necessary resources for running the benchmarks
described in the [POPL16]. Below this, there are two further sub-
directories. The models/
subdirectory contains *.mdl
files, each of which
describes a model which can be parsed by the model checker. The programs/
sub-
directory contains the source code of the 7 test programs from which models
were harvested at runtime, along with binary versions of these programs,
compiled using gcc 4.2.2 on Ubuntu Linux 12.04LTS. These programs have been
taken from the test suite of the Verifast tool; they have been modified slightly
in order to successfully compile them and for our tool to be able to harvest
an appropriate selection of runtime models.
This directory contains three types of files:
- *.defs
- these contain inductive predicate definitions against which our tool checks the models harvested from the appropriate program.
- *.tst
- these files contains descriptors for the benchmark tests to be run;
the descriptors consist of a filename prefix for selecting
appropriate
*.mdl
files, and a separation logic assertion (formula) against which to test the models. - *.bps
- these files contain descriptors that specify how to harvest runtime models from the test programs. For details of the harvesting tool, see below.
Within this directory, running the make command with the various targets discussed below will execute the tests referred to in the paper. In the following, {TEST} will stand for one of the tokens in the set { aplas-stack, composite, iter, lcset, queue, schorr-waite }
- [make quick-tests]
- will run a small subset of the tests in the benchmark suite as a quick representative demonstration of the tool, and display the results (with info of running times) to standard output.
- [make {TEST}-tests]
- will run all the benchmark tests associated with the {TEST} program and display the results (with info of running times) to standard output.
- [make {TEST}-ptime-tests]
- will run the benchmark tests associated with the {TEST} programs that fall within the PTIME fragment, using the PTIME algorithm and display the results (with info of running times) to standard output. The targets [composite-ptime-tests] and [lcset-ptime-tests] are not defined, since none of the benchmark tests for these programs fall within the PTIME fragment.
- [make spatial-true-tests]
- will model check a substantial selection of the
models against encodings of the spatial truth constant
T
, which every model satisfies. The results (with info of running times) are displayed to standard output. - [make binary-counter-tests]
- will run the model checker against predicate definitions encoding 1-bit, 2-bit and 3-bit binary counters, which fall within the EXPTIME-complete general fragment. The results (with info of running times) are displayed to standard output.
- [make all-tests]
- will call each of the {TEST}-tests, spatial-true-tests and binary-counter-tests targets in turn.
- [make all-ptime-tests]
- will call each of the (defined) ptime test targets in turn.
- [make {Target}-stats]
- will call the appropriate [{Target}-tests] target (as
described above) and pipe the output through a script that extracts the
running time statics for each benchmark test and saves it in a .csv file in
the
stats/
subdirectory. The statistics for each set of tests described by one of the*.tst
files (see above) is saved in a correspondingly named.csv
file, which also contains a timestamp; thus tests may be run multiple times and the running time statistics easily collected for each run individually.
N.B. Running the entire set of benchmark tests (e.g. using the [all-tests] target) will take a long time. The [spatial-true-tests] are the longest single set of benchmark tests, followed by [lcset-tests] and [schorr-waite-tests]
Runtime harvesting of models
The makefile in this directory contains targets for running the harvester tool on the benchmark suite test programs.
- [make {TEST}-models]
- will run the model harvester over the {TEST} program using
the descriptors found in the appropriate
*.bps
files. The resulting.mdl
files will be placed in themodels/
subdirectory. The script does not overwrite any.mdl
files it finds, but where files with the same filename prefix exist it will instead append a new numerical suffix to the newly generated files.
Note that when running the tests using the makefile [*-tests] targets the
tests specified by the .tst
configuration files will be run over ALL the
.mdl
files in the models/
subdirectory. Therefore running the tests AFTER
generating model files will cause the tests to be run over these new models
as well.
- [make clean-{TEST}]
- will remove all of the model files within the
models/
sub- directory whose filenames are prefixed with {TEST}.
N.B. Running the model-harvesting targets, i.e. [make {TEST}-stats] with {TEST}
in { aplas-stack, composite, iter, schorr-waite }, should result in the same set
of model files each time, since these are deterministic programs. However the
lcset and queue programs are concurrent and so running the model-harvesting
target for these programs will, in general, produce different sets of model
files each time. The Cyclist source tree contains the set of .mdl
files that
were used to produce the benchmark results in [POPL16].