Multiparty Session Types with a Bang!

TL;DR

Extends MPST to address limitations in replication and first-class role handling. MPST! is a conservative extension of MPST that adds replication (bang) and first-class roles, and its metatheory is developed as subject reduction and session fidelity parameterised by a safety property $\varphi$. Replication, especially together with recursion, increases expressiveness to context-free MPST and enables protocols involving races and mutual exclusion, demonstrated via load balancer, binary-tree serialization, dining philosophers, and an auction service. The paper analyzes typechecking decidability, proposes two syntactic approximations (tf and lf) to identify decidable subsets, and discusses practical design implications and connections to related work.

Abstract

Replication is an alternative construct to recursion for describing infinite behaviours in the pi-calculus. In this paper we explore the implications of including type-level replication in Multiparty Session Types (MPST), a behavioural type theory for message-passing programs. We introduce MPST!, a session-typed multiparty process calculus with replication and first-class roles. We show that replication is not an equivalent alternative to recursion in MPST, and that using both replication and recursion in one type system in fact allows us to express both context-free protocols and protocols that support mutual exclusion and races. We demonstrate the expressiveness of MPST! on examples including binary tree serialisation, dining philosophers, and a model of an auction, and explore the implications of replication on the decidability of typechecking.