A Calculus for Modular Loop Acceleration
59
integrated into our framework. Next, we present two novel acceleration techniques
and incorporate them into our calculus in Sec. 6. After discussing related work
in Sec. 7, we demonstrate the applicability of our approach via an empirical
evaluation in Sec. 8 and conclude in Sec. 9. All proofs can be found in [13].
2 Preliminaries
We use bold letters x, y, z, ... for vectors. Let C (z) be the set of closed-form
expressions over the variables z containing, e.g., all arithmetic expressions built
from z, integer constants, addition, subtraction, multiplication, division, and
exponentiation.
1 We consider loops of the form
while ϕ do x ← a
(T loop )
where x is a vector of d pairwise different variables that range over the integers,
the loop condition ϕ ∈ Prop(C (x)) is a finite propositional formula over the
atoms {p > 0 | p ∈ C (x)}, and a ∈ C (x)
d such that the function
2
x → a maps
integers to integers. Loop denotes the set of all such loops.
We identify T loop and the pair ϕ, a. Moreover, we identify a and the function
x → a where we sometimes write a(x) to make the variables x explicit and we
use the same convention for other (vectors of) expressions. Similarly, we identify
the formula ϕ resp. ϕ(x) and the predicate x → ϕ.
Throughout this paper, let n be a designated variable and let:
a :=
a1
...
a d
x :=
x1
...
x d
x
:=
x
1
...
x
d
y :=
x
n
x
Intuitively, the variable n represents the number of loop iterations and x
corresponds to the values of the program variables x after n iterations.
T loop induces a relation −→ T loop on Z
d :
ϕ(x) ∧ x
= a(x) ⇐⇒ x −→ T loop x
Our goal is to find a formula ψ ∈ Prop(C (y)) such that
ψ ⇐⇒ x −→
n
T loop
x
for all n > 0.
(equiv)
To see why we use C (y) instead of, e.g., polynomials, consider the loop
while x 1 > 0 do (
x1
x2 ) ←
x1−1
2·x2
.
(T exp )
Here, an acceleration technique synthesizes, e.g., the formula
x
1
x
2
=
x1−n
2
n ·x2
∧ x 1 − n + 1 > 0
( ψ exp )
1 Note that there is no widely accepted definition of “closed forms” and the results of
the current paper are independent of the precise definition of C (z).
2 i.e., the (anonymous) function that maps x to a
59
integrated into our framework. Next, we present two novel acceleration techniques
and incorporate them into our calculus in Sec. 6. After discussing related work
in Sec. 7, we demonstrate the applicability of our approach via an empirical
evaluation in Sec. 8 and conclude in Sec. 9. All proofs can be found in [13].
2 Preliminaries
We use bold letters x, y, z, ... for vectors. Let C (z) be the set of closed-form
expressions over the variables z containing, e.g., all arithmetic expressions built
from z, integer constants, addition, subtraction, multiplication, division, and
exponentiation.
1 We consider loops of the form
while ϕ do x ← a
(T loop )
where x is a vector of d pairwise different variables that range over the integers,
the loop condition ϕ ∈ Prop(C (x)) is a finite propositional formula over the
atoms {p > 0 | p ∈ C (x)}, and a ∈ C (x)
d such that the function
2
x → a maps
integers to integers. Loop denotes the set of all such loops.
We identify T loop and the pair ϕ, a. Moreover, we identify a and the function
x → a where we sometimes write a(x) to make the variables x explicit and we
use the same convention for other (vectors of) expressions. Similarly, we identify
the formula ϕ resp. ϕ(x) and the predicate x → ϕ.
Throughout this paper, let n be a designated variable and let:
a :=
a1
...
a d
x :=
x1
...
x d
x
:=
x
1
...
x
d
y :=
x
n
x
Intuitively, the variable n represents the number of loop iterations and x
corresponds to the values of the program variables x after n iterations.
T loop induces a relation −→ T loop on Z
d :
ϕ(x) ∧ x
= a(x) ⇐⇒ x −→ T loop x
Our goal is to find a formula ψ ∈ Prop(C (y)) such that
ψ ⇐⇒ x −→
n
T loop
x
for all n > 0.
(equiv)
To see why we use C (y) instead of, e.g., polynomials, consider the loop
while x 1 > 0 do (
x1
x2 ) ←
x1−1
2·x2
.
(T exp )
Here, an acceleration technique synthesizes, e.g., the formula
x
1
x
2
=
x1−n
2
n ·x2
∧ x 1 − n + 1 > 0
( ψ exp )
1 Note that there is no widely accepted definition of “closed forms” and the results of
the current paper are independent of the precise definition of C (z).
2 i.e., the (anonymous) function that maps x to a