@inproceedings{Vo2009,
  title = {Sound and Efficient Dynamic Verification of {MPI} Programs with Probe Non-determinism},
  author = {Anh Vo and Sarvani Vakkalanka and Jason Williams and Ganesh Gopalakrishnan and Robert M. Kirby and Rajeev Thakur},
  booktitle = {Recent Advances in Parallel Virtual Machine and Message Passing Interface},
  publisher = {Springer Berlin / Heidelberg},
  issn = {0302-9743 (Print) 1611-3349 (Online)},
  isbn = {978-3-642-03769-6},
  url = {http://www.springerlink.com/content/j8x410x17926711q/},
  abstract = {We consider the problem of verifying MPI programs that useMPI_ProbeandMPI_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 theMPI_ANY_SOURCEargument can make MPI probes non-deterministic, allowing them to match multiple senders, (ii) anMPI_Recvthat follows an MPI probe need not match theMPI_Sendthat 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.},
  volume = {5759},
  series = {Lecture Notes in Computer Science},
  year = {2009},
  pages = {271--281},
  subject_collection = {Computer Science},
  doi = {10.1007/978-3-642-03770-2_33},
}