Verification of MPI-based Computations

Author Stephen F. Siegel

Thumbnail PDF


  • Filesize: 123 kB
  • 3 pages

Document Identifiers

Author Details

Stephen F. Siegel

Cite AsGet BibTex

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)


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.
  • MPI
  • Spin
  • model checking
  • MPI-Spin
  • symbolic execution


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads