Title: Efficient Verification of Halting Properties for MPI Programs with Wildcard Receives
Author: Stephen F. Siegel
Abstract:
We are concerned with the verification of certain properties, such as freedom from deadlock, for parallel programs that are written using the Message Passing Interface (MPI). It is known that for MPI programs containing no "wildcard receives" (and restricted to a certain subset of MPI) freedom from deadlock can be established by considering only synchronous executions. We generalize this by presenting a model checking algorithm that deals with wildcard receives by moving back and forth between a synchronous and a buffering mode as the search of the state space progresses. This approach is similar to that taken by partial order reduction (POR) methods, but can dramatically reduce the number of states explored even when the standard POR techniques do not apply.
Citation:
Radhia Cousot, ed.: Verification, Model Checking, and Abstract Interpretation: 6th International Conference, VMCAI 2005, Paris, January 17-19, 2005, Proceedings. Lecture Notes in Computer Science 3385, Springer-Verlag (2005), pages 413-429
BibTeX:
@InProceedings{siegel:2005:vmcai,
author = "Stephen F. Siegel",
title = "Efficient Verification of Halting Properties for {MPI} Programs with Wildcard Receives",
crossref = {vmcai2005},
pages = {413--429}
}
@Proceedings{vmcai2005,
editor = "Radhia Cousot",
title = "Verification, Model Checking, and Abstract Interpretation: 6th International Conference, {VMCAI} 2005, Paris, January 17--19, 2005, Proceedings",
booktitle = "Verification, Model Checking, and Abstract Interpretation: 6th International Conference, {VMCAI} 2005, Paris, January 17--19, 2005, Proceedings",
series = {LNCS},
volume = 3385,
year = 2005
}
Download: