| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 672.77 KB | Adobe PDF | |||
| 673.61 KB | Adobe PDF |
Advisor(s)
Abstract(s)
We present a type-based approach to the verification of the
communication structure of parallel programs. We model parallel imperative programs where a fixed number of processes, each equipped with its local memory, communicates via a rich diversity of primitives, including point-to-point messages, broadcast, reduce, and array scatter and gather. The paper proposes a decidable dependent type system incorporating abstractions for the various
communication operators, a form of primitive recursion, and
collective choice. Term types may refer to values in the programming
language, including integer, floating point and arrays. The paper
further introduces a core programming language for imperative,
message-passing, parallel programming, and shows that the language
enjoys progress.
Description
Keywords
session types message passing type-based verification parallel programs