ISP (In-situ Partial Order): a dynamic verifier for MPI Programs
(For usage information, you may visit our tutorial page)
You may obtain the latest version of ISP (v0.3.1) as follows:
Please browse our group research Website for additional information.
[isp-v0.3.1.tar.gz]. This is ISP for installation on Linux and Mac OS/X.
This tarball is sufficient for running ISP on these operating systems.
The Graphical Explorer of MPI Programs (GEM)
contains links and installation instructions for our Eclipse Plug-in for ISP. This is useful
for all users wishing to extend the basic capabilities in the tarball with our work with the
Eclipse Parallel Tools Platform (PTP) .
GEM is developed for LINUX and MAC OS X.
[.iso] Ubuntu Live DVD ISO is a bootable disk image created for our recent tutorial presnetaion
at SC10 that may be burned onto a DVD,
allowing you to boot to a pre-configured Ubuntu 8.04 environment that has
ISP and GEM pre-installed. This is useful for users wanting to
experiment with ISP and GEM without making changes to their system.
To run ISP under Visual Studio, you must install the following three components:
All versions of ISP employ a Java GUI. This is the GUI invoked on the command line by ispUI.
This is a stand-alone program. For convenience, since we continually update ispUI, we provide you the
latest version in a JAR file. Simply replace the file ISP_INSTALL-DIR/bin/ispui.jar with the new one.
Documentation comes in the form of a user manual and many tests situated in a tests directory:
This page describes the tool ISP (``In-situ Partial Order'') developed
at the School of Computing, University of Utah.
Whether you are new to MPI or are an advanced user, ISP will help you
debug your programs, and graphically show you all the possible
send/receive matches, barrier synchronizations, etc.
For a given test harness, ISP guarantees soundness (i.e. every bug
reported is genuine) and completeness (i.e. it will find every bug in
its bug class). This is more than a standard debugger delivers. ISP's
search employs dynamic partial order reduction that allows it to consider
only the relevant process schedules.
Of course, ISP's debugging success depends on available resources, and many
reasonable pragmatic assumptions. The
general idea is to run ISP on a laptop / desktop and once the program is
debugged move it to a cluster machine. ISP has verified a 14KLOC program
in under five seconds on a laptop (e.g., the ParMETIS hypergraph partitioner
example in ISP's distribution).
A test harness is anything you set up for program testing - e.g., a
dataset to be processed using MPI. In many cases, verifying for one
harness is sufficient. ISP's bug classes are deadlocks, assertion
violations, and many types of MPI object leaks.
We want to see how ISP fares, whether it does not work as advertised,
or if it surprised you by finding a bug. Please drop us a note if any
of this happens. We will be very glad to help you use ISP. Our email
The user manual at the ISP download site fully explains all the tool
features. Credits for ISP go to many students who are fully
acknowledged in our user manual. Funding for ISP comes from Microsoft
ISP and its user manual may be downloaded from the above links.
Papers that explain ISP are available from our homepage:
In summary, the main features of ISP are the following:
Supports over 60 MPI 2.1 functions (see user manual for details)
Runs under Linux, MAC OS/X, and Windows.
The windows version has a Visual Studio plug-in that is also downloadable.
Tested with MPICH2, OpenMPI, and Microsoft MPI libraries.
Push-button formal verification of thousands of lines of MPI/C
code in seconds, for deadlocks, assertion violations, MPI object leaks,
and communication races (unexpected communication matches).
Comes with 100s of benchmark examples
Runs faster on multi-core machines, thanks to OpenMP based parallelization
We can also offer you the ISO image of a LiveCD that you can burn to
boot ISP on virtually any machine
It is well known that even an MPI program with five process, each
making five MPI calls each, has over 10 billion interleavings
(schedules). This is what bogs testing tools down -- they do not know
which interleavings matter, thus end up missing some interleavings
while pursuing others redundantly. ISP can compute relevant
interleavings dynamically, based on dependencies among MPI processes
using an algorithm called dynamic partial order reduction (or
DPOR). ISP's version of DPOR is called POE and is reported in our
However, even large MPI programs have only a few (often one) relevant
interleaving. For instance, we found that most tests of the 14 KLOC
program ParMETIS generates only one relevant interleaving. This
allowed ISP to finish on many ParMETIS tests in under five seconds on
an ordinary laptop.
ISP's Java GUI has tool tips and you can also watch the source lines
using the source window. The source window has tabbed and split views,
and you can further see the communication matches through color
codes. For Windows users, they get to use the cool Visual Studio
interface in addition to the Java GUI (assuming that they have
School of Computing * 50 S. Central Campus Dr. Rm. 3190 * Salt Lake City, UT
84112 * firstname.lastname@example.org