TY - GEN

T1 - Protocol-based verification of message-passing parallel programs

AU - López, Hugo A.

AU - Marques, Eduardo R.B.

AU - Martins, Francisco

AU - Ng, Nicholas

AU - Santos, César

AU - Vasconcelos, Vasco Thudichum

AU - Yoshida, Nobuko

PY - 2015/10/23

Y1 - 2015/10/23

N2 - 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.

AB - 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.

KW - Dependent types

KW - MPI

KW - Parallel programming

KW - Program verification

KW - Session types

UR - http://www.scopus.com/inward/record.url?scp=84958631303&partnerID=8YFLogxK

U2 - 10.1145/2814270.281430

DO - 10.1145/2814270.281430

M3 - Article in proceedings

AN - SCOPUS:84958631303

SP - 280

EP - 298

BT - OOPSLA 2015 - Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming Systems, Languages, and Applications

A2 - Eugster, Patrick

A2 - Aldrich, Jonathan

PB - Association for Computing Machinery

T2 - 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015

Y2 - 25 October 2015 through 30 October 2015

ER -