Sessions and Separation

Session types and separation logic are two formalisms used to obtain strong guarantees about concurrent programs, each with their own benefits. Session types provide an intuitive protocol mechanism for specifying sequences of value exchanges, where each exchange is constrained to a specific type. In contrast, separation logic is often used for more involved specifications and proofs about shared-memory concurrency.
This thesis combines the two efforts by introducing dependent separation protocols – a session-type based reasoning mechanism in separation logic – and a semantic session type system – a session type system that combines the expressivity of separation logic with the simplicity of type checking.
Dependent separation protocols mimic the intuition behind session types, by describing sequences of value exchanges constrained by separation-logic propositions. The dependent separation protocols are formalised for a representative language with fine-grained concurrency, mutable state, and higher-order functions. This formalisation, which we call Actris, is built on top of the higher-order concurrent separation logic Iris. The use of Iris provides the ability to reason about recursion, substructural properties, and integration with existing concurrency models, such as shared-memory and lock-based concurrency. We demonstrate the expressivity of Actris by proving the correctness of several variants of a distributed merge sort algorithm, a distributed load-balancing mapper, and a variant of the map-reduce algorithm.
The semantic session type system is achieved using semantic typing and logical relations, where the types and judgements of the type system are defined in terms of Actris. The type system supports term- and session-type polymorphism, equi-recursion, and subtyping, as well as copyable types, shared and mutable reference types, and mutex types. The type system additionally supports manual typing proofs, where typing judgements that cannot be derived from the typing rules of the type system can instead be proven in the logic. This technique effectively lets us combine the full expressivity of the logic, with the simplicity of the syntax-directed type checking of the type system. We demonstrate this feature by manually proving the typing judgement of a program, where two threads operate on a single session-typed channel endpoint in parallel.
All of the results of the thesis have been mechanised in the interactive proof assistant Coq, on top of the existing mechanisation of Iris, along with tactic support for resolving proof obligations related to message passing in a style similar to working with session types.