VSL Publications

Formal Analysis of MPI-based Parallel Programs

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.
Related Links
  1. Version on publisher's web site
	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}

VSL | Publications