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

SCHEDULE: NOV 13-19, 2010

Scalable Dynamic Formal Verification and Correctness Checking of MPI Applications

SESSION: M06: Scalable Dynamic Formal Verification and Correctness Checking of MPI Applications

EVENT TYPE: Tutorial

TIME: 8:30AM - 12:00PM

Presenter(s):Ganesh Gopalakrishnan, Bronis de Supinski, Matthias Muller


MPI programming at scale is error prone, with current debugging tools offering limited help. We present complementary tools that intuitively report deadlocks, messaging errors, and resource leaks. No single technique can offer thorough coverage of bugs and scalability: therefore we present two classes of tools focusing on each. Marmot and Umpire are dynamic correctness checkers that achieve high scalability, intercepting and analyzing MPI calls produced under natural schedules induced by large clusters. ISP is a dynamic tool that achieves guaranteed coverage of non-deterministic matches by enforcing relevant interleavings. It scales more than conventional model checkers by eliminating semantically equivalent interleavings. We are integrating our tools within the Eclipse Parallel Tools Platform (PTP) to make debugging intuitive and coordinated. We will also present promising new developments: MUST, enhancing the coverage of Umpire and Marmot, and DMA, redesigning ISP to achieve scalability. Our demo-laden tutorial will significantly benefit anyone who uses MPI.

Chair/Presenter Details:

Ganesh Gopalakrishnan - University of Utah

Bronis de Supinski - Lawrence Livermore National Laboratory

Matthias Muller - Technical University Dresden

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

   Sponsors    IEEE    ACM