Abstract
We show that many important properties of certain MPI programs can be verified by considering only a class of 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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Siegel, S. F., & Avrunin, G. S. (2007). Verification of halting properties for MPI programs using nonblocking operations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4757 LNCS, pp. 326–334). Springer Verlag. https://doi.org/10.1007/978-3-540-75416-9_44
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
