A carregar...
Publicação
Type-Based Verification of Message-Passing Parallel Programs
| Nome: | Descrição: | Tamanho: | Formato: | |
|---|---|---|---|---|
| 672.77 KB | Adobe PDF | |||
| 673.61 KB | Adobe PDF |
Orientador(es)
Resumo(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.
Descrição
Palavras-chave
session types message passing type-based verification parallel programs