Structural properties of parallel program's Petri net model

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 producer-consumer 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.