60
F. Frohn
where
x1−n
2
n ·x2
is equivalent to the value of (
x1
x2 ) after n iterations and the inequation x 1 − n + 1 > 0 ensures that T exp can be executed at least n times. Clearly,
the growth of x 2 cannot be captured by a polynomial, i.e., even the behavior of
quite simple loops is beyond the expressiveness of polynomial arithmetic.
In practice, one can restrict our approach to weaker classes of expressions to
ease automation, but the presented results are independent of such considerations.
Some acceleration techniques cannot guarantee (equiv), but the resulting
formula is an under-approximation of T loop , i.e., we have
ψ =⇒ x −→
n
T loop
x
for all n > 0.
(approx)
If (equiv) resp. (approx) holds, then ψ is equivalent to resp. approximates T loop .
Definition 1 (Acceleration Technique). An acceleration technique is a partial function
accel : Loop Prop(C (y)).
It is sound if accel (T ) approximates T for all T ∈ dom(accel ). It is exact if
accel (T ) is equivalent to T for all T ∈ dom(accel ).
3 Existing Acceleration Techniques
We now recall several existing acceleration techniques. In Sec. 4 we will see how
these techniques can be combined in a modular way. All of them first compute a
closed form c ∈ C (x, n)
d for the values of the program variables after n iterations.
Definition 2 (Closed Form). We call c ∈ C (x, n)
d a closed form of T loop if
∀x ∈ Z
d , n ∈ N. c = a
n (x).
Here, a
n is the n-fold application of a, i.e., a
0 (x) = x and a
n+1 (x) =
a(a
n (x)). To find closed forms, one tries to solve the system of recurrence
equations x
(n) = a(x
(n−1) ) with the initial condition x
(0) = x. In the sequel, we
assume that we can represent a
n (x) in closed form. Note that one can always
do so if a(x) = Ax + b with A ∈ Z
d×d and b ∈ Z
d , i.e., if a is affine. To this
end, one considers the matrix B :=
A b
0
T 1
and computes its Jordan normal form
B = T
−1 JT where J is a block diagonal matrix (which has complex entries if B
has complex eigenvalues). Then the closed form for J
n can be given directly (see,
e.g., [31]) and a
n (x) = T
−1 J
n T (
x
1 ). Moreover, one can compute a closed form if
a =
c1·x1+p1
...
c d ·x d +p d
where c i ∈ N and each p i is a polynomial over x 1 , . . . , x i−1 [15].
3.1 Acceleration via Decrease or Increase
The first acceleration technique discussed in this section exploits the following
observation: If ϕ(a(x)) implies ϕ(x) and ϕ(a
n−1 (x)) holds, then T loop is applicable at least n times. So in other words, it requires that the indicator function
(or characteristic function) I ϕ : Z
d
→ {0, 1} of ϕ with I ϕ (x) = 1 ⇐⇒ ϕ(x) is
monotonically decreasing w.r.t. a, i.e., I ϕ (x) ≥ I ϕ (a(x)).
F. Frohn
where
x1−n
2
n ·x2
is equivalent to the value of (
x1
x2 ) after n iterations and the inequation x 1 − n + 1 > 0 ensures that T exp can be executed at least n times. Clearly,
the growth of x 2 cannot be captured by a polynomial, i.e., even the behavior of
quite simple loops is beyond the expressiveness of polynomial arithmetic.
In practice, one can restrict our approach to weaker classes of expressions to
ease automation, but the presented results are independent of such considerations.
Some acceleration techniques cannot guarantee (equiv), but the resulting
formula is an under-approximation of T loop , i.e., we have
ψ =⇒ x −→
n
T loop
x
for all n > 0.
(approx)
If (equiv) resp. (approx) holds, then ψ is equivalent to resp. approximates T loop .
Definition 1 (Acceleration Technique). An acceleration technique is a partial function
accel : Loop Prop(C (y)).
It is sound if accel (T ) approximates T for all T ∈ dom(accel ). It is exact if
accel (T ) is equivalent to T for all T ∈ dom(accel ).
3 Existing Acceleration Techniques
We now recall several existing acceleration techniques. In Sec. 4 we will see how
these techniques can be combined in a modular way. All of them first compute a
closed form c ∈ C (x, n)
d for the values of the program variables after n iterations.
Definition 2 (Closed Form). We call c ∈ C (x, n)
d a closed form of T loop if
∀x ∈ Z
d , n ∈ N. c = a
n (x).
Here, a
n is the n-fold application of a, i.e., a
0 (x) = x and a
n+1 (x) =
a(a
n (x)). To find closed forms, one tries to solve the system of recurrence
equations x
(n) = a(x
(n−1) ) with the initial condition x
(0) = x. In the sequel, we
assume that we can represent a
n (x) in closed form. Note that one can always
do so if a(x) = Ax + b with A ∈ Z
d×d and b ∈ Z
d , i.e., if a is affine. To this
end, one considers the matrix B :=
A b
0
T 1
and computes its Jordan normal form
B = T
−1 JT where J is a block diagonal matrix (which has complex entries if B
has complex eigenvalues). Then the closed form for J
n can be given directly (see,
e.g., [31]) and a
n (x) = T
−1 J
n T (
x
1 ). Moreover, one can compute a closed form if
a =
c1·x1+p1
...
c d ·x d +p d
where c i ∈ N and each p i is a polynomial over x 1 , . . . , x i−1 [15].
3.1 Acceleration via Decrease or Increase
The first acceleration technique discussed in this section exploits the following
observation: If ϕ(a(x)) implies ϕ(x) and ϕ(a
n−1 (x)) holds, then T loop is applicable at least n times. So in other words, it requires that the indicator function
(or characteristic function) I ϕ : Z
d
→ {0, 1} of ϕ with I ϕ (x) = 1 ⇐⇒ ϕ(x) is
monotonically decreasing w.r.t. a, i.e., I ϕ (x) ≥ I ϕ (a(x)).