VSL Publications

Verification of MPI-based Computations

Cite
Stephen F. Siegel, Verification of MPI-based Computations. Distributed Verification and Grid Computing, Dagstuhl Seminar Proceedings 08332, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, Dagstuhl, Germany, 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 MPI-Spin, an extension to the model checker Spin for verifying MPI-based programs.
Downloads
  1. Paper on publisher's web site
  2. verification_dagstuhl_2008.pdf (preprint)
BibTeX 
@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}
}
VSL | Publications