Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

FTMPST: Fault-Tolerant Multiparty Session Types

Kirstin Peters, Uwe Nestmann, Christoph Wagner

TL;DR

This work extends multiparty session types (MPST) to cover fault-tolerant distributed algorithms by integrating failure-pattern semantics that model unreliable communication and crashes. It develops a fault-tolerant type system with global/local types, projections, and labels, and proves subject reduction and progress under carefully chosen failure-pattern conditions. The rotating coordinator algorithm serves as a concrete case study, illustrating how masking fault tolerance can be verified within this extended MPST framework and how termination, agreement, and validity can be achieved under standard fault-model assumptions. The approach provides a path toward formal verification of distributed protocols in fault-prone environments, with potential extensions to recursive and delegated fault-tolerant interactions.

Abstract

Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often resemble multiparty communication protocols. But proving their properties, in particular termination that is closely related to progress, can be elaborate. Since distributed algorithms are often designed to cope with faults, a first step towards using session types to verify distributed algorithms is to integrate fault-tolerance. We extend multiparty session types to cope with system failures such as unreliable communication and process crashes. Moreover, we augment the semantics of processes by failure patterns that can be used to represent system requirements (as, e.g., failure detectors). To illustrate our approach we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg.

FTMPST: Fault-Tolerant Multiparty Session Types

TL;DR

This work extends multiparty session types (MPST) to cover fault-tolerant distributed algorithms by integrating failure-pattern semantics that model unreliable communication and crashes. It develops a fault-tolerant type system with global/local types, projections, and labels, and proves subject reduction and progress under carefully chosen failure-pattern conditions. The rotating coordinator algorithm serves as a concrete case study, illustrating how masking fault tolerance can be verified within this extended MPST framework and how termination, agreement, and validity can be achieved under standard fault-model assumptions. The approach provides a path toward formal verification of distributed protocols in fault-prone environments, with potential extensions to recursive and delegated fault-tolerant interactions.

Abstract

Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often resemble multiparty communication protocols. But proving their properties, in particular termination that is closely related to progress, can be elaborate. Since distributed algorithms are often designed to cope with faults, a first step towards using session types to verify distributed algorithms is to integrate fault-tolerance. We extend multiparty session types to cope with system failures such as unreliable communication and process crashes. Moreover, we augment the semantics of processes by failure patterns that can be used to represent system requirements (as, e.g., failure detectors). To illustrate our approach we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg.
Paper Structure (15 sections, 10 theorems, 27 equations, 7 figures)

This paper contains 15 sections, 10 theorems, 27 equations, 7 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Summary
  4. Fault-Tolerance in Distributed Algorithms
  5. Fault-Tolerant Types and Processes
  6. Examples
  7. Projection
  8. Labels
  9. A Semantics with Failure Patterns
  10. Typing Fault-Tolerant Processes
  11. The Rotating Coordinator Algorithm
  12. Specification and Implementation
  13. Failure Patterns
  14. Termination, Agreement, and Validity
  15. Conclusions

Key Result

Lemma 5.3

If $\Gamma \vdash \mathit{P}\triangleright \Delta$ and $\mathit{P}\equiv \mathit{P}'$ then $\Gamma \vdash \mathit{P}' \triangleright \Delta$.

Figures (7)

  • Figure 1: Un-re-li-ab-le Communication (a) and Weak-ly Re-li-ab-le Branching (b).
  • Figure 2: Syntax of Fault-Tolerant MPST
  • Figure 3: Reduction Rules ($\longmapsto$) of Fault-Tolerant Processes (Part I).
  • Figure 4: Reduction Rules ($\longmapsto$) of Fault-Tolerant Processes (Part II).
  • Figure 5: Typing Rules for Fault-Tolerant Systems.
  • ...and 2 more figures

Theorems & Definitions (25)

  • Definition 3.1: Well-Formedness, Global Type
  • Definition 3.2: Well-Formedness, Global Type
  • Definition 5.1: Type Environments
  • Lemma 5.3: Subject Congruence
  • proof
  • Lemma 5.4: Substitution
  • proof
  • Definition 5.5: Coherence
  • Theorem 5.6: Subject Reduction
  • Definition 5.7: Weak Coherence
  • ...and 15 more