Title
Sound and Efficient Dynamic Verification of MPI Programs with Probe Non-determinism
Abstract
We consider the problem of verifying MPI programs that use MPI_Probe and MPI_Iprobe . Conventional testing tools, known to be inadequate in general, are even more so for testing MPI programs containing MPI probes. A few reasons are: (i) use of the MPI_ANY_SOURCE argument can make MPI probes non-deterministic, allowing them to match multiple senders, (ii) an MPI_Recv that follows an MPI probe need not match the MPI_Send that was successfully probed, and (iii) simply re-running the MPI program, even with schedule perturbations, is insufficient to bring out all behaviors of an MPI program using probes. We develop several key insights that help develop an elegant solution: prioritizing MPI processes during dynamic verification, handling non-determinism, and safe handling of probe loops. These solutions are incorporated into a new version of our dynamic verification tool ISP. ISP is now able to efficiently and soundly verify larger MPI examples, including MPI-BLAST and ADLB.
Year
DOI
Venue
2009
10.1007/978-3-642-03770-2_33
PVM/MPI
Keywords
Field
DocType
larger mpi example,probe non-determinism,mpi programs,mpi probe,dynamic verification,dynamic verification tool,probe loop,prioritizing mpi,mpi program,mpi probes non-deterministic,efficient dynamic verification,verifying mpi program,conventional testing tool
Computer science,Determinism,Parallel computing
Conference
Volume
ISSN
Citations 
5759
0302-9743
4
PageRank 
References 
Authors
0.51
14
6
Name
Order
Citations
PageRank
Vo Anh1124491.60
Sarvani Vakkalanka217711.14
Jason Williams340.51
Ganesh Gopalakrishnan41619130.11
Robert M. Kirby51443115.55
Rajeev Thakur63773251.09