Verification of MPI programs via compilation into Petri nets

We study parallel Java programs that use an implementation of the MPI (Message-Passing Interface) standard MPJ with the goal of proving their liveness that can be formulated in a simplified form as absence of deadlocks. In the process of parsing a given program, we create the program MPI communication model in the form of a Petri net. A static code analyzer has been developed; among its current version limitations are: point-to-point MPI communication functions Send and Recv are considered; models are obtained for a given number of processes; unfolding of loops is implemented for loops with the number of repetition known on the compilation stage. The obtained Petri net model of the program MPI communication is analyzed by Tina modeling system using the state space and symbolic state space techniques; application of the symbolic state space tool tedd for finding deadlocks yields manifold speed-up that makes feasible analyzing big software systems. The results are illustrated with a case study that includes both sets of program examples: deadlock free and containing deadlocks. The verification kit is supplied with generators of MPJ programs for testing and benchmarking the analyzer on big programs with pre-defined patterns of communications such as a chain and a loop of a given size, etc.