公平消息传递并行程序设计的Petri网方法

Fair Message-passing Parallel Program Design with Petri Net

公平性是并行程序正确的主要标准之一,但是并行程序执行的不确定性导致公平性验证较为困难。针对消息传递模式的并行程序,在建立相应Petri网模型的基础上,首先证明了并行程序的公平性与其Petri网模型的公平性之间的关系,然后提出了利用T-不变量判断并行程序公平性,以及通过添加控制库所实现并行程序公平的算法,最后指出了将改造后的模型转换为公平并行程序的方法,并用一个实例进行了验证。

Fairness is one of the main correct criterions of parallel programs, but the uncertainty of its execution leads to difficult verification. On the basis of modeling the message-passing parallel program with Petri nets, it was proved that the Petri net model of a fair parallel program is fair and has a unique support of T-invariant. In succession, the algorithm to discover the starvation, and ensure the fairness by appending control places was given. Finally, the transforming method from the reconstructed Petri net to a fair parallel program was discussed, and an example composed of two consumers and one producer was used to demonstrate the power of the method. This method can be used during the algorithm design period to improve programming efficiency.