Design, formal semantics and verification of parallel programming languages

随着并行和分布式计算机系统的飞速发展，提高并行程序的生产率和可靠性的研究近年来备受关注。在这项研究中，我们首先为异步通信过程设计了一种并行处理语言DNNP，并给出了该语言的简单和高度抽象的指称语义。为了给具有非确定性选择的并行语言给出一个组合语义，我们需要克服一个被称为Brock-Ackerman异常的问题，从而指出给这种语言给出一个高度抽象的语义是非常困难的，而且，如果语言不仅具有非确定性，而且还具有动态创建过程，那么给出一个高度抽象的语义就变得更加困难。对于具有这些功能的DNNP语言，我们已经成功地呈现了这样的语义。接下来，我们利用延拓的概念对该语义进行了改进，得到了一个更加抽象和可理解的DNNP语言语义。具有不确定性的并行语言的延续语义很少。因此，我们的研究展示了如何给出这种延续语义，并证明了它的有效性。此外，我们还研究了如何设计一种同时具有面向对象风格和并行性概念的语言，从而通过在DNNP语言中加入对象的概念，设计了一种基于对象的DNNO语言，并给出了DNNO的外延语义。虽然DNNO语言不具备面向对象范式的全部特征，但本研究对并行面向对象语言研究领域的发展具有重要意义。在本研究中，我们还在并行程序的验证和DNNP语言处理器的构建方面取得了一些基本的成果。

With the rapid progress of parallel and distributed computer systems, the research in the improvement of productivity and reliability of parallel programs has received much attention in recent years. In this study, we have first designed a parallel processing language DNNP for asynchronously communicating processes, and presented a simple and highly abstract denotational semantics for this language. In order to give a compositional semantics for a parallel language with nondeterministic choice, we need to overcome a problem called Brock-Ackerman anomaly, so that it has been pointed out that it is very difficult to give an highly abstract semantics for such one, Moreover, if the language has not only nondeterminism but also dynamic creation of processes, then it becomes a much harder task to give a highly abstract semantics. For the language DNNP with these facilities we have succeeded in presenting such semantics. Next, using the notion of continuation, we have improved this semantics and obtained a more abstract and comprehensible semantics of the language DNNP. There have been few continuation semantics of a parallel language with nondeterminism. Thus, our study has shown how to give a continuation semantics for such one and proven the usefulness. Moreover, we have studied how to design a language which consistently possesses both the notions of object-oriented style and parallelism, so that an object-based language DNNO has been designed by adding the language DNNP the notion of objects, and a denotation semantics for DNNO has been presented. Although the language DNNO does not possess all the characteristics of object-oriented paradigm, this research will be useful for the development of this research field of parallel object-oriented languages. In this study, we have also obtained some basic results on verification of parallel programs and on the construction of language processors of DNNP.