Semantics of Parallel Programs

点击翻译按钮获取中文摘要

This is a basic research program concerning semantic models for parallel programming languages. Initial emphasis is on the design of a mathematical model of parallel algorithms extending and generalizing earlier work of Berry and Curien on sequential algorithms and concrete data structures. The model is intensional, in that the denotation of a program includes information about parallel computation strategy in addition to information about the extensional or functional behavior of the program. This allows a novel intensional strictness ordering on parallel algorithms that plays a fundamental role in our theory; for instance, application of a parallel algorithm to its arguments is a continuous operation with respect to this ordering. It will be shown that the model forms a cartesian closed category in which an elegant account of parallel functional computation can be given. It will support semantically-based techniques for proving both traditional (extensional) correctness properties and efficiency properties that depend on intensional aspects of program behavior. The intensional information will be used to determine a hierarchical class of algorithms based on an intuitively reasonable notion of "degree of parallelism". This idea will provide a framework for assessing the relative expressive powers of various sequential and parallel primitives. In the long term theoretical insights gained in this investigation will be in the design of new programming languages that employ parallelism uniformly and generally, yet whose semantic properties are well understood, and for which tractable proof methods can be devised.