Model Checking Nonblocking MPI Programs

by Stephen F. Siegel

Abstract. This paper explores a way to apply model checking techniques to parallel programs that use the \emph{nonblocking} primitives of the Message Passing Interface (MPI). The method has been implemented as an extension to the model checker \spin{} called \mpispin. It has been applied to 17 examples from a widely-used textbook on MPI. Many correctness properties of these examples were verified and in two cases nontrivial faults were discovered.

This paper appeared in Verification, Model Checking, and Abstract Interpretation: 8th International Conference, VMCAI 2007, Nice, France, January 14-16, 2007, Proceedings. Lecture Notes in Computer Science 4349, Springer-Verlag (2007), pages 44-58.

You may download the paper in one of the following formats:

Return to: Publications and Preprints.
Stephen F. Siegel / LASER / Dept of Comp. Sci. / UMass