Semantics of Parallel Programs

这是一个关于并行程序设计语言语义模型的基础研究项目。最初的重点是设计并行算法的数学模型，扩展和推广了Berry和Curien早期在顺序算法和具体数据结构方面的工作。该模型是内涵的，因为程序的表示除了包括关于程序的扩展或功能行为的信息外，还包括关于并行计算策略的信息。这允许对并行算法进行一种新的内涵严格排序，这在我们的理论中起着基础性的作用；例如，将并行算法应用于其参数是相对于这种排序的连续操作。结果表明，该模型形成了一个笛卡尔闭合范畴，在这个范畴中可以很好地描述并行函数计算。它将支持基于语义的技术，用于证明依赖于程序行为的内涵方面的传统(扩展)正确性属性和效率属性。这些内涵信息将被用来根据“并行度”这一直观合理的概念确定算法的层次化类别。这个想法将为评估各种顺序和并行原语的相对表达能力提供一个框架。从长远来看，从这项研究中获得的理论见解将是设计新的编程语言，这些语言统一和普遍地使用并行性，但其语义属性被很好地理解，并且可以为其设计出易于处理的证明方法。

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.