VSL | Publications | Analysis of MPI Programs

Title: Analysis of MPI Programs

Authors: Stephen F. Siegel and George S. Avrunin

Abstract:

We investigate the application of formal verification techniques to parallel programs that employ the Message Passing Interface (MPI). We develop a formal model of a subset of MPI, and then prove a number of theorems about that model that ameliorate or eliminate altogether the state explosion problem. As an example, we show that if one wishes to verify freedom from deadlock, it suffices to consider only synchronous executions.

Appeared in:

Technical Report UM-CS-2003-036, Department of Computer Science, University of Massachusetts, 2003

BibTeX: 

@TechReport{siegel-avrunin:2004:mpi_tr,
  author = "Stephen F. Siegel and George S. Avrunin"
  title = "Analysis of {MPI} Programs"
  institution = "Department of Computer Science, University of Massachusetts",
  year = 2003,
  number = "UM-CS-2003-36"
}

Download:

VSL | Publications