A Calculus for Modular Loop Acceleration
73
while x 3 > 0 do
x1
x2
x3
←
x1+1
x2−x1
x3+x2
.
Here, the updated value of x 1 depends on x 1 , the update of x 2 depends on x 1
and x 2 , and the update of x 3 depends on x 2 and x 3 . Hence, the closed form of x 1
is linear, the closed form of x 2 is quadratic, and the closed form of x 3 is cubic:
x
(n)
3 = −
1
6 · n
3 +
1−x1
2
· n
2 +
x1
2 + x 2 −
1
3
· n + x 3
So when fixing x 1 , x 2 , and x 3 , x
(n)
3 has up to 2 extrema, i.e., its monotonicity may
change twice. However, our techniques based on eventual monotonicity require
that the respective expressions behave monotonically once they start to de- or
increase, so these techniques only allow one change of monotonicity.
This raises the question if our approach can accelerate every loop with
conjunctive guard and linear arithmetic whose closed form is a vector of (at most)
quadratic polynomials with rational coefficients. We leave this to future work.
For our benchmark collection, links to the StarExec-jobs of our evaluation,
and a pre-compiled binary (Linux, 64 bit) we refer to [14].
9 Conclusion and Future Work
After discussing existing acceleration techniques (Sec. 3), we presented a calculus
to combine acceleration techniques modularly (Sec. 4). Then we showed how to
combine existing (Sec. 5) and two novel (Sec. 6) acceleration techniques with
our calculus. This improves over prior approaches, where acceleration techniques
were used independently, and may thus improve acceleration-based verification
techniques [6,7,11,16–18,28] in the future. An empirical evaluation (Sec. 8) shows
that our approach is more powerful than state-of-the-art acceleration techniques.
Moreover, if it is able to accelerate a loop, then the result is exact (instead of
just an under-approximation) in most cases. Thus, our calculus can be used for
under-approximating techniques (e.g., to find bugs or counterexamples) as well
as in over-approximating settings (e.g., to prove safety or termination).
In the future, we plan to implement the missing features mentioned in Sec. 8
and integrate our novel calculus into our own acceleration-based program analyses
to prove lower bounds on the runtime complexity [16,17] and non-termination [11]
of integer programs. Furthermore, our experiments indicate that integrating
specialized techniques for FMATs (cf. Sec. 7) would improve the power of our
approach, as Flata exactly accelerated 49 loops where LoAT failed to do so (cf.
Sec. 8). Moreover, we plan to design a loop acceleration library, such that our
technique can easily be incorporated by other verification tools.
Data Availability Statement and Acknowledgments The tools and datasets
used for the current study are available in the Zenodo repository [12].
I thank Carsten Fuhs, Marcel Hark, Sophie Tourret, and the anonymous
reviewers for helpful feedback and comments. Moreover, I thank Radu Iosif and
Filip Konecn´ y for their help with Flata.
73
while x 3 > 0 do
x1
x2
x3
←
x1+1
x2−x1
x3+x2
.
Here, the updated value of x 1 depends on x 1 , the update of x 2 depends on x 1
and x 2 , and the update of x 3 depends on x 2 and x 3 . Hence, the closed form of x 1
is linear, the closed form of x 2 is quadratic, and the closed form of x 3 is cubic:
x
(n)
3 = −
1
6 · n
3 +
1−x1
2
· n
2 +
x1
2 + x 2 −
1
3
· n + x 3
So when fixing x 1 , x 2 , and x 3 , x
(n)
3 has up to 2 extrema, i.e., its monotonicity may
change twice. However, our techniques based on eventual monotonicity require
that the respective expressions behave monotonically once they start to de- or
increase, so these techniques only allow one change of monotonicity.
This raises the question if our approach can accelerate every loop with
conjunctive guard and linear arithmetic whose closed form is a vector of (at most)
quadratic polynomials with rational coefficients. We leave this to future work.
For our benchmark collection, links to the StarExec-jobs of our evaluation,
and a pre-compiled binary (Linux, 64 bit) we refer to [14].
9 Conclusion and Future Work
After discussing existing acceleration techniques (Sec. 3), we presented a calculus
to combine acceleration techniques modularly (Sec. 4). Then we showed how to
combine existing (Sec. 5) and two novel (Sec. 6) acceleration techniques with
our calculus. This improves over prior approaches, where acceleration techniques
were used independently, and may thus improve acceleration-based verification
techniques [6,7,11,16–18,28] in the future. An empirical evaluation (Sec. 8) shows
that our approach is more powerful than state-of-the-art acceleration techniques.
Moreover, if it is able to accelerate a loop, then the result is exact (instead of
just an under-approximation) in most cases. Thus, our calculus can be used for
under-approximating techniques (e.g., to find bugs or counterexamples) as well
as in over-approximating settings (e.g., to prove safety or termination).
In the future, we plan to implement the missing features mentioned in Sec. 8
and integrate our novel calculus into our own acceleration-based program analyses
to prove lower bounds on the runtime complexity [16,17] and non-termination [11]
of integer programs. Furthermore, our experiments indicate that integrating
specialized techniques for FMATs (cf. Sec. 7) would improve the power of our
approach, as Flata exactly accelerated 49 loops where LoAT failed to do so (cf.
Sec. 8). Moreover, we plan to design a loop acceleration library, such that our
technique can easily be incorporated by other verification tools.
Data Availability Statement and Acknowledgments The tools and datasets
used for the current study are available in the Zenodo repository [12].
I thank Carsten Fuhs, Marcel Hark, Sophie Tourret, and the anonymous
reviewers for helpful feedback and comments. Moreover, I thank Radu Iosif and
Filip Konecn´ y for their help with Flata.