Modeling MPI programs for verification

Abstract. We investigate the application of formal 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 MPI_ANY_SOURCE nor MPI_ANY_TAG. 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. 1