University of Utah

Search
School of Computing

  

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:
  • [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:
Please browse our group research Website for additional information.

 

OVERVIEW:

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 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:

DETAILS:

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 papers.

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


School of Computing * 50 S. Central Campus Dr. Rm. 3190 * Salt Lake City, UT 84112 * isp-dev@cs.utah.edu
Disclaimer

HomePeopleResearchAdmissionsSite Map