Stephen F. Siegel and George S. Avrunin, Verification of
MPI-based Software for Scientific Computation. In Graf, S.,
Mounier, L., eds.:
Model Checking Software: 11th International SPIN
Workshop, Barcelona, Spain, April 1-3, 2004,
Proceedings.
Lecture
Notes in Computer Science 2989,
Springer-Verlag (2004) 286–303.
We explore issues related to the application of finite-state
verification techniques to scientific computation software
employing the widely-used Message-Passing Interface (MPI).
Many of the features of MPI that are important for programmers
present significant difficulties for model checking. In this
paper, we examine a small parallel program that computes the
evolution in time of a discretized function u defined
on a 2-dimensional domain and governed by the diffusion
equation. Although this example is simple, it makes use of
many of the problematic features of MPI. We discuss the
modeling of these features and use Spin and INCA to verify
several correctness properties for various configurations of
this program. Finally, we describe some general theorems that
can be used to justify simplifications in finite-state models
of MPI programs and that guarantee certain properties must
hold for any program using only a particular subset of MPI.
@InProceedings{siegel-avrunin:2004:diffusion,
author = "Stephen F. Siegel and George S. Avrunin",
title = "Verification of {MPI}-based software for scientific computation",
crossref = {spin2004},
pages = {286--303}
}
@Proceedings{spin2004,
editor = "Susanne Graf and Laurent Mounier",
title = "Model Checking Software: 11th International {SPIN} Workshop, Barcelona, Spain, April 1--3, 2004, Proceedings",
booktitle = "Model Checking Software: 11th International {SPIN} Workshop, Barcelona, Spain, April 1--3, 2004, Proceedings",
publisher = "Springer-Verlag",
series = {LNCS},
volume = 2989,
year = 2004
}
