Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Mixed Choice in Asynchronous Multiparty Session Types

Laura Bocchi, Raymond Hu, Adriana Laura Voinea, Simon Thompson

TL;DR

A core construct for MC is proposed that allows transient inconsistencies in protocol state between distributed participants, but ensures all participants can always eventually reach a mutually consistent state.

Abstract

We present a multiparty session type (MST) framework with asynchronous mixed choice (MC). We propose a core construct for MC that allows transient inconsistencies in protocol state between distributed participants, but ensures all participants can always eventually reach a mutually consistent state. We prove the correctness of our system by establishing a progress property and an operational correspondence between global types and distributed local type projections. Based on our theory, we implement a practical toolchain for specifying and validating asynchronous MST protocols featuring MC, and programming compliant gen_statem processes in Erlang/OTP. We test our framework by using our toolchain to specify and reimplement part of the amqp_client of the RabbitMQ broker for Erlang.

Mixed Choice in Asynchronous Multiparty Session Types

TL;DR

A core construct for MC is proposed that allows transient inconsistencies in protocol state between distributed participants, but ensures all participants can always eventually reach a mutually consistent state.

Abstract

We present a multiparty session type (MST) framework with asynchronous mixed choice (MC). We propose a core construct for MC that allows transient inconsistencies in protocol state between distributed participants, but ensures all participants can always eventually reach a mutually consistent state. We prove the correctness of our system by establishing a progress property and an operational correspondence between global types and distributed local type projections. Based on our theory, we implement a practical toolchain for specifying and validating asynchronous MST protocols featuring MC, and programming compliant gen_statem processes in Erlang/OTP. We test our framework by using our toolchain to specify and reimplement part of the amqp_client of the RabbitMQ broker for Erlang.
Paper Structure (26 sections, 6 theorems, 19 equations, 9 figures, 1 table)

This paper contains 26 sections, 6 theorems, 19 equations, 9 figures, 1 table.

Table of Contents

  1. Introduction
  2. Contributions and roadmap
  3. Overview
  4. Asymmetric Mixed Choice in Asynchronous MST
  5. Stale message purging.
  6. MC protocol validation.
  7. Mixed Choice MST protocols in Erlang
  8. Global-to-local projection
  9. EFSM representation
  10. Programming mMST-based processes in Erlang.
  11. Properties of mMST
  12. Global Types
  13. Committing Set and Well-Formedness
  14. Well-formedness
  15. Semantics of Global Types
  16. ...and 11 more sections

Key Result

theorem 1

If $\mathtt G$ is initial, aware, and balanced then it enjoys progress.

Figures (9)

  • Figure 1: A multiparty timeout pattern as a safe mMST protocol using asynchronous mixed choice.
  • Figure 2: Local mMST protocols for each role of Timeout as EFSMs in Erlang gen_statem.
  • Figure 3: Extracts from the user-facing callback modules generated for A and B in the Timeout protocol.
  • Figure 4: Global semantics: standard rules (top) and new rules for MC (bottom)
  • Figure 5: Local semantics, selected rules. See \ref{['app:locallts']} for omitted structural rules. and the two context rules, $\textsc{[NLCtxt]}$ and $\textsc{[NRCtxt]}$, for $\nu c$ actions on the LHS and RHS of $\mathtt L_1\blacktriangleright \mathtt L_2$, respectively.
  • ...and 4 more figures

Theorems & Definitions (15)

  • definition 1: Committing set
  • definition 2: Non-committing set
  • definition 3: Well-formedness
  • definition 4: Progress
  • definition 5: Role dependencies $<_{\mathtt G}$ and $\ll_{\mathtt G}$
  • definition 6: Awareness
  • definition 7: Balance
  • theorem 1: Progress
  • lemma 1: Bottom-up fidelity
  • lemma 2: Top-down fidelity
  • ...and 5 more