Fair Termination of Asynchronous Binary Sessions
Luca Padovani, Gianluigi Zavattaro
TL;DR
The paper addresses ensuring termination and liveness for asynchronous binary sessions under a fairness assumption. It develops CaP, a calculus of asynchronous processes with non-blocking outputs modeled by buffers, and a linear-logic based framework for asynchronous session types, including a coinductive, fair LTS semantics. A new fair asynchronous subtyping relation, closed under duality, enables a robust type system guaranteeing fair termination and absence of orphan messages. The work advances the theory of asynchronous session types by linking subtyping, duality, and linear logic, and provides a foundation for practical liveness guarantees in asynchronous communication protocols.
Abstract
We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.