DROPS

Document

Verification of MPI-based Computations

Authors: Stephen F. Siegel

Published in: Dagstuhl Seminar Proceedings, Volume 8332, Distributed Verification and Grid Computing (2008)

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.

Cite as

Stephen F. Siegel. Verification of MPI-based Computations. In Distributed Verification and Grid Computing. Dagstuhl Seminar Proceedings, Volume 8332, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{siegel:DagSemProc.08332.5,
  author =	{Siegel, Stephen F.},
  title =	{{Verification of MPI-based Computations}},
  booktitle =	{Distributed Verification and Grid Computing},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8332},
  editor =	{Henri E. Bal and Lubos Brim and Martin Leucker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.5},
  URN =		{urn:nbn:de:0030-drops-16316},
  doi =		{10.4230/DagSemProc.08332.5},
  annote =	{Keywords: MPI, Spin, model checking, MPI-Spin, symbolic execution}
}

Search Results

Documents authored by Siegel, Stephen F.

Verification of MPI-based Computations

Abstract

Cite as

Thanks for your feedback!

Could not send message