The Model And Correctness Verification Of Parallal Programs In Embedded Multi-core Environment

The high-performances computation which the base of parallel computing has been the third underpinning of scientific studies. High performances have been the top reason to use parallel programs while the correctness is the chiefly level. However, the tools in parallel programs analysis and design pay attentions only to one of the two aspects—verification or high-performance.The author gives a prototype of a tool which provides both performance analysis and correctness of the parallel programs from the design to analysis of the results. It's the Petri net that is better than other models to model MPI parallel program in comparison.Now, the parallel programs under the message passing is the most popular paradigm and MPI has become the accepted standard of this pattern. This thesis shows the features of MPI functions, and gives Petri net models and C language in which they are conclued, and presents the preliminary steps and methods to model MPI programs. It presents the concepts of statically executable, corrects parallel program, studies the liveness, strongly connectedness, reversibility, reachability and safeness of MPI parallel programs model and presents some reasons to disobey those properties. And it presents algorithms using the graph traversal, T-invariants and reachability graph/tree to correct those reasons and properties.Correctness is the basis for parallel program, but its verification is much more difficult than the serial program because of its complexity. So it is necessary to model and study its properties. The Petri net .model of the correct parallel programs often used into prove the properties of it including strong connectivity, s-invariant, t-invariant, controlled deadlock and conservation. These properties can verify parallel programs in advance, avoid the state explosion problem and improve the efficiency while it has good replicability.The verification by using the properties of Petri net without construction reachability tree first, avoid the state explosion problem and improve the efficiency of verification. Also this method prove the model properties from the program point, more in line with the principle of verification procedures, have good portability and replicability.In this paper, we study the methods of correctness Verification of parallal programs based on Petri net, which can be summarized as the following:1 Study the values of the MPI function and construct Petri net models and present basic steps and methods to model MPI programs for the most widely used parallel programming model based on message passing and programming standard-MPI and its embedded C language,2 Discuss the MPI parallel programming model-the dynamic properties (liveness, reachability, reversibility and safeness) and structural properties (strongly connectivity, boundedness, conservation and t-invariant) of MPInet.3 Give the verification algorithm of previous properties and present a verification algorithm and several examples for the common parallel programming errors.