Title: Verification of Halting Properties for MPI Programs Using Nonblocking Operations
Authors: Stephen F. Siegel and George S. Avrunin
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 as MPI_ANY_SOURCE); in this paper we show that the same conclusions hold for programs that also use the nonblocking functions MPI_ISEND, MPI_IRECV, and MPI_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.
Apeeared 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.
BibTeX:
@InProceedings{siegel-avrunin:2007:nbsynch,
author = {Stephen F. Siegel and George S. Avrunin},
title = {Verification of Halting Properties for {MPI} Programs Using Nonblocking Operations},
year = {2007},
pages = {326--334},
crossref = {pvmmpi2007},
}
@Proceedings{pvmmpi2007,
editor = {Franck Cappello and Thomas H{\'e}rault and Jack Dongarra},
booktitle = {Recent Advances in Parallel Virtual Machine and Message Passing Interface, 14th European PVM/MPI User's Group Meeting, Paris, France, September 30 - October 3, 2007, Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {4757},
year = {2007}
}
Download: