并行程序Petri网模型的结构性质

Structural Properties of Parallel Program's Petri Net Model

正确性是并行程序的基础,但是由于它的复杂性,其验证要比串行程序困难得多,因此有必要进行建模并研究其性质.从程序的角度出发,在将基于消息传递的并行程序转换为Petri网模型之后,证明了与并行正确的并行程序对应的Petri网模型应当满足的结构性质,包括强连通性、S-不变量、T-不变量、受控死锁性质以及守恒性,并举例说明了这些性质在并行程序验证中的应用.这些性质可用于并行程序的事前验证,而且避免了使用动态性质进行验证时的状态爆炸问题,从而提高并行程序设计和验证效率.同时这些方法具有良好的可推广性.

High-performance computing based on parallel programming is used in many fields, and correctness is the basis of parallel programs, but parallel programs are more difficult to verify than the sequential programs because of their complexity. Thus it is necessary to model them. Petri net is often used to model the parallel program, and most research work verifies the program from the point of view of Petri net. In this paper, the message-passing parallel program is transformed into Petri net model firstly, and the structural properties of it are studied on the program＇s ground. It is proved that for a concurrent correct parallel program＇s model, its Petri net model is strongly connected and satisfies controlled siphon property, each of its process-subnets is conservative, and each of its transitions belongs to a support of T-invariant. Two examples, one is a simple point-to-point non-blocking communication and the other is a producerconsumer system, are given to show the applications of these properties in verification of the parallel program. These properties can be used in beforehand verification of the parallel program, and this method avoids state explosion caused by verification with dynamical properties. Thus it can improve the efficiency of program design and verification. This method can be generalized easily.