Asynchronous Global Protocols, Precisely: Full Proofs
Kai Pischke, Jake Masters, Nobuko Yoshida
TL;DR
This work tackles asynchronous multiparty session types by introducing a top-down framework that starts from a global protocol $G$, projects to local types, and refines them via precise asynchronous subtyping $\le_{a}$ to obtain optimized local types. The core innovation is an association between typing contexts and global types, proven to be sound and complete with respect to the operational semantics, enabling transfer of main theorems from bottom-up (local-types-based) MPST to the top-down (global-based) MPST. The authors establish a coinductive full merging projection for asynchronous settings, define a robust semantics for global types and typing contexts, and prove subject reduction and session fidelity for the top-down system via this association. They also introduce balanced^+ global types to ensure liveness and safety in the presence of en-route messages, and demonstrate that associated contexts are live, safe, and deadlock-free. Overall, the paper provides a rigorous bridge between global specifications and optimised local implementations, with formal guarantees that support reasoning about asynchronous MPST in distributed systems and potential for practical toolchains and verification.
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.