Modeling Parallel MPI Programs in Petri Nets

摘要

The method of modeling concurrent programs is introduced. The basic framework of MPI programs are modeled by Petri net structures. On the one hand, the atomic actions of statements' execution are represented by the transition firing, on the other hand, properties such as Orphan Message, Lack of Message, Deadlock and Livelock Subnet of concurrent programs are analyzed and verified.