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,...

• Type: Conference
• Year: 2007
• Where: FMICS
• Authors: Robert Palmer, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby
• Keywords: FMICS 2007, Formal Semantic, MPI Functions, TLA+ MPI Model