VSL | Publications | Modeling MPI Programs for Verification

Title: Modeling MPI Programs for Verification

Authors: Stephen F. Siegel and George S. Avrunin

Abstract:

We investigate the application of finite-state verification techniques to parallel programs that employ the Message Passing Interface (MPI). We develop a formal model sufficient to represent programs that use a particular subset of MPI, and then prove a number of theorems about that model that ameliorate the state explosion problem or that show that certain properties of particular programs must necessarily hold. Most of these theorems require that the programs use neither \Mpianysource{} nor \Mpianytag. As an example, we show that for such programs, to verify freedom from deadlock, it suffices to consider only synchronous executions. While our motivation is to prove theorems that make finite-state verification techniques more tractable, the same results could also assist theorem-proving or other formal methods.

Appeared in:

Technical Report UM-CS-2004-75, Department of Computer Science, University of Massachusetts, 2004

BibTeX:

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

Download:

modelingmpi_tr_2004.pdf (full paper)

VSL | Publications