Computer Science Department
School of Computer Science, Carnegie Mellon University
Semantics-based Parallel Cost Models and Their Use in Provably Efficient Implementations
The dissertation introduces a framework of provably efficient implementations in which performance issues of a language can be defined and analyzed. We define several language models, each consisting of an operational semantics augmented with the costs of execution. In particular, the dissertation examines three functional languages based on fork-and-join parallelism, speculative parallelism, and data-parallelism, and it examines their time and space costs. We then define implementations of each language model onto several common machine models, prove these implementations correct, and derive their costs.
Each of these implementations uses an intermediate model based on an abstract machine to stage the overall implementation. The abstract machine executes a series of steps transforming a stack of active states and store into new states and store. The dissertation proves the efficiency of the implementation by relating the steps to the parallel traversal of a computation graph defined in the augmented operational semantics.
Provably efficient implementations are useful for programmers, language implementors, and language designers. For example, they provide a formal definition of language and implementation costs for program analysis, compiler specification, and language comparisons. The dissertation describes performance problems in existing implementations of Id and NESL and gives provably more efficient alternatives for each. It also compares the example language models, first using several specific algorithms, and also in more generality, for example, quantifying the speedup obtainable in the data-parallel language relative to the fork-and-join language.