Parsynt is an automatic parallelizer - but it's not a compiler. Using on program synthesis, it produces parallel divide-and-conquer implementations of loops in a C input program. It uses TBB as a target framework for the implementation and provides, if possible, a proof of functional equivalence to the input code in Dafny. In the background, it relies on the syntax-guided synthesis solver Rosette to find a suitable join function.

Get the source archive here and execute the setup.sh script in the root folder. We are working on packaging the application in a more suitable format.
The script relies on the aptitude package manager. We have tested the installation on Ubuntu 16.04 and 14.04. For other OSes and OSes without the aptitude package manager, you should install the requirements yourself. For more instructions visit the GitHub repository.

REMARK : we use Ocaml's OPAM package manager, so you should have the environment variables correctly set if you have already installed it. Otherwise, you will be asked during the installation of OPAM is you want it to write into your .profile. We assume the environment has access to OPAM's binaries.

When setup.sh succeeds, you have a link to an executable in the base folder. Try the tool on a file example.c.

./Parsynth c_examples/<example_name.c>

The tool will look for all the innermost for loops and try to find a divide-and-conquer parallelization for them. If it succeeds, it will produce a TBB implementation in tbb_examples/<name of the function where the loop appears>.cpp and a proof to be checked by Dafny in dafny_examples/<name of the function where the loop appears>.dfy.

To check the proofs, the user might want to install the Dafny Proof checker.