如何开发并行程序并保证其正确性是一个研究热点。由于线程交错执行次序的不确定性,测试、调试工作不易覆盖所有执行情况、不易再现出错的执行,于是即使进行大量的测试、调试工作也不能完全保证程序是正确的。确定性并行技术保证程序在相同输入下的的所有执行是一致的并且能再现执行,因而能简化测试、调试工作。由于对并行确定性现存的认识并不统一,而且在指导测试、调试工作时存在缺陷,因此本文以一个基于共享消息通道的确定性并行编程模型为例,深入研究确定性的内涵、证明方法与以及如何更完善地指导测试、调试工作。为此,本文探讨并完成以下工作：1、提出一种能较好的统一认识不同确定性的角度本文指出各种确定性异同的核心因素在于：选择哪些程序点进行观察以及如何观察程序的状态。如何选择两者进行组合是主观的,对应了不同的确定性。而一个程序是否满足某确定性是客观的,取决于程序的语义和存储模型。当选定两个因素后,一个程序是确定的,当且仅当其任意两次执行到达指定程序点的能力相同(都能到达观察点或者都不能,两者是对立的),而且(若可以)到达观察点处时的状态观察起来相同。例如,最终点确定性指在程序执行的最终点,观察整个程序的状态。调试确定性指在程序执行的断点处,观察被调试线程相关的状态。2、提出一般性的确定性证明框架,将其应用于一个基于共享消息通道的SPMC模型上并证明模型的最终点确定性和调试确定性本文选定确定性并行编程模型SPMC (single-producer-multiple-consumer)作为确定性的研究对象。给出模型的抽象语法、程序状态定义和操作语义。基于此,定义并证明两种确定性分别用于指导测试、调试工作。由于同时理解形式化的复杂模型和其确定性证明并不容易,为此,本文的介绍思路是先研究一些足够简单的确定性并行编程模型,用它们展示证明模型确定性的普遍性框架,最后应用于SPMC模型的研究。总之,本文对确定性的认识更具普遍性而且对测试、调试工作的指导更完善,对确定性的证明有一定的普遍适用性。