Design, formal semantics and verification of parallel programming languages

并行编程语言的设计、形式语义和验证

• 批准号: 02680022
• 负责人: OYAMAGUCHI Michio
• 金额: $ 0.7万
• 依托单位: Mie university
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1990
• 资助国家: 日本
• 起止时间: 1990 至 1992
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-02680022/
• 关键词: parallel processing; denotational semantics; continuation; object oriented; language processor; program verification; 形式的意味論; 必須呼び出し計算; 正当性検証; 表示的意味記述

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.

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

项目成果

Oyamaguchi, M.: "Continuation Semantics of Dynamic Networks of Nondeterministic Processes" Technical Report of IEICE Japan, COMP. 91-62. 31-40 (1991)

Oyamaguchi, M.：“非确定性过程动态网络的连续语义”IEICE 日本技术报告，COMP。

OYAMAGUCHI,M.: "On the Word Problem for RightーGround TermーRewriting Systems" The Transaction of the IEICE. E73. 718-723 (1990)

OYAMAGUCHI, M.：“关于右－基本术语－重写系统的单词问题”，IEICE 718-723（1990）。

大山口 通夫: "接続法による並列処理言語DNNPの表示的意味記述について" 電子情報通信学会技術研究報告. COMP. 62.31-40 (1991)

Michio Oyamaguchi：“关于使用虚拟语气方法的并行处理语言 DNNP 的指称语义描述”IEICE COMP 62.31-40 (1991)。

神田 孝浩: "Supercombinatorに基づく関数型言語処理系について" 1993年電子情報通信学会春季全国大会. (1993)

Takahiro Kanda：“关于基于 Supercombinator 的函数式语言处理系统”1993 年 IEICE 春季全国会议（1993）。

OYAMAGUCHI,M.: "The Reachability and Joimability Problems for Right-Ground Term-Rewriting Systims" Journal of Information Proceesing. 13. 347-354 (1990)

OYAMAGUCHI,M.：“正确基础术语重写系统的可达性和可玩性问题”信息处理杂志。