ConSORT: Context- and Flow-Sensitive Ownership Refinement Types

This is the project website for the ConSORT project. It provides the source code for ConSORT, its experiments, and basic instructions for building and running.

Table of Contents

Source Code

The source code for ConSORT is available here.

Building

System Requirements

ConSORT is known to build and run on Linux. It has been successfully built under 32-bit Cygwin on Windows (64-bit Cygwin does not work). Mac remains untested.

Dependencies

At the time of writing, ConSORT requires at least OCaml 4.08 and is known to work with this version. It also depends on the following OCaml packages (known, working OPAM versions show in parentheses):

Additionally, ConSORT uses dune for compilation. Version 1.11.3 is known to work. We also use make as a wrapper to invoke dune.

Compilation

cd into the extracted archive and run make.

Running

Environment

In general, ConSORT requires that the depended upon CHC solvers exist somewhere in your path. Accordingly, ensure that at least one of Z3, HoICE, or Eldarica are available in your path. (The executable used for invoking a solver can be overridden with command line options; see the help output of ConSORT for details.)

Invocation

To run ConSORT, we recommend using the test.sh script available in source directory; this script automatically includes the definitions of arithmetic and boolean primitives when invoking ConSORT. ConSORT can be invoked directly with build/_default/test.exe from the source directory. The basic invocation is:

./test.sh test-program.imp

test-program.imp is the path to some file written in our extended IMP language.

Additional Options

All available command line options are described by passing the -help flag to either test.sh or the underlying executable. The most important flag is likely -timeout, which takes an integer argument which indicates the timeout in seconds for the solver.

Interpreting the Output

After invoking the solver, ConSORT will generally return one of 4 outputs:

Currently ConSORT does not produce explanatory output giving, e.g., concrete counter-examples to safety.

Running the Experiments

Our implementations of the benchmarks mentioned in the paper are available under the benchmarks/ folder. jayhorn/ contains the implementations of the JayHorn benchmarks, and consort/ contains the implementations of our custom benchmark suite.

To run ConSORT on our experiments, run

./test.sh -solver parallel -timeout 60 path/to/prog.imp

Note that using the parallel solver requires Eldarica, HoICE, and Z3 to be installed on your system.

Comparison with JayHorn

Due to licensing concerns, we cannot distribute JayHorn or the benchmarks used in the LPAR ‘17 paper. To perform the full comparison, you will need to download and build the JayHorn tool. The GitHub repository is here. We used revision b933502ae7ee8da469939e8cb45bc3b2f801fc0a in our experiments.

After downloading and building the tool you will need to update the experiment configuration. Set the key jayhorn in config.yml to point to the jayhorn.jar file produced by the JayHorn build.

In addition you will need to download the benchmarks themselves from here. After downloading, update the key jayhorn_bench.jayhorn_imp with the path to the lpar17-benchmarks/jayhorn-benchmark subdirectory within the repository.

Once configuration is complete, the experiments can be run by executing python run_experiments.py results.yml. After completion, results.yml will contain the complete experiment results on all test files.

Acknowledgments: The CSS for this site was written by James Bornholt for the Synapse artifact site and is used with permission.