| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 1.78 MB | Adobe PDF | |||
| 1.78 MB | Adobe PDF |
Advisor(s)
Abstract(s)
We present a methodology for the verification of Message Passing
Interface (MPI) programs written in C. The aim is to statically
verify programs against protocol specifications, enforcing
properties such as fidelity and absence of deadlocks. We make use
of a protocol language based on a dependent type system for
message-passing parallel programs.
%
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 the~C programming language.
%
The program is then annotated with specific assertions that,
together with a pre-established set of contracts for MPI primitives,
guide the verifier to either prove or disprove the program's
conformance to the protocol.
We successfully verified MPI programs in a running time that is
independent of the number of processes or other input parameters.
This contrasts with other techniques, notably model checking and
symbolic execution, that suffer from the state-explosion problem.
We experimentally evaluated our approach against TASS,
a state-of-the-art tool for MPI program verification.
Description
Keywords
protocol parallel programs verification MPI