On this page... (hide)

  1. 1. Overview
  2. 2. Background
  3. 3. Documents
  4. 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.

3.  Documents

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.