A Calculus for Modular Loop Acceleration
71
For technical reasons, the closed forms computed by LoAT are valid only if
n > 0, whereas Def. 2 requires them to be valid for all n ∈ N. The reason is that
PURRS has only limited support for initial conditions. In the future, we plan
to use a different recurrence solver to circumvent this problem. Thus, LoAT’s
results are only correct for all n > 1 (instead of all n > 0). Moreover, LoAT can
currently compute closed forms only if the loop body is triangular, meaning that
each a i is an expression over x 1 , . . . , x i . The reason is that PURRS cannot solve
systems of recurrence equations, but only a single recurrence equation at a time.
However, LoAT failed to compute closed forms for just 26 out of 1511 loops in our
experiments, i.e., this appears to be a minor restriction in practice. Furthermore,
conditional acceleration via metering functions has not yet been integrated into
the implementation of our calculus. While LoAT can synthesize formulas with
non-polynomial arithmetic, it cannot yet parse them, i.e., the input is restricted
to polynomials. Finally, LoAT does not yet support disjunctive loop conditions.
Apart from these differences, our implementation closely follows the current
paper. It repeatedly applies the conditional acceleration techniques from Sections 5
and 6 with the following priorities: T hm. 8 > T hm. 7 > T hm. 11 > T hm. 13.
To evaluate our approach, we extracted 1511 loops with conjunctive guards
from the category Termination of Integer Transition Systems of the Termination
Problems Database [35], the benchmark collection which is used at the annual
Termination and Complexity Competition [19], as follows:
1. We parsed all examples with LoAT and extracted each single-path loop with
conjunctive guard (resulting in 3829 benchmarks).
2. We removed duplicates by checking syntactic equality (resulting in 2825
benchmarks).
3. We removed loops whose runtime is trivially constant using an incomplete
check (resulting in 1733 benchmarks).
4. We removed loops which do not admit any terminating runs, i.e., loops where
Thm. 2 applies (resulting in 1511 benchmarks).
We compared our implementation with LoAT’s implementation of acceleration
via monotonicity (Thm. 3, [11]) and its implementation of acceleration via
metering functions (Thm. 4, [17]), which also incorporates the improvements
proposed in [16]. We did not include the techniques from Theorems 1 and 2 in our
evaluation, as they are subsumed by acceleration via monotonicity. Furthermore,
we compared with Flata [24], which implements the techniques to accelerate
FMATs and octagonal relations discussed in Sec. 7. Note that our benchmark
collection contains 16 loops with non-linear arithmetic where Flata is bound to
fail, since it only supports linear arithmetic. We did not compare with FAST [2],
which uses a similar approach as the more recent tool Flata.
All tests have been run on StarExec [34]. The results can be seen in Table 1.
They show that our novel calculus was superior to the competing techniques in
our experiments. In all but 7 cases where our calculus successfully accelerated the
given loop, the resulting formula was polynomial. Thus, integrating our approach
into existing acceleration-based verification techniques should not present major
obstacles w.r.t. automation.
71
For technical reasons, the closed forms computed by LoAT are valid only if
n > 0, whereas Def. 2 requires them to be valid for all n ∈ N. The reason is that
PURRS has only limited support for initial conditions. In the future, we plan
to use a different recurrence solver to circumvent this problem. Thus, LoAT’s
results are only correct for all n > 1 (instead of all n > 0). Moreover, LoAT can
currently compute closed forms only if the loop body is triangular, meaning that
each a i is an expression over x 1 , . . . , x i . The reason is that PURRS cannot solve
systems of recurrence equations, but only a single recurrence equation at a time.
However, LoAT failed to compute closed forms for just 26 out of 1511 loops in our
experiments, i.e., this appears to be a minor restriction in practice. Furthermore,
conditional acceleration via metering functions has not yet been integrated into
the implementation of our calculus. While LoAT can synthesize formulas with
non-polynomial arithmetic, it cannot yet parse them, i.e., the input is restricted
to polynomials. Finally, LoAT does not yet support disjunctive loop conditions.
Apart from these differences, our implementation closely follows the current
paper. It repeatedly applies the conditional acceleration techniques from Sections 5
and 6 with the following priorities: T hm. 8 > T hm. 7 > T hm. 11 > T hm. 13.
To evaluate our approach, we extracted 1511 loops with conjunctive guards
from the category Termination of Integer Transition Systems of the Termination
Problems Database [35], the benchmark collection which is used at the annual
Termination and Complexity Competition [19], as follows:
1. We parsed all examples with LoAT and extracted each single-path loop with
conjunctive guard (resulting in 3829 benchmarks).
2. We removed duplicates by checking syntactic equality (resulting in 2825
benchmarks).
3. We removed loops whose runtime is trivially constant using an incomplete
check (resulting in 1733 benchmarks).
4. We removed loops which do not admit any terminating runs, i.e., loops where
Thm. 2 applies (resulting in 1511 benchmarks).
We compared our implementation with LoAT’s implementation of acceleration
via monotonicity (Thm. 3, [11]) and its implementation of acceleration via
metering functions (Thm. 4, [17]), which also incorporates the improvements
proposed in [16]. We did not include the techniques from Theorems 1 and 2 in our
evaluation, as they are subsumed by acceleration via monotonicity. Furthermore,
we compared with Flata [24], which implements the techniques to accelerate
FMATs and octagonal relations discussed in Sec. 7. Note that our benchmark
collection contains 16 loops with non-linear arithmetic where Flata is bound to
fail, since it only supports linear arithmetic. We did not compare with FAST [2],
which uses a similar approach as the more recent tool Flata.
All tests have been run on StarExec [34]. The results can be seen in Table 1.
They show that our novel calculus was superior to the competing techniques in
our experiments. In all but 7 cases where our calculus successfully accelerated the
given loop, the resulting formula was polynomial. Thus, integrating our approach
into existing acceleration-based verification techniques should not present major
obstacles w.r.t. automation.