VSL Publications

Analysis of MPI Programs

Stephen F. Siegel and George S. Avrunin, Analysis of MPI Programs, Technical Report UM-CS-2003-036, Department of Computer Science, University of Massachusetts, 2003
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.
  1. analysismpi_tr_2003.pdf (full paper)
  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"

VSL | Publications