TY - GEN
T1 - Practical model-checking method for verifying correctness of MPI programs
AU - Pervez, Salman
AU - Gopalakrishnan, Ganesh
AU - Kirby, Robert M.
AU - Palmer, Robert
AU - Thakur, Rajeev
AU - Gropp, William
PY - 2007
Y1 - 2007
N2 - Formal 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 of 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.
AB - Formal 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 of 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.
UR - http://www.scopus.com/inward/record.url?scp=38449120055&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=38449120055&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-75416-9_46
DO - 10.1007/978-3-540-75416-9_46
M3 - Conference contribution
AN - SCOPUS:38449120055
SN - 9783540754152
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 344
EP - 353
BT - Recent Advances in Parallel Virtual Machine and Message Passing Interface - 14th European PVM/MPI Users' Group Meeting, Proceedings
PB - Springer
T2 - 14th European PVM/MPI Users' Group Meeting on Parallel Virtual Machine and Message Passing Interface
Y2 - 30 September 2007 through 3 October 2007
ER -