A Calculus for Modular Loop Acceleration
69
Theorem 12 (Acceleration via Eventual Increase). If ϕ(x) ≡
k
i=1 C i
where each C i contains an inequation expr i (x) > 0 such that
expr i (x) ≤ expr i (a(x)) =⇒ expr i (a(x)) ≤ expr i (a
2 (x)),
then the following acceleration technique is sound:
T loop → x
= a
n (x) ∧
k
i=1
0 < expr i (x) ≤ expr i (a(x))
With Thm. 12, we can accelerate T ev-inc to
x
1
x
2
=
n
2 −n
2 +x2·n+x1
x2+n
∧ 0 < x 1 ≤ x 1 + x 2
(ψ ev-inc )
as we have
(x 1 ≤ x 1 + x 2 ) ≡ (0 ≤ x 2 ) =⇒ (0 ≤ x 2 + 1) ≡ (x 1 + x 2 ≤ x 1 + x 2 + x 2 + 1).
However, Thm. 12 is not exact, as the resulting formula only covers program
runs where each expr i behaves monotonically. So ψ ev-inc only covers those runs
of T ev-inc where the initial value of x 2 is non-negative. Again, turning Thm. 12
into a conditional acceleration technique is straightforward.
Theorem 13 (Conditional Acceleration via Eventual Increase). If we
have χ(x) ≡
k
i=1 C i where each C i contains an inequation expr i (x) > 0 such
that
q
ϕ(x) ∧ expr i (x) ≤ expr i (a(x)) =⇒ expr i (a(x)) ≤ expr i (a
2 (x)),
(4)
then the following conditional acceleration technique is sound:
(χ, a, q
ϕ) → x
= a
n (x) ∧
k
i=1
0 < expr i (x) ≤ expr i (a(x))
Example 6. Consider the following variant of T ev-inc .
while x 1 > 0 ∧ x 3 > 0 do
x1
x2
x3
←
x1+x2
x2+x3
x3
Starting with its canonical acceleration problem, we get
x
= a
n (x)
x 1 > 0 ∧ x 3 > 0
a :=
x1+x2
x2+x3
x3
T hm. 8
e x
= a
n (x) ∧ x 3 > 0 | x 3 > 0 | x 1 > 0 | a
T hm. 13
x
= a
n (x) ∧ x 3 > 0 ∧ 0 < x 1 ≤ x 1 + x 2 | x 3 > 0 ∧ x 1 > 0 | | | a
where the second step can be performed via Thm. 13 as
( q
ϕ(x) ∧ expr (x) ≤ expr (a(x))) ≡ (x 3 > 0 ∧ x 1 ≤ x 1 + x 2 ) ≡ (x 3 > 0 ∧ 0 ≤ x 2 )
implies
(0 ≤ x 2 + x 3 ) ≡ (x 1 + x 2 ≤ x 1 + x 2 + x 2 + x 3 ) ≡ (expr (a(x)) ≤ expr (a
2 (x))).