Deterministic concurrency synthesis

Installing the DPS tool from source:

  • You need Ubuntu (12.04) to use the DPS tool. Download it from here and follow the instructions below.
  • Extract the archive. Go to directory dps/bench and execute ./build.sh there. This compiles the testing benchmarks.
  • Go to the dps directory. Edit build.sh as follows:
    • 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).
  • Finally, run ./build.sh and wait a few minutes.
  • The output files are out_JGF*.txt

Virtual Machine with DPS preinstalled.

  • If you want to directly download a VM image for VirtualBox with DPS in it, go here.