Practical model-checking method for verifying correctness of MPI programs

Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Robert Palmer, Rajeev Thakur, William Gropp

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

Abstract

Formal program verification often requires creating a model of the program and running it through a model-checking tool. However, this model-creation step is itself error prone, tedious, and difficult for someone not familiar with formal verification. In this paper, we describe a tool for verifying correctness of MPI programs that does not require the creation of a model and instead works directly on the MPI program. Our tool uses the MPI profiling interface, PMPI, to trap MPI calls and hand over control of the MPI function execution to a scheduler. The scheduler verifies correctness of the program by executing all "relevant" interleavings of the program. The scheduler records an initial trace and replays its interleaving variants by using dynamic partial-order reduction. We describe the design and implementation of the tool and compare it with our previous work based on model checking.

Original languageEnglish (US)
Title of host publicationRecent Advances in Parallel Virtual Machine and Message Passing Interface - 14th European PVM/MPI Users' Group Meeting, Proceedings
PublisherSpringer
Pages344-353
Number of pages10
ISBN (Print)9783540754152
DOIs
StatePublished - Jan 1 2007
Externally publishedYes
Event14th European PVM/MPI Users' Group Meeting on Parallel Virtual Machine and Message Passing Interface - Paris, France
Duration: Sep 30 2007Oct 3 2007

Publication series

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

Other

Other14th European PVM/MPI Users' Group Meeting on Parallel Virtual Machine and Message Passing Interface
Country/TerritoryFrance
CityParis
Period9/30/0710/3/07

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Practical model-checking method for verifying correctness of MPI programs'. Together they form a unique fingerprint.

Cite this