This paper introduces a programming framework based on the theory of session types for safe and scalable parallel designs. Session-based languages can offer a clear and tractable framework to describe communications between parallel components and guarantee communication-safety and deadlock-freedom by compile-time type checking and parallel MPI code generation. Many representative communication topologies such as ring or scatter-gather can be programmed and verified in session-based programming languages.
We use a case study involving N-body simulation to illustrate the session-based programming style. Finally, we outline a proposal to integrate session programming with heterogeneous systems for edcient and communication-safe parallel applications by a combination of code generation and type checking.
Presented in 2nd International Workshop on Behavioural Types (BEAT2), September 2013
Published version via DOI | Paper | www