ISP (In-situ Partial Order): a dynamic verifier for MPI Programs

ISP Architecture

ISP GUI

(For usage information, you may visit our tutorial page) DOWNLOAD INFO You may obtain the latest version of ISP (v0.3.1) as follows: Download [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: [ISP Visual Studio Plugin.msi] Visit either the HPC Pack 2008 SDK w/ SP1 website OR the MS Compute Cluster Pack SDK website to download and install a Windows MPI environment. Java (JRE 6u14) [ispui.JAR] 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: [.pdf] of the ISP User Manual Website of ISP examples Please browse our group research Website for additional information.

 

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 is isp-dev@cs.utah.edu

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 and NSF.

ISP and its user manual may be downloaded from the above links. Papers that explain ISP are available from our homepage: RELATED PUBLICATIONS.

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
• BSD License
• We can also offer you the ISO image of a LiveCD that you can burn to boot ISP on virtually any machine

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 installed Java).