Making ISP (Dynamic Verification for MPI) Practical

Опубликовано 6 сентября 2016, 18:39

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.