Argonne National Laboratory

Practical Model-Checking Mehtod for Verifying Correctness of MPI Programs

TitlePractical Model-Checking Mehtod for Verifying Correctness of MPI Programs
Publication TypeJournal
Year of Publication2007
AuthorsPervez, S, Gopalakrishnan, G, Kirby, RM, Palmer, R, Thakur, R, Gropp, WD
Other NumbersANL/MCS-P1440-0707
AbstractFormal program verification often requires creating a model of the program and running it through a model-checking tool. However, this model-creation step is itself error prone, tedious, and difficult for someone not familiar with formal verification. In this paper, we describe a tool for verifying correctness of MPI programs that does not require the creation of a model and instead works directly on the MPI program. Our tool uses the MPI profiling interface, PMPI, to trap MPI calls and hand over control to the MPI function execution to a scheduler. The scheduler verifies correctness of the program by executing all "relevant" interleavings of the program. The scheduler records an initial trace and replays its interleaving variants by using dynamic partial-order reduction. We describe the design and implementation of the tool and compare it with our previous work based on model checking.