@inproceedings{Vakkalanka2009,
  title = {Static-Analysis Assisted Dynamic Verification of {MPI} Waitany Programs (Poster Abstract)},
  author = {Sarvani Vakkalanka and Grzegorz Szubzda and Anh Vo 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/y6527920l7g62n26/},
  abstract = {It is well known that the number of schedules (interleavings) of a concurrent program grows exponentially with the number of processes. Our previous work has demonstrated the advantages of an MPI-specific dynamic partial order reduction (DPOR, [5]) algorithm called POE in a tool called ISP [1,2,3] in dramatically reducing the number of interleavings during formal dynamic verification. Higher degrees of interleaving reduction were achieved when the programs weredeterministic. In this work, we consider the problem of verifying MPI usingMPI_Waitany(and related operations wait/test some/all). Such programs potentially have a higher degree of non-determinism. For such programs, POE can become ineffective, as shown momentarily. To solve this problem, we employ static analysis (supported by ROSE [4]) in a supporting role to POE to determine the extent to which theoutparameters ofMPI_Waitanycan affect subsequent control flow statements. This informs ISPs scheduler to exert even more intelligent backtrack/replay control.},
  volume = {5759},
  series = {Lecture Notes in Computer Science},
  year = {2009},
  pages = {329--330},
  subject_collection = {Computer Science},
  doi = {10.1007/978-3-642-03770-2_43},
}