[Mpi-forum] MPI program verification tool

[Rajeev Thakur]

FYI... A tool for verifying MPI programs if anyone is interested in trying
out...


-------------------------------------
From: Ganesh <ganesh at cs.utah.edu>
Tue Feb 24 14:50:19 CST 2009
Subject: Availability of an MPI program verification tool

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