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.Stephen F. Siegel, Efficient verification of halting properties for MPI programs with wildcard receives, in 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).
This paper is ©Springer-Verlag. You may download the paper in one of the following formats:
Other items: