[mpich-discuss] Availability of an MPI program verification tool

[Ganesh]

Hi,

The ISP (``In-situ Partial Order'') Verification tool for MPI is now 
available for download. ISP push-button verifies MPI  C programs and 
presents intuitive error-traces as well as other info (e.g. the 
completes-before relation showing how MPI operations may finish) using 
two graphical user interfaces: a Java based one, and a Visual Studio 
based one. Other features of ISP that makes it helpful in learning / 
teaching MPI as well as debugging MPI programs in parallel programming 
projects include:

   * Runs under Linux, MAC OS/X, and Windows.
   * 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.
   * 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 any machine, and teach ISP under a Virtual Machine
   * BSD License

The user manual at the ISP download site fully explains all the tool 
features, and also the email for contact (isp-dev at cs.utah.edu)

http://www.cs.utah.edu/formal_verification/ISP-release

Credits for ISP go to many students who are fully acknowledged in our 
user manual. Funding for ISP comes from Microsoft and NSF.

Papers that explain ISP are available from our homepage (leave out 
/ISP-release above)

Ganesh Gopalakrishnan
School of Computing, University of Utah
--