2026-07-26T16:45:04Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:1631 2024-03-06T11:08:14Z ddc:004 open_access

Verification of MPI-based Computations Siegel, Stephen F. MPI Spin model checking MPI-Spin symbolic execution 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Stephen F. Siegel 2008 Is Part Of Dagstuhl Seminar Proceedings, Volume 8332, Distributed Verification and Grid Computing (2008) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.08332.5 urn:nbn:de:0030-drops-16316 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08332.5 eng https://creativecommons.org/licenses/by/4.0/legalcode