TY - GEN
T1 - Implementing efficient dynamic formal verification methods for MPI programs
AU - Vakkalanka, Sarvani
AU - Delisi, Michael
AU - Gopalakrishnan, Ganesh
AU - Kirby, Robert M.
AU - Thakur, Rajeev
AU - Gropp, William
N1 - Funding Information:
Supported in part by NSF CNS-00509379, Microsoft HPC Institutes Program, and the Mathematical, Information, and Computational Science Division subprogram of the Office of Advanced Scientific Computing Research, Office of Science, U.S. Department of Energy, under Contract DE-AC02-06CH11357.
PY - 2008
Y1 - 2008
N2 - We examine the problem of formally verifying MPI programs for safety properties through an efficient dynamic (runtime) method in which the processes of a given MPI program are executed under the control of an interleaving scheduler. To ensure full coverage for given input test data, the algorithm must take into consideration MPI's out-of-order completion semantics. The algorithm must also ensure that nondeterministic constructs (e.g., MPI wildcard receive matches) are executed in all possible ways. Our new algorithm rewrites wildcard receives to specific receives, one for each sender that can potentially match with the receive. It then recursively explores each case of the specific receives. The list of potential senders matching a receive is determined through a runtime algorithm that exploits MPI's operation ordering semantics. Our verification tool ISP that incorporates this algorithm efficiently verifies several programs and finds bugs missed by existing informal verification tools.
AB - We examine the problem of formally verifying MPI programs for safety properties through an efficient dynamic (runtime) method in which the processes of a given MPI program are executed under the control of an interleaving scheduler. To ensure full coverage for given input test data, the algorithm must take into consideration MPI's out-of-order completion semantics. The algorithm must also ensure that nondeterministic constructs (e.g., MPI wildcard receive matches) are executed in all possible ways. Our new algorithm rewrites wildcard receives to specific receives, one for each sender that can potentially match with the receive. It then recursively explores each case of the specific receives. The list of potential senders matching a receive is determined through a runtime algorithm that exploits MPI's operation ordering semantics. Our verification tool ISP that incorporates this algorithm efficiently verifies several programs and finds bugs missed by existing informal verification tools.
UR - http://www.scopus.com/inward/record.url?scp=56549113655&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=56549113655&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-87475-1_34
DO - 10.1007/978-3-540-87475-1_34
M3 - Conference contribution
AN - SCOPUS:56549113655
SN - 3540874747
SN - 9783540874744
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 248
EP - 256
BT - Recent Advances in Parallel Virtual Machine and Message Passing Interface - 15th European PVM/MPI Users' Group Meeting, Proceedings
T2 - 15th European PVM/MPI Users' Group Meeting, EuroPVM/MPI 2008
Y2 - 7 September 2008 through 10 September 2008
ER -