CAJ | 학술논문

文章研究并行编程模型的确定性与其证明方法。论文介绍了确定性并行的构成因素，并给出较统一的认识；基于这些认识，提出一种从一组操作语义中归纳而得的性质证得确定性的证明方法；以一个使用共享消息通道的确定性并行编程模型为例，形式化该编程模型并证明其确定性。本文弥补了对确定性已有认识的不足，能更完善地指导测试与调试，且证明方法有一定的适用性。
문장연구병행편정모형적학정성여기증명방법。논문개소료학정성병행적구성인소，병급출교통일적인식；기우저사인식，제출일충종일조조작어의중귀납이득적성질증득학정성적증명방법；이일개사용공향소식통도적학정성병행편정모형위례，형식화해편정모형병증명기학정성。본문미보료대학정성이유인식적불족，능경완선지지도측시여조시，차증명방법유일정적괄용성。
The paper studies the determinism of parallel programming model and its proofing method. In brief, 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.