Empirical Evaluation of: A Calculus for Modular Loop Acceleration


Artifact Evaluation

Here you can find the zip-file for the artifact evaluation committee.

Downloading LoAT

We provide a pre-compiled binary of LoAT (Linux, 64 bit). Apart from that, LoAT is open-source and available on Github


Examples


Evaluation

StarExec-Jobs

Below we provide links to the StarExec-Jobs of our evaluation.

In the tables on StarExec, the result "YES" means that the loop in question was accelerated exactly, "MAYBE" means that it was accelerated approximately, and "NO" means that the tool failed to accelerate it. By clicking on one of the examples and unfolding "output", you can see the full output of the tool.

LoAT's Output

If the loop was accelerated successfully, then the end of the output looks, e.g., as follows:

0.00/0.12 Start location: start
0.00/0.12 0: start -> f : [], cost: 0
0.00/0.12 2: f -> f : x'=-n+x, x_1'=n+x_1, x_2'=x_3, x_4'=x_5, [ n>0 && 1+x_1>0 && x_3>0 && x_2>0 && 1-n+x>0 && -1+x_4>0 && -1+x_5>0 ], cost: 1
0.00/0.12 EOF

The leading 0.00/0.12 is a timestamp which is added by StarExec and can thus be ignored, just as the trailing EOF. The accelerated loop is presented in a rule-based formalism, which is equivalent to the formulas that are used in the paper. It is always prefixed by c: f -> f where c is a natural number. The remainder of the corresponding line above is equivalent to the formula

x'=-n+x && x_1'=n+x_1 && x_2'=x_3 && x_4'=x_5 && n>0 && 1+x_1>0 && x_3>0 && x_2>0 && 1-n+x>0 && -1+x_4>0 && -1+x_5>0.

The costs are irrelevant for our paper and can thus be ignored.

Flata's Results

The invocation of Flata was suggested by its developers. Note that Flata sometimes failed with one of the following two errors:

This happens when the loop contains non-linear arithmetic, which is not supported by Flata.

Zip-Files with Results

As StarExec might be temporarily unavailable due to updates, we also provide zip-files with the results and the full output of LoAT and Flata.


LoAT's Input Format

LoAT uses the input format of the tool KoAT (file ending .koat). It represents programs as transition systems, using a rule-based formalism. An example for a valid input is:

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS start))
(VAR x y z)
(RULES
  start(x, y, z) -> f(x, y, z)
  f(x, y, z) -> f(x-1, y+x, z-y) [x > 0 && y > 0 && z > 0]
)

The first line is needed for historical reasons and is meaningless in the context of our paper.

The second line declares the entry-point of the program. Note that KoAT's input format requires that each program has a unique entry-point without any incoming transitions (i.e., in the example above, a rule where start occurs on the right-hand side would be invalid).

In the third line, the program variables are declared.

For the purpose of our paper, the RULES-section always contains two rules: One of the form

start(...) -> f(...),

which is needed due to the requirement that the entry-point of the program does not have incoming transitions (see above), and a second rule

f(x_1,...,x_d) -> f(t_1,...,t_d) [phi],

which represents the loop that should be accelerated. More precisely, it represents the following loop:

while (phi)
  x_1 := t_1
  ...
  x_d := t_d