Sciweavers

Share
FMICS
2007
Springer

An Approach to Formalization and Analysis of Message Passing Libraries

9 years 3 months ago
An Approach to Formalization and Analysis of Message Passing Libraries
Message passing using libraries implementing the Message Passing Interface (MPI) standard is the dominant communication mechanism in high performance computing (HPC) applications. Yet, the lack of an implementation independent formal semantics for MPI is a huge void that must be filled, especially given the fact that MPI will be implemented on novel hardware platforms in the near future. To help reason about programs that use MPI for communication, we have developed a formal TLA+ semantic definition of the point to point communication operations to augment the existing standard. The proposed semantics includes 42 MPI functions, including all 35 point to point operations, many of which have not been formally modeled previously. We also present a framework to extract models from SPMD-style C programs, so that designers may understand the semantics of MPI by exercising short, yet pithy, communication scenarios written in C/MPI. In this paper, we describe (i) the TLA+ MPI model features,...
Robert Palmer, Michael Delisi, Ganesh Gopalakrishn
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FMICS
Authors Robert Palmer, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby
Comments (0)
books