Design, formal semantics and verification of parallel programming languages

随着并行和分布式计算机系统的快速发展，提高并行程序的生产率和可靠性的研究近年来受到了极大的关注。在本研究中，我们首先设计了一种用于进程异步通信的并行处理语言DNNP，并给出了该语言简单且高度抽象的指称语义。为了给具有不确定选择的并行语言提供组合语义，我们需要克服一个称为Brock-Ackerman异常的问题，从而指出给这种语言一个高度抽象的语义是非常困难的，而且，如果该语言不仅具有不确定性，而且还具有进程的动态生成，那么给出一个高度抽象的语义就变得更加困难。对于具有这些功能的语言DNNP，我们已经成功地给出了这样的语义。其次，利用延拓的概念，改进了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.