Formal verification of programs that use MPI one-sided communication

Salman Pervez, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur, William Gropp

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We used formal-verification methods based on model checking to analyze the correctness properties of one existing and two new distributed-locking algorithms implemented by using MPI's one-sided communication. Model checking exposed an overlooked correctness issue with the first algorithm, which had been developed by relying only on manual reasoning. Model checking helped confirm the basic correctness properties of the two new algorithms, while also identifying the remaining problems in them. Our experience is that MPI-based programming, especially the tricky and relatively poorly understood one-sided communication features, stand to gain immensely from model checking. Considering that many other areas of concurrent hardware and software design now routinely employ model checking, our experience confirms that the MPI community can benefit greatly from the use of formal verification.

Original languageEnglish (US)
Title of host publicationRecent Advances in Parallel Virtual Machine and Message Passing Interface - 13th European PVM/MPI User's Group Meeting, Proceedings
PublisherSpringer
Pages30-39
Number of pages10
ISBN (Print)354039110X, 9783540391104
DOIs
StatePublished - 2006
Externally publishedYes
Event13th European PVM/MPI User's Group Meeting - Bonn, Germany
Duration: Sep 17 2006Sep 20 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4192 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th European PVM/MPI User's Group Meeting
Country/TerritoryGermany
CityBonn
Period9/17/069/20/06

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Formal verification of programs that use MPI one-sided communication'. Together they form a unique fingerprint.

Cite this