Specifying and executing optimizations for generalized control flow graphs

William Mansky, Elsa L. Gunter, Dennis Griffith, and Michael D. Adams

Status: Published

Abstract

Optimizations performed by compilers, usually expressed as rewrites on program graphs, are a core part of modern compilers. However, even production compilers have bugs, and these bugs are difficult to detect and resolve. In this paper we present Morpheus, a domain-specific language for formal specification of program transformations, and describe its executable semantics. The fundamental approach of Morpheus is to describe program transformations as rewrites on control flow graphs with temporal logic side conditions. The syntax of Morpheus allows cleaner, more comprehensible specifications of program optimizations; its executable semantics allows these specifications to act as prototypes for the optimizations themselves, so that candidate optimizations can be tested and refined before going on to include them in a compiler. We demonstrate the use of Morpheus to state, test, and refine the specification of a variety of transformations, including a simple loop peeling transformation for single-threaded code and a redundant store elimination optimization on parallel programs.

Keywords

Optimizing compilers; Program transformations; Temporal logic; SMT solvers

Citation

William Mansky, Elsa L. Gunter, Dennis Griffith, and Michael D. Adams. Specifying and executing optimizations for generalized control flow graphs. Science of Computer Programming, 130:2–23, November 2016. ISSN 0167-6423. doi: 10.1016/j.scico.2016.06.003.

BibTeX Entry

@article{mansky2016ptrans,
  author = {Mansky, William and Gunter, Elsa L. and Griffith, Dennis and Adams, Michael D.},
  title = {Specifying and executing optimizations for generalized control flow graphs},
  journal = {Science of Computer Programming},
  pages = {2--23},
  year = {2016},
  volume = {130},
  month = nov,
  issn = {0167-6423},
  doi = {10.1016/j.scico.2016.06.003},
}