MPI-Spin is an extension to the popular model checker Spin. It adds to Spin's input language a number of functions, types, and constants for modeling parallel programs that use the Message Passing Interface. MPI-Spin (but not Spin itself) is distributed under the GNU Public License. The author of MPI-Spin is Stephen F. Siegel.
Many of the difficulties involved in constructing correct
parallel programs arise from the fact that a parallel program
can behave differently when executed twice, even when the same
input is used for both executions. There are numerous sources
for such nondeterminism in MPI programs: the execution
steps from the processes may be interleaved differently in time;
a receive statement using MPI_ANY_SOURCE may select
a message from a different source; a call
to MPI_Waitany may select a different request for
completion; a message sent by a call to MPI_Send
may be buffered in one execution while in the other the sender
is blocked until the message can be delivered synchronously.
This nondeterminism makes effective testing and debugging of MPI
programs extremely difficult and is one of the main reasons that
many computational scientists are interested in formal
verification methods, such
as model
checking.
In theory, model checking techniques can be used to explore all nondeterministic choices in a parallel program and to verify that the program will satisfy user-specified correctness properties on all executions (or output a trace if a property can be violated). In practice, however, there are many barriers to the successful application of model checking to parallel programs, especially to MPI programs. Among these is the fact that most model checking tools operate on a model of the program, rather than on the program code itself. The model is typically expressed in a low-level modeling language which has no notion of MPI (or of many other common program constructs).
Promela, the input language for the widely-used model checker Spin, does contain a few simple primitives that correspond to basic message-passing operations, but these primitives are inadequate for expressing the complex notions that arise in many MPI programs, such as communication requests, posting, testing, canceling, and waiting on requests, persistent requests, and so on.
For this reason, I have developed MPI-Spin, an extension to Spin that supports many commonly-used MPI functions, constants, and types, including those used for nonblocking point-to-point communication. The syntax matches closely the syntax for the C bindings for MPI, which greatly simplifies the task of translating a C/MPI program into Promela.
By default, MPI-Spin checks a number of generic properties that
one would expect to hold in any correct MPI program. These
include (1) the program cannot deadlock, (2) there are never two
incomplete requests whose buffers intersect non-trivially, (3)
the total number of outstanding requests never exceeds a
specified bound, (4) when MPI_Finalize is called
there are no request objects allocated for and there are no
buffered messages destined for the calling process, and (5) the
size of an incoming message is never greater than the size of
the receive buffer. In addition, MPI-Spin can check
application-specific properties formulated in temporal logic.
Finally, MPI-Spin provides extensive support for symbolic
execution, making it possible to verify that a program behaves
correctly on all possible inputs. The papers
listed below describe MPI-Spin and its applications in more
detail, and the numerous examples are included with the
distribution.
The current version of MPI-Spin is version 1.1 of June 7, 2008. Installation instructions can be found in the MPI-Spin manual, which is also included in the distribution. MPI-Spin requires a very slighltly modified version of Spin, called Spin-M, which is also distributed below.
The term "MPI-Spin" refers only to the extension to Spin described above, and not to Spin itself.
MPI-Spin is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.
MPI-Spin is distributed in the hope that it will be useful, but without any warranty; without even the implied warranty of merchantability or fitness for a particular purpose. See the GNU Lesser General Public License for more details.