Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Fault-Tolerant Multiparty Session Types with Global Escape Loops

Lukas Bartl, Julian Linne, Kirstin Peters

TL;DR

The paper extends fault-tolerant multiparty session types (FTMPST) with a novel fault-tolerant loop that uses global escapes to achieve termination without requiring global coordination. It defines a semantics enriched with failure patterns and a non-blocking exit mechanism, and provides a typing framework with coherence to ensure progress and termination under controlled fault assumptions. The Rotating Coordinator Algorithm is used as a case study to demonstrate how unreliably communicating loops and exit messages support agreement and termination in a fault-prone setting. Overall, the work advances verification of distributed algorithms under faults by integrating failure patterns, un-reliable loop constructs, and global escapes into MPST, while outlining directions for relaxation of assumptions and automation of proofs.

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 FTMPST (a version of fault-tolerant multiparty session types with failure patterns to represent system requirements for system failures such as unreliable communication and process crashes) by a novel, fault-tolerant loop construct with global escapes that does not require global coordination. Each process runs its own local version of the loop. If a process finds a solution to the considered problem, it does not only terminate its own loop but also informs the other participants via exit-messages. Upon receiving an exit-message, a process immediately terminates its algorithm. To increase efficiency and model standard fault-tolerant algorithms, these messages are non-blocking, i.e., a process may continue until a possibly delayed exit-message is received. To illustrate our approach, we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg.

Fault-Tolerant Multiparty Session Types with Global Escape Loops

TL;DR

The paper extends fault-tolerant multiparty session types (FTMPST) with a novel fault-tolerant loop that uses global escapes to achieve termination without requiring global coordination. It defines a semantics enriched with failure patterns and a non-blocking exit mechanism, and provides a typing framework with coherence to ensure progress and termination under controlled fault assumptions. The Rotating Coordinator Algorithm is used as a case study to demonstrate how unreliably communicating loops and exit messages support agreement and termination in a fault-prone setting. Overall, the work advances verification of distributed algorithms under faults by integrating failure patterns, un-reliable loop constructs, and global escapes into MPST, while outlining directions for relaxation of assumptions and automation of proofs.

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 FTMPST (a version of fault-tolerant multiparty session types with failure patterns to represent system requirements for system failures such as unreliable communication and process crashes) by a novel, fault-tolerant loop construct with global escapes that does not require global coordination. Each process runs its own local version of the loop. If a process finds a solution to the considered problem, it does not only terminate its own loop but also informs the other participants via exit-messages. Upon receiving an exit-message, a process immediately terminates its algorithm. To increase efficiency and model standard fault-tolerant algorithms, these messages are non-blocking, i.e., a process may continue until a possibly delayed exit-message is received. To illustrate our approach, we analyse a variant of the well-known rotating coordinator algorithm by Chandra and Toueg.

Paper Structure

This paper contains 6 sections, 2 theorems, 15 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Fault-Tolerant Types and Processes
  3. A Semantics with Failure Patterns for Global Escape Loops
  4. Typing Fault-Tolerant Processes
  5. The Rotating Coordinator Algorithm
  6. Conclusions

Key Result

Theorem 2

If $\Gamma, \Delta$ are coherent, $\Gamma, \textcolor{blue}{\Theta} \vdash \mathit{P}\triangleright \Delta$, and $\mathit{P}\longmapsto \mathit{P}'$, then there is some $\Delta'$ such that $\Gamma, \textcolor{blue}{\Theta} \vdash \mathit{P}' \triangleright \Delta'$.

Figures (4)

  • Figure 1: Syntax of Fault-Tolerant MPST with Global Escape Loops.
  • Figure 2: Reduction Rules ($\longmapsto$) of Fault-Tolerant Processes with Global Escape Loops.
  • Figure 3: Typing Rules for Fault-Tolerant Systems with Global Escape Loops.
  • Figure 4: Runtime Typing Rules for Fault-Tolerant Systems.

Theorems & Definitions (4)

  • Definition 1: Type Environments
  • Definition 2: Coherence
  • Theorem 2: Subject Reduction
  • Theorem 3: Progress/Session Fidelity