Fault-Tolerant Multiparty Session Types with Global Escape Loops

TL;DR

This paper introduces a fault-tolerant extension to multiparty session types with global escape loops, enabling verification of distributed algorithms' progress and termination without global coordination, exemplified by a variant of the rotating coordinator algorithm.

Contribution

It proposes a novel fault-tolerant loop construct with global escapes in session types, allowing local termination signals and non-blocking exit messages for distributed fault-tolerant algorithms.

Findings

Successfully models fault-tolerant distributed algorithms

Ensures progress and termination without global synchronization

Analyzes a variant of the rotating coordinator algorithm

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.