Guide to the implementation accompanying the paper
Our implementation is written in Java and depends on JavaILP and lpsolve. In order to compile the source codes, you will need both JavaILP and lpsolve. However, JavaILP is embedded in the executable jar file, so in order to run the jar file, you just need to install lpsolve first and make sure that it is in the Java CLASSPATH. This is already taken care of in the virtual machine.
Running the implementation
To run the implementation over an input program “input.prog”, simply execute the following command in a terminal:
java -jar main.jar input.prog
It will try to synthesize a linear DSM-map for the outer-most loop of the input program and writes a log of every step of the process.
Note 1: A DSM-map with epsilon=0 corresponds to failure.
Note 2: The command above will only produce a DSM with respect to the outermost loop. If a program consists of several loops, they should be handled separately (see the programs in examples.zip)
Format of the input
The input program should be written according to the syntax grammar provided in the paper. The invariants should be enclosed between two ‘#’ characters and the program should end with the keyword “end”. See the examples.
Reproducing the results
There is a script named “run.sh” on the Desktop of the virtual machine. To obtain all the results reported in the paper, simply double-click it and choose “Run in Terminal”. It will run our algorithm on all benchmarks (which are in the “examples” directory). A new directory named “results” will be created which contains a complete log of every run.
We expect run.sh to take around 1 minute to execute.
Reading the logs
Each log writes a detailed account of every step of our algorithm (following the paper). The most interesting part of a log is its last part, where it outputs the complete DSM as well as the runtime of our analysis. You can verify the results reported in Tables 1 and 2 and Appendix F.2 by simply looking at this part. Note that in the tables we are only reporting eta(1).
Potential Differences with the paper
If you have any difficulty in installing the prerequisites or running the implementation, please contact email@example.com.