Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fearless Asynchronous Communications with Timed Multiparty Session Protocols

Ping Hou, Nicolas Lagaillardie, Nobuko Yoshida

TL;DR

This paper proposes the first formal integration of affinity, time constraints, timeouts, and time-failure handling based on multiparty session types based on multiparty session types for supporting reliability in asynchronous distributed systems.

Abstract

Session types using affinity and exception handling mechanisms have been developed to ensure the communication safety of protocols implemented in concurrent and distributed programming languages. Nevertheless, current affine session types are inadequate for specifying real-world asynchronous protocols, as they are usually imposed by time constraints which enable timeout exceptions to prevent indefinite blocking while awaiting valid messages. This paper proposes the first formal integration of affinity, time constraints, timeouts, and time-failure handling based on multiparty session types for supporting reliability in asynchronous distributed systems. With this theory, we statically guarantee that asynchronous timed communication is deadlock-free, communication safe, while being fearless -- never hindered by timeout errors or abrupt terminations. To implement our theory, we introduce a Rust toolchain designed to facilitate the implementation of safe affine timed protocols. Our toolchain leverages generic types and the time library to handle timed communications, integrated with optional types for affinity. We evaluate our approach by extending diverse examples from the literature to incorporate time and timeouts, demonstrating that our solution incurs negligible overhead compared with an untimed implementation. We also showcase the correctness by construction of our approach by implementing various real-world use cases, including a remote data protocol from the Internet of Remote Things domain, as well as protocols from real-time systems like Android motion sensors and smartwatches.

Fearless Asynchronous Communications with Timed Multiparty Session Protocols

TL;DR

This paper proposes the first formal integration of affinity, time constraints, timeouts, and time-failure handling based on multiparty session types based on multiparty session types for supporting reliability in asynchronous distributed systems.

Abstract

Session types using affinity and exception handling mechanisms have been developed to ensure the communication safety of protocols implemented in concurrent and distributed programming languages. Nevertheless, current affine session types are inadequate for specifying real-world asynchronous protocols, as they are usually imposed by time constraints which enable timeout exceptions to prevent indefinite blocking while awaiting valid messages. This paper proposes the first formal integration of affinity, time constraints, timeouts, and time-failure handling based on multiparty session types for supporting reliability in asynchronous distributed systems. With this theory, we statically guarantee that asynchronous timed communication is deadlock-free, communication safe, while being fearless -- never hindered by timeout errors or abrupt terminations. To implement our theory, we introduce a Rust toolchain designed to facilitate the implementation of safe affine timed protocols. Our toolchain leverages generic types and the time library to handle timed communications, integrated with optional types for affinity. We evaluate our approach by extending diverse examples from the literature to incorporate time and timeouts, demonstrating that our solution incurs negligible overhead compared with an untimed implementation. We also showcase the correctness by construction of our approach by implementing various real-world use cases, including a remote data protocol from the Internet of Remote Things domain, as well as protocols from real-time systems like Android motion sensors and smartwatches.
Paper Structure (37 sections, 9 theorems, 12 figures, 2 tables)

This paper contains 37 sections, 9 theorems, 12 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Overview
  3. ATMP: Theory Overview
  4. Solution to Stuck Processes Due to Time Failures
  5. $\texttt{MultiCrusty}^{T}$ : Toolchain Overview
  6. Affine Timed Multiparty Session Calculus
  7. Clock Constraint, Valuation, and Reset
  8. Syntax of Processes
  9. Operational Semantics
  10. Affine Timed Multiparty Session Type System
  11. Timed Multiparty Session Types
  12. Timed Local Types (timed session types)
  13. Queue Types
  14. Subtyping
  15. Projection
  16. ...and 22 more sections

Key Result

Theorem 14

Given associated timed global type $\langle{{\color{tcColor} \mathbb{V}}\xspace};{{\color{gtColor} G}}\rangle$ and typing environment ${\color{stColor} \Gamma}$: ${\color{tcColor}{\langle{{\color{tcColor} \mathbb{V}}\xspace};{{\color{gtColor} G}}\rangle} \mathrel{{\color{stColor}\sqsubseteq}_{{

Figures (12)

  • Figure 1: Overview of affine asynchronous communication with time.
  • Figure 2: Main types of $\texttt{MultiCrusty}^{T}$
  • Figure 3: Top: reduction rules for ATMP session $\pi$-calculus. Bottom: structural congruence rules for the ATMP$\pi$-calculus, where $\operatorname{fpv}\!\left({{\color{mpColor} D}}\right)$ is the set of free process variables in ${\color{mpColor} D}$, and $\operatorname{dpv}\!\left({{\color{mpColor} D}}\right)$ is the set of declared process variables in ${\color{mpColor} D}$. New rules are $\colorbox{\highlightColour}{$\text{highlighted}$}$.
  • Figure 4: Time-passing function ${\color{mpColor}\Psi_{{\color{tcColor} t}\xspace}({\color{mpColor} P})}$.
  • Figure 5: Syntax of timed global types, timed local types, and queue types.
  • ...and 7 more figures

Theorems & Definitions (29)

  • Definition 1: Syntax
  • Definition 2: Semantics
  • Remark 3
  • Example 4
  • Example 5
  • Definition 6: Subtyping
  • Definition 7: Projection
  • Example 8
  • Definition 9: Typing Environments
  • Definition 10: Typing Environment Reduction
  • ...and 19 more