Type-Based Verification of Message-Passing Parallel Programs
VASCO THUDICHUM VASCONCELOS, Francisco Martins, Eduardo R. B. Marques, Hugo A. López, César Santos, Nobuko Yoshida · Portuguese National Funding Agency for Science, Research and Technology (RCAAP Project by FCT) · 2014
Abstract. We present a type-based approach to the verification of the communication structure of parallel programs. We model parallel imper-ative programs where a fixed number of processes, each equipped with its local memory, communicates via a rich diversity of primitives, includ-ing point-to-point messages, broadcast, reduce, and array scatter and gather. The paper proposes a decidable dependent type system incorpo-rating abstractions for the various communication operators, a form of primitive recursion, and collective choice. Term types may refer to val-ues 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. 1