Design, formal semantics and verification of parallel programming languages

点击翻译按钮获取中文摘要

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.