Validating More Loop Optimizations
Ying Hu, Clark Barrett, Benjamin Goldberg |
Amir Pnueli
|
Translation Validation is a technique for ensuring that a
translator produces correct results. Because complete verification of
the translator itself is often infeasible, translation validation
advocates coupling the verification task with the translation task, so
that each run of the translator produces verification conditions
which, if valid, prove the correctness of the translation.
In
previous work, the translation validation approach was applied to give
a framework for proving the correctness of a variety of compiler
optimizations, with a recent focus on loop transformations. However,
some of these ideas were preliminary and had not been
implemented. Additionally, there were examples of common loop
transformations which could not be handled by our previous
approaches.
This paper
addresses these issues. We introduce a new rule Reduce for loop
reduction transformations, and we generalize our previous rule
Validate so that it can handle transformations which eliminate simple
loops. We then describe how all of this (including some previous
theoretical work) is implemented in our compiler validation tool TVOC.
Key Words: Translation validation, formal methods, loop optimizations.