On this page... (hide)
- 1. Overview
- 2. Background
- 3. Documents
- 4. License
1. Overview
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.
2. Background
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. Download and installation
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 slightly modified version of Spin, called Spin-M, which is also distributed below.
- mpi-spin.tgz: source code, examples, documentation
- Spin-M: the modified version of Spin
3. Documents
- MPI-Spin Tutorial
- Using MPI-Spin to Model Check MPI Programs with Nonblocking Communication, Stephen F. Siegel, EuroPVM/MPI 2006. A short introduction to MPI-Spin.
- Model Checking Nonblocking MPI Programs, Stephen F. Siegel, VMCAI 2007. A more detailed exposition concentrating on the modeling method and theoretical background.
- MPI-Spin Version 1.1: A User's Manual, Stephen F. Siegel. This is the latest version of the user's manual. The version of the manual included in the source file tar ball may be older than this one.
- Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs, Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, Lori A. Clarke, ISSTA 2006. This paper describes a method to verify that a parallel program always computes the same result as a sequential version of that program. This method is supported in MPI-Spin through the symbolic type and operations.
- Combining Symbolic Execution with Model Checking to Verify Parallel Numerical Programs, Stephen F. Siegel, Anastasia Mironova, George S. Avrunin, Lori A. Clarke, ACM TOSEM, 2008. A more in-depth treatment of the material above.
- A Case Study in the Use of Model Checking to Verify Parallel Scientific Software?, Stephen F. Siegel, Samuel E. Moelius III, and Louis F. Rossi, Technical Report UD-CIS-2007-343. An application of MPI-Spin to a complex vortex-method simulation system.
- Analyzing BlobFlow: A Case Study Using Model Checking to Verify Parallel Scientific Software?, Stephen F. Siegel and Louis F. Rossi, EuroPVM/MPI 2008. A shorter version of above.
4. License
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.