Nuno P. Lopes
Compiler optimizations are increasingly important and complex. Developers rely on them to improve performance, reduce code size, and reduce power consumption of their programs. The advent of mobile devices with limited resources and the need to minimize the operating costs of data centers puts even more pressure on the quality of the results of compiler optimizations. Therefore, compiler developers are being forced to devise and quickly deploy new and more complex optimizations, which compromises correctness.
Compiler optimizations are still designed and implemented by hand, and usually without providing any formal guarantee of correctness. Moreover, in addition to devising the code transformations, developers have to come up with an analysis that determines in which cases the optimization can be applied. In other words, the optimization designer has to specify a precondition that ensures that the optimization is semantics-preserving, as well as implement an algorithm to check if a given code fragment fulfills the precondition.
Devising preconditions for optimizations by hand is a non-trivial task. It is easy to miss a corner case, making the optimization unsound. It is also easy to specify a precondition that, although correct, is too restrictive, and therefore misses some optimization opportunities.
In this thesis, I propose an algorithm for the automatic synthesis of weakest preconditions for compiler optimizations. It is, to the best of my knowledge, the first known algorithm for this task. The algorithm works in a counterexample-driven way and is complete, modulo the employed verification tool.
I also propose a new algorithm to prove program equivalence, with an application to proving correctness of compiler optimizations. This algorithm is able to automatically verify more optimizations than any previously proposed technique. The algorithm works by transforming optimizations into numeric programs and then computing a precise summary of their behavior.
N. P. Lopes. Automatic Synthesis of Weakest Preconditions for Compiler Optimizations. PhD thesis, Instituto Superior Técnico, July 2014.
@phdthesis{Lopes-phdthesis,
title = {Automatic Synthesis of Weakest Preconditions for Compiler Optimizations},
author = {Nuno P. Lopes},
school = {Instituto Superior T\'{e}cnico},
month = jul,
year = 2014
}