Asynchronous Global Protocols, Precisely: Full Proofs

TL;DR

This paper introduces a rigorous framework for asynchronous multiparty session types, ensuring system compatibility, correctness, and liveness through a novel global-to-local projection approach with proven operational semantics.

Contribution

It presents the first proof of correctness for the most expressive endpoint projection, enabling independent component development with guaranteed system properties.

Findings

Proposed new operational semantics for global protocols.

Defined an asynchronous association between global protocols and local types.

Proved type soundness, session fidelity, deadlock-freedom, and liveness for optimized components.

Abstract

Asynchronous multiparty session types are a type-based framework which ensure the compatibility of components in a distributed system by checking compliance against a specified global protocol. We propose a top-down approach, starting with the global protocol which is then projected into a set of local specifications. Next, we use an asynchronous refinement relation, precise asynchronous multiparty subtyping, to enable local specifications to be optimised by permuting actions within individual asynchronous components. This supports local reasoning, as each component can be independently developed and refined in isolation, before being integrated into a larger system. We show that this methodology guarantees both type soundness and liveness of the collection of optimised components. In this article, we first propose new operational semantics of global protocols which capture sound optimisations in the context of asynchronous message-passing. Next we define an asynchronous association between global protocols and a set of optimised local types. Thirdly, we prove, for the first time, the correctness of the most expressive endpoint projection in the literature, coinductive full merging projection. We then show the main theorems of this article: soundness and completeness of the operational correspondence of the asynchronous association. As a consequence, the association acts as an invariant that can be used to transfer key theorems from the bottom-up system to the top-down system. In particular, we used this to prove type soundness, session-fidelity, deadlock-freedom and liveness of the collection of optimised endpoints.