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
ABSTRACT: MPI programming at scale is error prone, with current debugging
tools offering limited help.
We present complementary tools that
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.
Ganesh Gopalakrishnan - University of Utah
Bronis de Supinski - Lawrence Livermore National Laboratory