Denotational reasoning for asynchronous multiparty session types

TL;DR

This paper introduces the first denotational semantics for asynchronous multiparty session types, enabling reasoning about message reordering and correctness of communication optimizations.

Contribution

It develops a novel denotational semantics model for asynchronous multiparty session types using grading to track computational effects.

Findings

Proves correctness of message reordering optimizations

Ensures communication safety, deadlock-freedom, and liveness

Models asynchronous message-passing as a computational effect

Abstract

We provide the first denotational semantics for asynchronous multiparty session types with precise asynchronous subtyping. Our semantics enables us to reason about asynchronous message-passing, in which message-sending is non-blocking. It enables us to prove the correctness of communication optimisations, in particular, those involving reordering of messages. Our development crucially relies on modelling message-passing as a computational effect. We apply grading, a paradigm for tracking computational effects, to asynchronous message-passing, demonstrating that multiparty session typing can be viewed as an instance of grading. We demonstrate the utility of our model by showing that it forms an adequate denotational semantics for a call-by-value asynchronous message-passing calculus, that ensures communication safety, deadlock-freedom and liveness in the presence of communication optimisations.