Implementing efficient dynamic formal verification methods for MPI programs

Sarvani Vakkalanka, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationRecent Advances in Parallel Virtual Machine and Message Passing Interface - 15th European PVM/MPI Users' Group Meeting, Proceedings
Number of pages9
StatePublished - 2008
Event15th European PVM/MPI Users' Group Meeting, EuroPVM/MPI 2008 - Dublin, Ireland
Duration: Sep 7 2008Sep 10 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5205 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other15th European PVM/MPI Users' Group Meeting, EuroPVM/MPI 2008

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Implementing efficient dynamic formal verification methods for MPI programs'. Together they form a unique fingerprint.

Cite this