Formal analysis for MPI-based high performance computing software.

摘要

Model checking has been applied to concurrent system paradigms such as cache coherence protocols, device drivers, and threads based programming with great success in finding errors that are otherwise difficult to diagnose and remove. The primary reasons for this success are: (i) the set of communication idioms, used in a given paradigm, is relatively small and well understood by the model checking tools, (ii) model checking examines all interesting execution traces in an automatic and systematic way, and (iii) the properties being checked are amenable to model checking analysis.; In this dissertation, the application of model checking analysis to MPI-based parallel programs, which have a rich set of communication idioms available in the form of a communication library, is examined. To facilitate model checking analysis, formal model of the MPI 1.1 standard is proposed using the Temporal Logic of Actions (TLA+). This model serves as an executable reference for answering questions about how the various operations may interact and describes the communication idioms using a formal logic notation. Using the model, one can pose pithy litmus tests with respect to the MPI standard that are analyzed using TLC, a model checker for the TLA+ language.; A representative subset of communication primitives are chosen (one send, receive, wait, and test operation, along with barrier) and the independence characteristics of these operations are shown. Leveraging this independence information, this dissertation presents a dynamic partial-order reduction algorithm to facilitate scalability in model checker based reasoning. The partial-order reduction algorithm and this subset of communication primitives has been implemented in a prototype model checker called MPIC.; To facilitate litmus test based examination of MPI-based C programs, a model extraction framework is presented. This framework is integrated with the Microsoft Visual Studio development environment, combining TLA+ program models with the TLA+ MPI model. Initial results are encouraging as intricate scenarios for a small number of process can be examined. The framework also creates MPIC models, allowing for the examination of somewhat larger programs in a limited setting.