Reduced Execution Semantics of MPI: From Theory to Practice

Abstract: There is growing need to develop formal verification tools for Message Passing Interface (MPI) programs, to eliminate bugs such as deadlocks and local assertion violations. Of all approaches, dynamic verification is most practical for MPI. Since the number of interleavings of concurrent programs grow exponentially, we devise a dynamic interleaving reduction algorithm (dynamic partial order reduction, DPOR) tailor-made for MPI, called POE. The key contributions of this paper are: (i) a formal semantics that elucidates the complex dynamic semantics of MPI, and played an essential role in the design of the POE algorithm and the construction of the ISP tool. (ii) a formal specification of our POE algorithm. We discuss how these ideas may help us build dynamic verifier for other APIs, and summarize a dynamic verifier being designed for applications written using a recently proposed API for multi-core communication.

• Type: Conference
• Year: 2009
• Where: FM
• Authors: Sarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby
• Keywords: Dynamic Interleaving Reduction, Dynamic Verifier, FM 2009, Natural Language Processing, POE Algorithm