The Model And Verification Of MPI Parallal Programs Based On Petri Net

The high-performance computation based on parallel computing has been the third underpinning of the human being's scientific study. High performance is the first reason to use parallel programs, and correctness is the chiefly condition to use it. However, the tools which were used to aid parallel programs design and analysis pay attentions only to one of the two aspects--high-performance or correctness.The author presents a prototype of a tool that provides both performance analysis and verification of the parallel programs from design running to analysis of results. Also, this thesis presents the principles and methods to design CAPSE tools founded on the traits of previous tools. We think the Petri net is superior over other models to model the MPI parallel programs by comparison.The parallel program based on message passing is the most popular paradigm now, and MPI has become the most popularly accepted standard of this pattern. This thesis studies the features of the MPI functions, and gives the Petri net models of them and C language in which they are nested, and presents the preliminary steps and method to model an MPI program. We present the concepts of statically executable and concurrently correct parallel program, and study the safeness strongly connectedness reachability reversibility and liveness of MPI parallel program's model MPInet, and present some possible reasons to disobey these properties, for instance, lack-of-sending message orphan message non-match message deadlock (including inconsistency deadlock and circular deadlock) livelock and so on. At the same time, we present algorithms using the graph traversal and reachability graph/tree T-invariants to verify these properties and reasons.