Protocol-Based Verification of Message-Passing Parallel Programs
File(s)
Accepted version
Author(s)
Type
Conference Paper
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-ofthe-art
tools for MPI to conclude that our approach offers a
scalable solution.
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-ofthe-art
tools for MPI to conclude that our approach offers a
scalable solution.
Date Issued
2015-10-25
Date Acceptance
2015-08-03
Publisher
ACM
Copyright Statement
© ACM, 2015. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in PUBLICATION, {VOL#, ISS#, (DATE)} https://dx.doi.org/10.1145/2814270.2814302
Source
2015 ACM International Conference on Object Oriented Programming, Systems, Languages & Applications
Publication Status
Accepted
Start Date
2015-10-25
Finish Date
2015-10-30
Coverage Spatial
Pittsburgh, Pennsylvania