A Calculus for Modular Loop Acceleration
paper written by Florian Frohn
Vincent Mihalkovic 456247@mail.muni.cz
Faculty of Informatics, Masaryk University December 1, 2021
Intruduction
Acceleration techniques
Where? static analyses for programs operating on integers.
How? extract a quantifier-free first-order formula ^ from a singLe-path Loop T.
Why? proving safety, reachability, deducing bounds, proving (non-)termination.
This paper:
■ existing acceleration techniques only apply if certain prerequisites are in place.
■ introduce a calculus which allows for combining several acceleration techniques modularly.
■ two novel acceleration techniques .
V. Mihalkovic • IA072 • December 1, 2021
2/20
Preliminaries
■ x,y,z,... for vectors
/ ai
■ a := ...
\ od
■ Let ^(z) be the set of closed-form expressions ofver the variables z containing, e.g., all arithemtic expressions built from z, integer constants, addition, subtraction, muLtipication, division and exponentiation.
■ We identify TToop (the set of all such Loops) and the pair (cp, a).
■ while ip do x <— a
■ (p e Prop(^(x)) is a finite propositionaL formula over the atoms {p > 0 | p e ^(x)}. We identify the formula (p(x) and the predicate x i-> <p
■ function x i-> a maps integers to integers. We write a(x) to make the variables x explicit.
e.g.: while xi > 0 do (      J <- f ^ ^~ 1 ) (7IooP)
X o
V. Mihalkovic . IA072 . December 1, 2021 3/20
Preliminaries
Throughout this presentation, let n be a designated variable and let:
Intuitively, the variable n represents the number of loop iterations and j corresponds to the values of the program variables x after n iterations.
■ 7ioop induces a relation —>r[oop on Zd :
ip(x) a x' = a(x) <=> x —>T[oop x'
■ Our goal is to find a formula ^ e Prop(^(y)) such that
ib^^x—x' forall/?>0
T I Loop
■ Some acceleration techniques cannot guarantee (equiv), but the resulting formula is an under-approximation of 7Toop i-e., we have
i^^^x —>^oop x'   for all n > 0
If (equiv) resp. ( approx) holds, then ^ is equivalent to resp. approximates 7[00D.
V. Mihalk6vic • IA072 . DecemBerl, 2021
Acceleration techniques
An acceleration technique is a partial function
acceL: Loop Prop(V(y))
sound if acceL (T) approximates T for all T e dom( acceL).
exact if acceL (T) is equivaLent to T for aLL T e dom( acceL).
■ ALL these techniques first compute a dosed form c e ff(x, n)d for the vaLues of the program variabLes after n iterations.
■ We caLL c e ^(x, n)d a cLosed form of 7Toop if
\/xeZd,neN.c = an(x)
m Here, an is the /7-foLd appLication of a, i.e., a°(x) = x and an+1(x) = a(an(x)).
V. Mihalkovic • IA072 • December 1, 2021
5/20
Acceleration via Monotonie Decrease
If ip(a(x)) implies tp(x) and (p (an_1(x)) holds, then 7Toop is applicable at Least n times.
So in other words: 1^ : Zd -> {0,1} of <p with /^(x) = 1       <p(x) is monotonically decreasing w.r.t. a, i.e., /^(x) /v?(a(x)). Theorem 1: If
¥>(a(x)) => p(x) then the following acceleration technique is exact:
7TooP -x'= a"(x) a(^(an-1(x))
Limitations:
While Xi > 0 a X2 > 0 dO ^ ^ ) *~ ( x2 + 1 ) C^on-dec )
It cannot be accelerated with Thm. 1 as
Xi-1>0ax2 + 1>0^Xi>0aX2>0
V. Mihalkovic • IA072 . December 1, 2021
6/20
Example recalled
So for example, Thm. 1 accelerates Texp to ipexp.
whilfiX^Odo (Texp)
Since
Xi — 1 > 0 ^ Xi > 0
<p(<*(*))
an acceleration technique synthesizes, e.g., the formula
%) = ( 2"TX" ) - Xj- n + 1 > 0 (^exp)
V. Mihalkovic • IA072 • December 1, 2021
Acceleration via Monotonie Increase
Theorem 2: If
then the following acceleration technique is exact:
TToop    x7 = a"(x) a <p(x)
As a minimaL example, Thm. 2 accelerates
while x>0dox^x + l
to
xf = x + riAX>0
V. MihaLkovic • IA072 . December 1, 2021 8/20
Acceleration via Decrease and Increase
Theorem 3: If
(p(x) V?l(x) a (p2(x) a V93(X)
¥>i(x) =>^i(a(x))
^l(x) a V92(X) a V93(X) => ^3(^(X))
then the following acceleration technique is exact:
TToop    x7 = a"(x) a ^(x) a (p2 (a""1^)) A ^3(x)
Here, ipi and (^3 are again invariants of the loop. Thus, as in Thm. 2 it suffices to require that they hold before entering the loop. On the other hand, ^2 needs to satisfy a similar condition as in Thm. 1 and thus it suffices to require that ^2 holds before the last iteration. We also say that ^2 is a converse invariant (w.r.t. cpi). It is easy to see that Thm. 3 is equivalent to Thm. 1 if cpi = cpi = T (where T denotes logical truth) and it is equivalent to Thm. 2 if (f2 = ¥1 — T.
V. Mihalkovic • IA072 • December 1, 2021
9/20
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.
■ CaLcuLus that repeatedLy appLies acceleration techniques to simplify an acceleration problem resulting from a Loop 7i00p ur|til it is solved and hence gives rise to a suitable   e Prop(^(y)) which approximates resp. is equivalent to TIoop •
V. Mihalkovic • IA072 . December 1, 2021
10/20
Acceleration Problem
Definition 3 A tuple
a\ where
■ ijj e Prop(^(y)),the partial result that has been computed so far m (p e Prop(^(x)),the part of the loop condition that remains to be
processed       always approximates ((J5, a» m (f e Prop(^(x)),the part of the loop condition that has already been processed successfully   (loop     a) still needs to be accelerated)
■ a : Zd Zd
The canonical acceleration problem of a Loop 7i00p "s
[x' = a»|T|^(x)|a(x)]
Possible states:
■ consistent if ^ approximates a),
■ exact if ^ is equivalent to a),
■ solved if it is consistent and (p = T.
The goal of our calculus is to transform a canonical into a solved acceleration problem.
V. Mihalkovic • IA072 . December 1, 2021 11 / 20
If) Lf) if
Acceleration problem
When we have simplified a canonical acceleration problem from [x' = an(x) | T | cp(x) \ a(x)J
to [^i(y) | £(x) | £(x) | a(x)] then
ip = Lp a (p and -01 => x —>^>fl> x' Thus, it then suffices to find some ^2 e Prop(^(y)) such that
x
The reason is that we have and thus
^1 a ^2 => X -^_flv X7
i.e., ^1 a ^2 approximates 7Toop •
V. Mihalkovic • IA072 • December 1, 2021
Conditional acceleration
Definition 4 We call a partial function
accel: Loop x Prop(V(x)) Prop(^(y))
a conditional acceleration technique, sound if
x —► <v5,*>x' A accel«X, a>, <p)    implies   x —► ^a>x' for all ((x, a), <p) e dom( accel ),x,x' e Zd, and a? > 0. exact if additionally
* —► (XA^,a/    implies    accel«x, a>,
for all ((x, a), <£) e dom( accel ),x,x' e Zd, and n > 0
We are now ready to present our acceleration calculus, which combines Loop acceleration techniques in a modular way.
V. Mihalkovic • IA072 . December 1, 2021 13 / 20
Acceleration Calculus
Definition 5 The relation on acceleration problems is defined by the following rule:
sound CondAccelTechn
/-A-N
0 / x ^ 0    accel«x, a), ^2 1^1 I    I (p I a] —>(e) lipi u ^2 I    u x I £\x I 0"
step is exact (written —>e) if accel is exact.
■ our calculus allows us to pick a subset x (of clauses) from the yet unprocessed condition (p and
■ "move" it to (J5, which has already been processed successfully.
■ To this end, (x, a) needs to be accelerated by a conditional acceleration technique, i.e., when accelerating (x, d) we may assume x —► ^ ayx'.
Note that every acceleration technique trivially gives rise to a conditional acceleration technique (by disregarding the second argument $ of accel in Def. 4). Thus, our calculus allows for combining arbitrary existing acceleration techniques without adapting them.
V. Mihalkovic • IA072 • December 1, 2021
14/20
Example
while xi > 0 a x2 > 0 do
(Tn
non-dec
Xi — n x2 + n
T Xi > 0 a xj > 0
V. Mihalkovic • IA072 • December 1, 2021
15/20
Acceleration calculus, properties
Lemma 1. —* preserves consistency and —*e preserves exactness. Then the correctness of our calculus follows immediately. The reason is that
[x' = an(x)\T\<p(x) |a(x)] —*e) |^(y)| £(x)|T|a(x)] implies <p = Cp
Theorem 5 (Correctness of ^ ). If
[x' = an(x)\T\<p(x) |a(x)] —* [^(y)| (?(x)|T|a(x)] then tj) approximates TIoop •
If
[x' = an(x)\T\ip(x) \a(x)j —e* bl>(y)\m\T\a(x)} then t\) is equivalent to TIoop •
Termination of our calculus is trivial, as the size of the third component Cp of the acceleration problem is decreasing. Theorem 6 (Termination of
sj^j*. ^# sj^j*. terminates.
V. Mihalkovic • IA072 • December 1, 2021
16/20
Conditional Acceleration via Monotonie Decrease
Theorem 7 If
then the following conditional acceleration technique is exact:
So we just add $ to the premise of the implication that needs to be checked to apply acceleration via monotonie decrease. Thm. 2 can be adapted analogously.
V. Mihalkovic • IA072 • December 1, 2021
17/20
Acceleration via Eventual Monotonicity
The combination of the calculus and the conditional acceleration techniques still fails to handle certain interesting classes of loops ... Acceleration via Eventual Decrease All (combinations of) techniques presented so far fail for the following example.
The reason is that xi does not behave monotonically ...
Theorem 10 (Acceleration via Eventual Decrease). If (p(x) = /\f=1 C, where
each C, contains an inequation expr ,-(x) > 0 such that
ev—dec
expr,-(x) ^ expr/(a(x)) =^> expr/(a(x)) ^ expr,- (a2(x)
then the following acceleration technique is sound:
i=l
If C, = expr, > 0 for all / e [1, k], then it is exact.
V. Mihalkovic • IA072 • December 1, 2021
18/20
Experiments
■ Loop Acceleration Tool - LoAT
■ LoAT uses Z3 to check implications and PURRS to compute closed forms.
■ To evaluate our approach, they extracted 1511 loops with conjunctive guards from the category Termination of Integer Transition Systems of the Termination Problems Database which is used at the annual Termination and Complexity Competition
■ Flata, which implements the techniques to accelerate FMATs and octagonal relations
V. Mihalkovic • IA072 • December 1, 2021
19/20
Experiment tables
	LoAT	Monot.	Meter	FLata
exact	1444	845	O3	1231
approx	38	0	733	0
fail	29	666	778	280
avg rt	0.16 s	0.11 s	0.09 s	0.47 s
	Ev Inc	Ev Doc	Ev Mon	
exact	1444	845	845	
approx	0	493	0	
fail	67	173	666	
avg rt	0.15 s	0.14 s	0.09 s	
V. Mihalkovic • IA072 • December 1, 2021
20/20
MUNI
FACULTY
OF INFORMATICS