ISP ("In-situ Partial Order") is a tool for the formal verification of

MPI MPI or Mpi may refer to: Science and technology Biology and medicine * Magnetic particle imaging, an emerging non-invasive tomographic technique * Myocardial perfusion imaging, a nuclear medicine procedure that illustrates the function of the hear ...

programs developed within the School of Computing at the University of Utah. Like model checkers, such as

SPIN Spin or spinning most often refers to: * Spinning (textiles), the creation of yarn or thread by twisting fibers together, traditionally by hand spinning * Spin, the rotation of an object around a central axis * Spin (propaganda), an intentionally b ...

, ISP verifies the complete state space of a system for a set of safety properties. However, unlike model checkers, ISP performs ''code level verification''. This means that the tool verifies all ''relevant interleavings'' of a concurrent program by replaying the actual program code ''without'' building verification models. This idea was pioneered in a number of tools, notably by Godefroid, in his VeriSoft tool. Other recent tools of this genre include the Java Pathfinder, Microsoft's CHESS tool, and MODIST. Relevant interleavings are computed using a customized ''dynamic partial order reduction'' algorithm called ''POE''.Sarvani Vakkalanka, Ganesh Gopalakrishnan, and Robert M. Kirby, ''Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings,'' Computer Aided Verificatio
(CAV 2008)
pp. 66-79, LNCS 5123. ISP has been used to successfully verify up to 14,000 lines of MPI/C code for deadlocks and assertion violations. It currently supports over 60 MPI 2.1 functions, and has been tested with MPICH2,

OpenMPI Open MPI is a Message Passing Interface (MPI) library project combining technologies and resources from several other projects (FT-MPI, LA-MPI, LAM/MPI, and PACX-MPI). It is used by many TOP500 supercomputers including Roadrunner, which was th ...

, and Microsoft MPI libraries. ISP is available for download for

linux Linux ( or ) is a family of open-source Unix-like operating systems based on the Linux kernel, an operating system kernel first released on September 17, 1991, by Linus Torvalds. Linux is typically packaged as a Linux distribution, which ...

and

Mac OS X macOS (; previously OS X and originally Mac OS X) is a Unix operating system developed and marketed by Apple Inc. since 2001. It is the primary operating system for Apple's Mac (computer), Mac computers. Within the market of ...

; as a

Visual Studio Visual Studio is an integrated development environment (IDE) from Microsoft. It is used to develop computer programs including web site, websites, web apps, web services and mobile apps. Visual Studio uses Microsoft software development platfor ...

plugin for running under

Windows Windows is a group of several proprietary graphical operating system families developed and marketed by Microsoft. Each family caters to a certain sector of the computing industry. For example, Windows NT for consumers, Windows Server for serv ...

, and as an

Eclipse An eclipse is an astronomical event that occurs when an astronomical object or spacecraft is temporarily obscured, by passing into the shadow of another body or by having another body pass between it and the viewer. This alignment of three ce ...

plugin..

References

Anh Vo, Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, and Rajeev Thakur, ''Formal Verification of Practical MPI Programs,'
PPoPP 2009
Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, and Robert M. Kirby, ''Scheduling Considerations for Building Dynamic Verification Tools for MPI,'' Parallel and Distributed Systems - Testing and Debuggin
(PADTAD-VI)
Seattle, WA, July, 2008. Sarvani Vakkalanka, Michael DeLisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, ''Implementing Efficient Dynamic Formal Verification Methods for MPI Programs,'' Recent Advances in Parallel Virtual Machine and Message Passing Interfac
(EuroPVM/MPI 2008)
Dublin, Ireland, 2008, LNCS 5205, pp. 248–256. Sarvani Vakkalanka, Subodh Sharma, Ganesh Gopalakrishnan, and Robert M. Kirby, ''ISP: A Tool for Model Checking MPI Programs,'' Principles and Practices of Parallel Programmin
(PPoPP 2008)
Salt Lake City, February 2008, pp. 285–286. Salman Pervez, Robert Palmer, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, and William Gropp, ''Practical Model Checking Methods for Verifying Correctness of MPI Programs,'' Recent Advances in Parallel Virtual Machine and Message Passing Interfac
(PDF)
(EuroPVM/MPI), Paris, 344—353, LNCS 4757, France, September 30 - October 3, 2007

Cited By

''Combining symbolic execution with model checking to verify parallel numerical programs'',umass.ed
PDF
SF Siegel, A Mironova, GS Avrunin, LA Clarke - ACM Transactions on Software Engineering and Methodology - portal.acm.org Verification of halting properties for MPI programs using nonblocking operations - psu.ed
PDF
SF Siegel, GS Avrunin - Lecture Notes in Computer Science, 2007 - Springer
MPIWiz: Subgroup reproducible replay of MPI applications
R Xue, X Liu, M Wu, Z Guo, W Chen, W Zheng, Z Zhang, Geoffrey M. Voelker Tsinghua University, Microsoft Research Asia, University of Southern California San Diego - cs.ucsd.edu Dynamic testing of flow graph based parallel applications - epfl.c

B Schaeli, RD Hersch - Proceedings of the 6th workshop on Parallel and distributed Programming, 2008 - portal.acm.org Visual Debugging of MPI Applications - epfl.c
PDF
B Schaeli, A Al-Shabibi, RD Hersch - Proceedings of the 15th European PVM/MPI Users' Group …, 2008 - Springer

External links

ISP-Release
{{DEFAULTSORT:Isp Formal Verification Tool Parallel computing Application programming interfaces