Deterministic concurrency synthesis

Virtual Machine with DPS preinstalled.

  • Note: we tested the Virtual Machine, by giving it 14GB of RAM. Make sure your host machine has 16GB or more.
  • Download the virtual machine image from here
  • Untar it and run it in VirtualBox.
  • Login
    • User: dps
    • Password: DPSpassword
  • The tool is in a subdirectory dps of the home directory. Run "cd dps"
  • Run ./build.sh
  • The output files are out_JGF*.txt
    • To see the number of determinizations, you can run "grep models *.txt"
  • Optional: if you want to only run some benchmarks, you can edit build.sh in the dps/ directory.
    • The variable BENCHMARKS contains a list of benchmarks to run on (keep in mind that Crypt requires 12GB of RAM).
    • The variable OPTIONS determines the type of synthesis:
      • tsc_trans2 - this generates the most fine-grained constraints by not requiring an ordering specification, or
      • rw_avoidconflict_tsc_trans2 - this includes the specification where reads go after write on a variable (unless this creates a confict).

If you want to download the source code only, click here