License
When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-16316
URL: http://drops.dagstuhl.de/opus/volltexte/2008/1631/
Go to the corresponding Portal


Siegel, Stephen F.

Verification of MPI-based Computations

pdf-format:
Document 1.pdf (124 KB)


Abstract

The Message Passing Interface is a widely-used parallel programming model and is the effective standard for high-performance scientific computing. It has also been used in parallel model checkers, such as DiVinE. In this talk we discuss the verification problem for MPI-based programs. The MPI is quite large and the semantics complex. Nevertheless, by restricting to a certain subset of MPI, the verification problem becomes tractable. Certain constructs outside of this subset (such as wildcard receives) can lead to a rapid blowup in the number of states, but MPI-specific reduction techniques have led to progress in combating this state explosion. Specifying correctness is another challenge. One approach is to use a trusted sequential version of the program as the specification, and use model checking and symbolic execution techniques to establish the functional equivalence of the sequential and parallel versions. This approach is supported in extsc{Mpi-Spin}, an extension to the model checker extsc{Spin} for verifying MPI-based programs.

BibTeX - Entry

@InProceedings{siegel:DSP:2008:1631,
  author =	{Stephen F. Siegel},
  title =	{Verification of MPI-based Computations},
  booktitle =	{Distributed Verification and Grid Computing },
  year =	{2008},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  number =	{08332},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2008/1631},
  annote =	{Keywords: MPI, Spin, model checking, MPI-Spin, symbolic execution}
}

Keywords: MPI, Spin, model checking, MPI-Spin, symbolic execution
Seminar: 08332 - Distributed Verification and Grid Computing
Issue Date: 2008
Date of publication: 30.10.2008


DROPS-Home | Fulltext Search | Imprint Published by LZI