RECORD
Specifying and Executing Optimizations for Parallel Programs
Programming Languages · Submitted 30 Jul 2014
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim The syntax of PTRANS allows cleaner, more comprehensible specification 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.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
Compiler optimizations, usually expressed as rewrites on program graphs, are a core part of all modern compilers. However, even production compilers have bugs, and these bugs are difficult to detect and resolve. The problem only becomes more complex when compiling parallel programs; from the choice of graph representation to the possibility of race conditions, optimization designers have a range of factors to consider that do not appear when dealing with single-threaded programs. In this paper we present PTRANS, a domain-specific language for formal specification of compiler transformations, and describe its executable semantics. The fundamental approach of PTRANS is to describe program transformations as rewrites on control flow graphs with temporal logic side conditions. The syntax of PTRANS allows cleaner, more comprehensible specification 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 PTRANS to state, test, and refine the specification of a redundant store elimination optimization on parallel programs.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | Compiler optimizations, usually expressed as rewrites on program graphs, are a core part of all modern compilers. | background 1.00 | 0.04 | 0.02 | asserted 1.00 |
| s1 | However, even production compilers have bugs, and these bugs are difficult to detect and resolve. | background 0.98 | 0.07 | 0.02 | asserted 1.00 |
| s2 | The problem only becomes more complex when compiling parallel programs; from the choice of graph representation to the possibility of race conditions, optimization designers have a range of factors to consider that do not appear when dealing with single-threaded programs. | background 0.96 | 0.05 | 0.02 | asserted 1.00 |
| s3 | In this paper we present PTRANS, a domain-specific language for formal specification of compiler transformations, and describe its executable semantics. | contribution 1.00 | 0.93 | 0.21 | asserted 1.00 |
| s4 | The fundamental approach of PTRANS is to describe program transformations as rewrites on control flow graphs with temporal logic side conditions. | method 0.90 | 0.68 | 0.10 | asserted 1.00 |
| s5 | The syntax of PTRANS allows cleaner, more comprehensible specification 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. | contribution 0.51 | 0.52 | 0.33 | asserted 1.00 |
| s6 | We demonstrate the use of PTRANS to state, test, and refine the specification of a redundant store elimination optimization on parallel programs. | contribution 0.86 | 0.96 | 0.29 | asserted 1.00 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original abstract
Compiler optimizations, usually expressed as rewrites on program graphs, are a core part of all modern compilers. However, even production compilers have bugs, and these bugs are difficult to detect and resolve. The problem only becomes more complex when compiling parallel programs; from the choice of graph representation to the possibility of race conditions, optimization designers have a range of factors to consider that do not appear when dealing with single-threaded programs. In this paper we present PTRANS, a domain-specific language for formal specification of compiler transformations, and describe its executable semantics. The fundamental approach of PTRANS is to describe program transformations as rewrites on control flow graphs with temporal logic side conditions. The syntax of PTRANS allows cleaner, more comprehensible specification 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 PTRANS to state, test, and refine the specification of a redundant store elimination optimization on parallel programs.
Human review
How the literature uses it
1 arXiv paper cite this in 1 sentence
What it cites · 1 sentence without a confident label
Uses the method or tool of 1 paper
-
All formalizations and proofs have been developed in the Isabelle theorem prover [ref] , allowing us to provide strong guarantees of correctness for our verified optimizations.
cs.LO/9301106 · : A Language for Parallel Program Transformation · 0.99
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.