Abstract. We show that many important properties of certain MPI programs can be verified by considering only executions in which all communication takes place synchronously. In previous work, we showed that similar results hold for MPI programs that use only blocking communication (and avoid certain other constructs, such asMPI_ANY_SOURCE); in this paper we show that the same conclusions hold for programs that also use the nonblocking functionsMPI_ISEND,MPI_IRECV, andMPI_WAIT. These facts can be used to dramatically reduce the number of states explored when using model checking techniques to verify properties such as freedom from deadlock in such programs.
This paper appeared in Recent Advances in Parallel Virtual Machine and Message Passing Interface: 14th European PVM/MPI Users' Group Meeting, Paris, France, September/October 2007, Proceedings. Lecture Notes in Computer Science 4757, Springer-Verlag (2007), pages 326-334.
You may download the paper in one of the following formats: