Semantics of Parallel Programs

并行程序的语义

• 批准号: 9412980
• 负责人: Stephen Brookes
• 金额: $ 19.5万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1995
• 资助国家: 美国
• 起止时间: 1995-09-01 至 1998-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9412980&HistoricalAwards=false
• 关键词: Semantics; Parallel; Programs

This project seeks to develop denotational semantics for a variety of programming languages, tailored to support compositional reasoning about various important forms of program behavior. It studies a typical functional programming language, and two typical parallel imperative languages: a language for shared-variable parallelism, and a language of communicating processes related to Hoare's CSP and Milner's CCS. Notions of behavior considered for the parallel languages include safety and liveness properties, and partial and total correctness, assuming various forms of fairness properties that correspond to natural assumptions about the runtime execution of concurrent processes. This should permit reasoning about parallel programs to be carried out without knowledge of or reference to details concerning scheduling. There also is a research focus on intensional properties concerning runtime and efficient use of resources. Technically, the project aims to develop fully abstract semantics, with respect to a variety of important notions of program behavior. A semantics is fully abstract if it gives the same meaning to two program phrases precisely when they induce identical behavior in all program contexts. This provides a rigorous criterion for judging the utility of a semantics in supporting compositional or modular reasoning about program behavior. The long term goal is the development of a unifying framework suitable for establishing and exploiting relationships between languages, models, and proof methods for reasoning about programs. In particular, the research seeks to establish a mathematically tractable theory and use it to develop practical techniques for modular design and analysis of parallel programs.

这个项目寻求为各种编程语言开发外延语义，以支持关于各种重要程序行为形式的组合推理。它研究了一种典型的函数式编程语言，以及两种典型的并行命令式语言：一种用于共享变量并行的语言，一种与Hoare的CSP和Milner的CCS相关的进程通信语言。并行语言考虑的行为概念包括安全性和活动性属性，以及部分和完全正确，假设各种形式的公平性属性对应于关于并发进程的运行时执行的自然假设。这应该允许在不知道或参考有关调度的细节的情况下执行关于并行程序的推理。也有关于运行时和资源的有效使用的内涵属性的研究。从技术上讲，该项目的目标是开发关于程序行为的各种重要概念的完全抽象语义。当两个程序短语在所有程序上下文中诱导相同的行为时，如果语义赋予两个程序短语相同的含义，则语义是完全抽象的。这为判断语义在支持关于程序行为的组合或模块推理方面的效用提供了严格的标准。长期目标是开发一个统一的框架，适用于建立和利用语言、模型和证明方法之间的关系，以便对程序进行推理。特别是，这项研究试图建立一个数学上易于处理的理论，并使用它来开发并行程序的模块化设计和分析的实用技术。