Title: Verification of MPI-based Software for Scientific Computation
Authors: Stephen F. Siegel and George S. Avrunin
Abstract:
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.
Appeared 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
BibTeX:
@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
}
Download: