A Calculus for Modular Loop Acceleration
63
Linear metering functions can be synthesized via Farkas’ Lemma and SMT
solving [17]. However, many loops do not have non-trivial linear metering functions.
To see this, reconsider T non-dec . Here, (x 1 , x 2 ) → x 1 is not a metering function
as T non-dec cannot be iterated at least x 1 times if x 2 ≤ 0. Thus, [16] proposes
a refinement of [17] based on metering functions of the form x → I ξ (x) · f (x)
where ξ ∈ Prop(C (x)) and f is linear. With this improvement, the metering
function (x 1 , x 2 ) → I x2>0 (x 2 ) · x 1 can be used to accelerate T non-dec to
x
1
x
2
=
x1−n
x2+n
∧ x 1 > 0 ∧ x 2 > 0 ∧ n < x 1 + 1.
4 A Calculus for Modular Loop Acceleration
All acceleration techniques presented so far are monolithic: Either they accelerate
a loop successfully or they fail completely. In other words, we cannot combine
several techniques to accelerate a single loop. To this end, we now present a
calculus that repeatedly applies acceleration techniques to simplify an acceleration
problem resulting from a loop T loop until it is solved and hence gives rise to a
suitable ψ ∈ Prop(C (y)) which approximates resp. is equivalent to T loop .
Definition 3 (Acceleration Problem). A tuple
ψ | q
ϕ |
ϕ | a
where ψ ∈ Prop(C (y)), q
ϕ,
ϕ ∈ Prop(C (x)), and a : Z
d
→ Z
d is an acceleration
problem. It is consistent if ψ approximates q
ϕ, a, exact if ψ is equivalent to
q
ϕ, a, and solved if it is consistent and
ϕ ≡ ≡. The canonical acceleration
problem of a loop T loop is
x
= a
n (x) | | | ϕ(x) | a(x) .
Example 1. The canonical acceleration problem of T non-dec is
x
1
x
2
=
x1−n
x2+n
x 1 > 0 ∧ x 2 > 0
x1−1
x2+1
.
The first component ψ of an acceleration problem ψ | q
ϕ |
ϕ | a is the partial
result that has been computed so far. The second component q
ϕ corresponds
to the part of the loop condition that has already been processed successfully.
As our calculus preserves consistency, ψ always approximates q
ϕ, a. The third
component is the part of the loop condition that remains to be processed, i.e., the
loop
ϕ, a still needs to be accelerated. The goal of our calculus is to transform
a canonical into a solved acceleration problem.
More specifically, when we have simplified a canonical acceleration problem
x
= a
n (x) | | | ϕ(x) | a(x) to ψ 1 (y) | q
ϕ(x) |
ϕ(x) | a(x), then ϕ ≡ q
ϕ ∧
ϕ
and
ψ 1 =⇒ x −→
n
q
ϕ,a x
.
63
Linear metering functions can be synthesized via Farkas’ Lemma and SMT
solving [17]. However, many loops do not have non-trivial linear metering functions.
To see this, reconsider T non-dec . Here, (x 1 , x 2 ) → x 1 is not a metering function
as T non-dec cannot be iterated at least x 1 times if x 2 ≤ 0. Thus, [16] proposes
a refinement of [17] based on metering functions of the form x → I ξ (x) · f (x)
where ξ ∈ Prop(C (x)) and f is linear. With this improvement, the metering
function (x 1 , x 2 ) → I x2>0 (x 2 ) · x 1 can be used to accelerate T non-dec to
x
1
x
2
=
x1−n
x2+n
∧ x 1 > 0 ∧ x 2 > 0 ∧ n < x 1 + 1.
4 A Calculus for Modular Loop Acceleration
All acceleration techniques presented so far are monolithic: Either they accelerate
a loop successfully or they fail completely. In other words, we cannot combine
several techniques to accelerate a single loop. To this end, we now present a
calculus that repeatedly applies acceleration techniques to simplify an acceleration
problem resulting from a loop T loop until it is solved and hence gives rise to a
suitable ψ ∈ Prop(C (y)) which approximates resp. is equivalent to T loop .
Definition 3 (Acceleration Problem). A tuple
ψ | q
ϕ |
ϕ | a
where ψ ∈ Prop(C (y)), q
ϕ,
ϕ ∈ Prop(C (x)), and a : Z
d
→ Z
d is an acceleration
problem. It is consistent if ψ approximates q
ϕ, a, exact if ψ is equivalent to
q
ϕ, a, and solved if it is consistent and
ϕ ≡ ≡. The canonical acceleration
problem of a loop T loop is
x
= a
n (x) | | | ϕ(x) | a(x) .
Example 1. The canonical acceleration problem of T non-dec is
x
1
x
2
=
x1−n
x2+n
x 1 > 0 ∧ x 2 > 0
x1−1
x2+1
.
The first component ψ of an acceleration problem ψ | q
ϕ |
ϕ | a is the partial
result that has been computed so far. The second component q
ϕ corresponds
to the part of the loop condition that has already been processed successfully.
As our calculus preserves consistency, ψ always approximates q
ϕ, a. The third
component is the part of the loop condition that remains to be processed, i.e., the
loop
ϕ, a still needs to be accelerated. The goal of our calculus is to transform
a canonical into a solved acceleration problem.
More specifically, when we have simplified a canonical acceleration problem
x
= a
n (x) | | | ϕ(x) | a(x) to ψ 1 (y) | q
ϕ(x) |
ϕ(x) | a(x), then ϕ ≡ q
ϕ ∧
ϕ
and
ψ 1 =⇒ x −→
n
q
ϕ,a x
.