Large Scale Verification of MPI Programs Using Lamport Clocks with Lazy Update

Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby, Bronis R. De Supinski, Martin Schulz, Greg Bronevetsky

Research output: Chapter in Book/Report/Conference proceedingOther chapter contribution

10 Citations (Scopus)


We propose a dynamic verification approach for large-scale message passing programs to locate correctness bugs caused by unforeseen nondeterministic interactions. This approach hinges on an efficient protocol to track the causality between nondeterministic message receive operations and potentially matching send operations. We show that causality tracking protocols that rely solely on logical clocks fail to capture all nuances of MPI program behavior, including the variety of ways in which nonblocking calls can complete. Our approach is hinged on formally defining the matches-before relation underlying the MPI standard, and devising lazy update logical clock based algorithms that can correctly discover all potential outcomes of nondeterministic receives in practice. can achieve the same coverage as a vector clock based algorithm while maintaining good scalability. LLCP allows us to analyze realistic MPI programs involving a thousand MPI processes, incurring only modest overheads in terms of communication bandwidth, latency, and memory consumption.
Original languageEnglish
Title of host publication2011 International Conference on Parallel Architectures and Compilation Techniques (PACT)
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages10
ISBN (Print)978-1-4577-1794-9
Publication statusPublished - 2011


Dive into the research topics of 'Large Scale Verification of MPI Programs Using Lamport Clocks with Lazy Update'. Together they form a unique fingerprint.

Cite this