contributed articles

doI: 10.1145/2043174.2043194

The goal is reliable parallel simulations, helping scientists understand nature, from how foams compress to how ribosomes construct proteins.

BY GaneSH GoPaLaKRISHnan, RoBeRt m. KIRBY,
StePHen SIeGeL, RaJeeV tHaKuR, WILLIam GRoPP,
e WInG LuSK, BRonIS R. de SuPInSKI, maRtIn SCHuLz,
and GReG BRoneVetSKY
formal
analysis of
mPI-based
Parallel
Programs

through near-universal adoption. MPI
development continues, with MPI- 2. 2
released in 2009 and MPI 3.0 expected
in 2012. The standard is published on
the Web21 and as a book, along with
several other books based on it; see, for
example, Gropp et al. 13 and Pacheco. 26
Implementations are available in open
source from MPICH222 and Open MPI25
from software vendors and from every
vendor of HPC systems. MPI is widely
cited; Google Scholar recently returned
39,600 hits for the term “+MPI +Mes-
sage Passing Interface.”
MPI is designed to support highly
scalable computing applications us-
ing more than 100,000 cores on, say,
the IBM Blue Gene/P (see Figure 1) and
Cray XT5. Many MPI programs repre-
sent dozens, if not hundreds, of person-
years of development, including cali-
bration for accuracy and performance
tuning. Scientists and engineers world-
wide use MPI in thousands of applica-
tions, including in investigations of al-
ternate-energy sources and in weather
simulation. For HPC computing, MPI
is by far the dominant programming
model; most (at some centers, all) ap-
plications running on supercomputers
use MPI. Many application developers
for exascale systems15 regard support
for MPI as a requirement.

Still, the MPI debugging methods available to these developers are typically wasteful and ultimately unreliable. Existing MPI testing tools seldom provide coverage guarantees, examin-

Mos T ParaLLeL CoMPUTiNG applications in high-performance computing use the Message Passing Interface (MPI) API. Given the fundamental importance of parallel computing to science and engineering research, application correctness is paramount. MPI was originally developed around 1993 by the MPI Forum, a group of vendors, parallel programming researchers, and computational scientists. however, the document defining the standard is not issued by an official standards organization but has become a de facto standard

key insights

addressing the challenges of distributed
systems, debugging necessitates
collaboration between HPC and formal
verification.
along with HPC, distributed computing
based on communication libraries is
going mainstream in the commodity
world, two communities that must look
to learn and benefit from one another.
Catastrophic disruption of programmer
productivity can be avoided through
formal verification tools that handle
problems of scale, enhance coverage
by avoiding redundant searches, and
decrease false-alarm rates through
more precise analysis.