Semantics-Based Parallel Cost Models and Their Use in Provably EfficientImplementations

摘要

Understanding the performance issues of modern programming language execution canbe difficult. These languages have abstract features, such as higher-order functions, laziness, and objects, that ease programming, but which make their mapping to the underlying machine more difficult. Understanding parallel languages is further complicated by the need to describe what computations are performed in parallel and how they are affected by communication and latency in the machine. This lack of understanding can obscure even the asymptotic performance of a program and can also hide performance bugs in the language implementation. 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.