70
F. Frohn
We also considered versions of Theorems 11 and 13 where the inequations in
(3) resp. (4) are strict, but this did not lead to an improvement in our experiments.
Moreover, we experimented with a variant of Thm. 13 that splits the loop under
consideration into two consecutive loops, accelerates them independently, and
composes the results. While such an approach can accelerate loops like ψ ev-inc
exactly, the impact on our experimental results was minimal. Thus, we postpone
an in-depth investigation of this idea to future work.
7 Related Work
Acceleration-like techniques are also used in over-approximating settings (see,
e.g., [10, 20, 21, 25, 26, 29, 32, 33]), whereas we consider exact and under-approximating loop acceleration techniques. As many related approaches have already
been discussed in Sec. 3, we only mention two more techniques here.
First, [4, 7] presents an exact acceleration technique for finite monoid affine
transformations (FMATs), i.e., loops with linear arithmetic whose body is of
the form x ← Ax + b where {A
i
| i ∈ N} is finite. For such loops, PresburgerArithmetic is sufficient to construct an equivalent formula ψ, i.e., it can be
expressed in a decidable logic. In general, this is clearly not the case for the
techniques presented in the current paper (which may even synthesize nonpolynomial closed forms, see T exp ). As a consequence and in contrast to our
technique, this approach cannot handle loops where the values of variables grow
super-linearly (i.e., it cannot handle examples like T 2-invs ). Implementations
are available in the tools FAST [2] and Flata [24]. Further theoretical results
on linear transformations whose n-fold closure is definable in (extensions of)
Presburger-Arithmetic can be found in [5].
Second, [6] shows that octagonal relations can be accelerated exactly and
in [27], it is proven that such relations can even be accelerated in polynomial
time. This generalizes earlier results for difference bound constraints [9]. As
in the case of FMATs, the resulting formula can be expressed in PresburgerArithmetic. Octagonal relations are defined by a finite conjunction ξ of inequations
of the form ±x ± y ≤ c, x, y ∈ x ∪ x
, c ∈ Z. Then ξ induces the relation
x −→ ξ x
⇐⇒ ξ(x, x
). So in contrast to the loops considered in the current
paper where x
is uniquely determined by x, octagonal relations can represent
non-deterministic programs. Therefore and due to the restricted form of octagonal
relations, the work from [6, 27] is orthogonal to ours.
8 Implementation and Experiments
We prototypically implemented our approach in our open-source Loop Acceleration Tool LoAT [11, 16, 17]:
https://github.com/aprove-developers/LoAT/tree/tacas20
It uses Z3 [30] to check implications and PURRS [1] to compute closed forms.
F. Frohn
We also considered versions of Theorems 11 and 13 where the inequations in
(3) resp. (4) are strict, but this did not lead to an improvement in our experiments.
Moreover, we experimented with a variant of Thm. 13 that splits the loop under
consideration into two consecutive loops, accelerates them independently, and
composes the results. While such an approach can accelerate loops like ψ ev-inc
exactly, the impact on our experimental results was minimal. Thus, we postpone
an in-depth investigation of this idea to future work.
7 Related Work
Acceleration-like techniques are also used in over-approximating settings (see,
e.g., [10, 20, 21, 25, 26, 29, 32, 33]), whereas we consider exact and under-approximating loop acceleration techniques. As many related approaches have already
been discussed in Sec. 3, we only mention two more techniques here.
First, [4, 7] presents an exact acceleration technique for finite monoid affine
transformations (FMATs), i.e., loops with linear arithmetic whose body is of
the form x ← Ax + b where {A
i
| i ∈ N} is finite. For such loops, PresburgerArithmetic is sufficient to construct an equivalent formula ψ, i.e., it can be
expressed in a decidable logic. In general, this is clearly not the case for the
techniques presented in the current paper (which may even synthesize nonpolynomial closed forms, see T exp ). As a consequence and in contrast to our
technique, this approach cannot handle loops where the values of variables grow
super-linearly (i.e., it cannot handle examples like T 2-invs ). Implementations
are available in the tools FAST [2] and Flata [24]. Further theoretical results
on linear transformations whose n-fold closure is definable in (extensions of)
Presburger-Arithmetic can be found in [5].
Second, [6] shows that octagonal relations can be accelerated exactly and
in [27], it is proven that such relations can even be accelerated in polynomial
time. This generalizes earlier results for difference bound constraints [9]. As
in the case of FMATs, the resulting formula can be expressed in PresburgerArithmetic. Octagonal relations are defined by a finite conjunction ξ of inequations
of the form ±x ± y ≤ c, x, y ∈ x ∪ x
, c ∈ Z. Then ξ induces the relation
x −→ ξ x
⇐⇒ ξ(x, x
). So in contrast to the loops considered in the current
paper where x
is uniquely determined by x, octagonal relations can represent
non-deterministic programs. Therefore and due to the restricted form of octagonal
relations, the work from [6, 27] is orthogonal to ours.
8 Implementation and Experiments
We prototypically implemented our approach in our open-source Loop Acceleration Tool LoAT [11, 16, 17]:
https://github.com/aprove-developers/LoAT/tree/tacas20
It uses Z3 [30] to check implications and PURRS [1] to compute closed forms.