Specifying and executing optimizations for generalized control flow graphs
| Autor: | Elsa L. Gunter, William Mansky, Dennis Griffith, Michael D. Adams |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
Syntax (programming languages)
Programming language Semantics (computer science) Computer science 020207 software engineering 0102 computer and information sciences 02 engineering and technology Parallel computing computer.file_format computer.software_genre 01 natural sciences Control flow 010201 computation theory & mathematics Formal specification 0202 electrical engineering electronic engineering information engineering Temporal logic Compiler Executable State (computer science) computer Software |
| Zdroj: | Science of Computer Programming. 130:2-23 |
| ISSN: | 0167-6423 |
| DOI: | 10.1016/j.scico.2016.06.003 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect