MAG$π$!: The Role of Replication in Typing Failure-Prone Communication

TL;DR

This paper addresses modeling failure-prone, timeout-based communication in distributed MPST. It introduces MAG$π$! as the first MPST extension that lifts replication from the $π$-calculus to the type level, enabling infinitely available servers and offloading failure handling to clients via timeout branches. It develops a formal language and type system with unrestricted, linear and affine contexts, and proves meta-theoretic properties including subject reduction and session fidelity, along with a safety predicate and deadlock- and termination-related results. It also provides a bag-buffer based operational semantics over networks, discusses topologies and client-server benefits, and outlines future work on decidability and deeper replication in MPST.

Abstract

MAG$π$ is a Multiparty, Asynchronous and Generalised $π$-calculus that introduces timeouts into session types as a means of reasoning about failure-prone communication. Its type system guarantees that all possible message-loss is handled by timeout branches. In this work, we argue that the previous is unnecessarily strict. We present MAG$π$!, an extension serving as the first introduction of replication into Multiparty Session Types (MPST). Replication is a standard $π$-calculus construct used to model infinitely available servers. We lift this construct to type-level, and show that it simplifies specification of distributed client-server interactions. We prove properties relevant to generalised MPST: subject reduction, session fidelity and process property verification.