A Sound and Complete Characterization of Fair Asynchronous Session Subtyping

TL;DR

This paper provides a complete semantic characterization of fair asynchronous session subtyping, enabling more precise analysis of communication protocols in message-passing systems.

Contribution

It introduces a novel labeled transition system that captures asynchronous semantics, achieving a sound and complete characterization of fair refinement for session types.

Findings

Established a sound and complete semantic characterization.

Linked asynchronous and synchronous session type refinements.

Developed a novel labeled transition system for session types.

Abstract

Session types are abstractions of communication protocols enabling the static analysis of message-passing processes. Refinement notions for session types are key to support safe forms of process substitution while preserving their compatibility with the rest of the system. Recently, a fair refinement relation for asynchronous session types has been defined allowing the anticipation of message outputs with respect to an unbounded number of message inputs. This refinement is useful to capture common patterns in communication protocols that take advantage of asynchrony. However, while the semantic (\`a la testing) definition of such refinement is straightforward, its characterization has proved to be quite challenging. In fact, only a sound but not complete characterization is known so far. In this paper we close this open problem by presenting a sound and complete characterization of asynchronous fair refinement for session types. We relate this characterization to those given in the literature for synchronous session types by leveraging a novel labelled transition system of session types that embeds their asynchronous semantics.