并行编程模型的确定性的证明方法及其应用

The Proofing Method for the Deterministic Parallel Programming Model and Its Application

文章研究并行编程模型的确定性与其证明方法。论文介绍了确定性并行的构成因素,并给出较统一的认识;基于这些认识,提出一种从一组操作语义中归纳而得的性质证得确定性的证明方法;以一个使用共享消息通道的确定性并行编程模型为例,形式化该编程模型并证明其确定性。本文弥补了对确定性已有认识的不足,能更完善地指导测试与调试,且证明方法有一定的适用性。

The paper studies the determinism of parallel programming model and its prootlng memoo, m Drier, the paper introduces the components of deterministic parallelism and gives a general unified perspective. Based on the perspective, the paper presents a method for proving the determinism via a group of properties which are summarized out from operational semantics. And the paper takes a shared-message-channel-based parallel programming model, as the example to formalize the model and prove its determinism. This paper overcomes the shortcomings of existing research on determinism, can perfectly instruct testing and debugging work. Furthermore, the proofing method has certain suitability.