Making ISP (Dynamic Verification for MPI) Practical

March 30, 2009
Ganesh Gopalakrishnan | University of Utah

Scientists who work on a whole range of high performance computing problems (e.g. earthquake simulation) employ the Message Passing Interface (MPI) as their lingua franca. Unfortunately, they are ill-equipped to grapple with concurrency in this domain through existing debuggers. Given the impracticality of creating formal models from the code, and given the ineffectiveness of static analysis other than in a supporting role, we developed a dynamic approach (inspired by Godefroid’s Verisoft and his work with Flanagan on Dynamic Partial Order Reduction). Given the weak completion order of invoked MPI operations, and the cluster-to-cluster variation of runtime buffering and runtime scheduling, engineering our ideas into a practical push-button model checker for MPI C programs took many innovations. The resulting tool ISP is being downloaded, has implementations for Windows, Linux, and Mac, supporting multiple MPI libraries, and comes with a Visual Studio plug-in as well as a Java GUI. One of our best results is the model checking of a 14KLOC hypergraph partitioner for one test harness in less than five seconds on a laptop. Our talk will detail these points, demonstrate ISP (www.cs.utah.edu/formal_verification/ISP-release), and describe one pursuit in detail: can the addition of buffering increase deadlocks (called slack inelasticity). Our group of 12 students is actively developing two other dynamic verification tools, one for thread programs (tool called Inspect by Yu Yang) and the other for a newly proposed multicore communications API (tool called MCC by Subodh Sharma). This tale of three DPOR incarnations will be our closing thought.

Speaker Details

Ganesh Gopalakrishnan has been on faculty at the University of Utah, School of Computing, since 1986, working on hardware modeling, self-timed circuits, pipelined processors, cache coherence, and memory consistency. His efforts beginning 2003 have a dominant focus on putting dynamic verification tools in the hands of users who grapple with concurrency. He is teaching a class on multi-core computing, and hopes to educate undergraduates in the value of such tools (including CHESS). He also has a student building an FPGA with nine MIPS cores talking the MCAPI protocol on a fabric also on hardware. His efforts have immensely benefited from advice received from researchers at IBM, Intel, FreeScale, and Microsoft. His funding sources are Microsoft, NSF, and SRC.