Ganesh Gopalakrishnan, Robert M. Kirby, Stephen
Siegel, Rajeev Thakur, William Gropp, Ewing Lusk, Bronis R. De
Supinski, Martin Schulz, and Greg Bronevetsky, Formal analysis of
MPI-based parallel programs, Communications of the ACM
54(12):82--91, December 2011.
The Message Passing Interface (MPI) is the
dominant programming model for high-performance computing.
Applications that use over 100,000 cores are currently running on
large HPC systems. Unfortunately, MPI usage presents a number of
correctness challenges that can result in wasted simulation cycles
and errant computations. In this article, we describe recently
developed formal and semi-formal approaches for verifying MPI
applications, highlighting the scalability/coverage tradeoffs taken
in them. We concentrate on MPI because of its ubiquity and because
similar issues will arise when developing verification techniques
for other performance-oriented concurrency APIs. We conclude with a
look at the inevitability of multiple concurrency models in future
parallel systems and point out why the HPC community urgently needs
increased participation from formal methods researchers.
@article{gopalakrishnan-etal:2011:cacm,
Address = {New York, NY, USA},
Author = {Gopalakrishnan, Ganesh and Kirby, Robert M. and Siegel, Stephen and Thakur, Rajeev and Gropp, William and Lusk, Ewing and De Supinski, Bronis R. and Schulz, Martin and Bronevetsky, Greg},
Doi = {10.1145/2043174.2043194},
Issn = {0001-0782},
Issue_Date = {December 2011},
Journal = {Communications of the ACM},
Month = dec,
Number = {12},
Numpages = {10},
Pages = {82--91},
Publisher = {ACM},
Title = {Formal analysis of {MPI}-based parallel programs},
Url = {http://doi.acm.org/10.1145/2043174.2043194},
Volume = {54},
Year = {2011}
}
