Empirical Evaluation of: A Calculus for Modular Loop Acceleration (and Non-Termination Proofs)

This is the empirical evaluation of the papers A Calculus for Modular Loop Acceleration and A Calculus for Modular Loop Acceleration and Non-Termination Proofs. You can find the source code for our tool LoAT at GitHub.

Moreover, we refer to the general LoAT website for further information.

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 the source code of the version that was used for our evaluation is 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.

Detailed Results

Below we provide tables with the detailed results of our benchmarks:

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

Here, the updates to the variables x_1, ..., x_d are simultaneous: For example, if we have assignments x_1 := x_1 + 1 and x_2 := x_1, the new value of x_2 will be the value that x_1 had before the assignment x_1 := x_1 + 1 in the current loop iteration.

A Calculus for Modular Loop Acceleration and Non-Termination Proofs

For our evaluation of our novel calculus for loop acceleration, see above. In the following, we provide information about the evaluation of our novel calculus for proving non-termination.

Downloading LoAT

We provide a pre-compiled binary of LoAT (Linux, 64 bit). Apart from that, LoAT is open-source and the source code of the version that was used for our evaluation is available on Github.

Examples

The examples that could not be solved by any tool in our evaluation are:

Evaluation

Versions of Other Tools

Invoking the Tools

Below we show how to invoke the different tools and configurations that we evaluated.

Detailed Results

Below we provide tables with the detailed results of our benchmarks: