Protocol-based verification of message-passing parallel programs

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

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

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.

OriginalsprogEngelsk
TitelOOPSLA 2015 - Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications
RedaktørerPatrick Eugster, Jonathan Aldrich
Antal sider19
ForlagAssociation for Computing Machinery, Inc.
Publikationsdato23 okt. 2015
Sider280-298
ISBN (Elektronisk)9781450336895
DOI
StatusUdgivet - 23 okt. 2015
Begivenhed2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015 - Pittsburgh, USA
Varighed: 25 okt. 201530 okt. 2015

Konference

Konference2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015
LandUSA
ByPittsburgh
Periode25/10/201530/10/2015
SponsorACM SIGPLAN
NavnProceedings of the Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA
Vol/bind25-30-Oct-2015

ID: 235144392