Sciweavers

Share
FM
2009
Springer

Reduced Execution Semantics of MPI: From Theory to Practice

11 years 6 months ago
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.
Sarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishn
Added 26 May 2010
Updated 26 May 2010
Type Conference
Year 2009
Where FM
Authors Sarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby
Comments (0)
books