Semantics of Parallel Programs

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

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.