SC is the International Conference for
 High Performnance Computing, Networking, Storage and Analysis

SCHEDULE: NOV 13-19, 2010

A Scalable and Distributed Dynamic Formal Verifier for MPI Programs

SESSION: Parallel Analysis Tools


TIME: 3:30PM - 4:00PM

SESSION CHAIR: Martin Schulz

AUTHOR(S):Anh Vo, Sriram Aananthakrishnan, Ganesh Gopalakrishnan, Greg Bronevetsky, Bronis R. de Supinski, Martin Schulz


Standard testing methods of MPI programs do not guarantee coverage of all non-deterministic interactions (e.g., wildcard-receives). Programs tested by these methods can have untested paths (bugs) that may become manifest unexpectedly. Previous formal dynamic verifiers cover the space of non-determinism but do not scale, even for small applications. We present DAMPI, the first dynamic analyzer for MPI programs that guarantees scalable coverage of the space of non-determinism through a decentralized algorithm based on Lamport-clocks. DAMPI computes alternative non-deterministic matches and enforces them in subsequent program replays. To avoid interleaving explosion, DAMPI employs heuristics to focus coverage to regions of interest. We show that DAMPI can detect deadlocks and resource-leaks in real applications. Our results on a wide range of applications using over a thousand processes, which is an order of magnitude larger than any previously reported results for MPI dynamic verification tools, demonstrate that DAMPI provides scalable, user-configurable testing coverage.

Chair/Author Details:

Martin Schulz (Chair) - Lawrence Livermore National Laboratory

Anh Vo - University of Utah

Sriram Aananthakrishnan - University of Utah

Ganesh Gopalakrishnan - University of Utah

Greg Bronevetsky - Lawrence Livermore National Laboratory

Bronis R. de Supinski - Lawrence Livermore National Laboratory

Martin Schulz - Lawrence Livermore National Laboratory

Add to iCal  Click here to download .ics calendar file

Add to Outlook  Click here to download .vcs calendar file

Add to Google Calendarss  Click here to add event to your Google Calendar

The full paper can be found in the ACM Digital Library and IEEE Computer Society

   Sponsors    IEEE    ACM