Protocol-Based Verification of Message-Passing Parallel Programs

Hugo-Andrés López-Acosta, Eduardo R. B. Eduardo R. B. Marques, Francisco Martins, Nicholas Ng, César Santos, Vasco Thudichum Vasconcelos, Nobuko Yoshida

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

We present ParTypes, a type-based methodology for the verification of Message Passing Interface (MPI) programs written in the C programming language. The aim is to statically verify programs against protocol specifications, enforcing properties such as fidelity and absence of deadlocks. We develop a protocol language based on a dependent type system for message-passing parallel programs, which includes various communication operators, such as point-to-point messages, broadcast, reduce, array scatter and gather. For the verification of a program against a given protocol, the protocol is first translated into a representation read by VCC, a software verifier for C. We successfully verified several MPI programs in a running time that is independent of the number of processes or other input parameters. This contrasts with alternative techniques, notably model checking and runtime verification, that suffer from the state-explosion problem or that otherwise depend on parameters to the program itself. We experimentally evaluated our approach against state-of-the-art tools for MPI to conclude that our approach offers a scalable solution.
Original languageEnglish
Title of host publicationProceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2015
PublisherAssociation for Computing Machinery
Publication date2015
Pages280-298
ISBN (Print)978-1-4503-3689-5
DOIs
Publication statusPublished - 2015
EventOOPSLA'15 - The ACM SIGPLAN conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH) - Pittsburgh, United States
Duration: 25 Oct 201530 Oct 2015
http://2015.splashcon.org/

Conference

ConferenceOOPSLA'15 - The ACM SIGPLAN conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH)
Country/TerritoryUnited States
CityPittsburgh
Period25/10/201530/10/2015
Other2015: SPLASH includes OOPSLA
Internet address

Keywords

  • Program verification
  • Parallel programming
  • MPI
  • Session types
  • Dependent types

Fingerprint

Dive into the research topics of 'Protocol-Based Verification of Message-Passing Parallel Programs'. Together they form a unique fingerprint.

Cite this