Manifestly Phased Communication via Shared Session Types

TL;DR

This paper extends session types to shared channels with multiple clients, enabling static verification of multi-phase protocols in concurrent systems, which was not possible with prior linear session type models.

Contribution

It introduces a novel subtyping framework for shared session types, capturing multi-phase interaction protocols with manifest phases in client types.

Findings

Supports multi-phase client-server interactions

Enables static protocol verification for shared channels

Generalizes previous linear session type subtyping

Abstract

Session types denote message protocols between concurrent processes, allowing a type-safe expression of inter-process communication. Although previous work demonstrate a well-defined notion of subtyping where processes have different perceptions of the protocol, these formulations were limited to linear session types where each channel of communication has a unique provider and client. In this paper, we extend subtyping to shared session types where channels can now have multiple clients instead of a single client. We demonstrate that this generalization can statically capture protocol requirements that span multiple phases of interactions of a client with a shared service provider, something not possible in prior proposals. Moreover, the phases are manifest in the type of the client.