Session types for link failures

DOI10.1007/978-3-319-60225-7_1MaRDI QIDQ5082187zbMATH OpenOpenAlexFDO

Authors Manuel Adameit, Kirstin Peters, Uwe Nestmann

Publication date 15 June 2022

Published in Formal Techniques for Distributed Objects, Components, and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1607.07286, https://hal.inria.fr/hal-01658430/document

Mathematics Subject Classification ID

Reliability, testing and fault tolerance of networks and computer systems (68M15) Distributed algorithms (68W15) Distributed systems (68M14)

Abstract: We strive to use session type technology to prove behavioural properties of fault-tolerant distributed algorithms. Session types are designed to abstractly capture the structure of (even multi-party) communication protocols. The goal of session types is the analysis and verification of the protocols' behavioural properties. One important such property is progress, i.e., the absence of (unintended) deadlock. Distributed algorithms often resemble (compositions of) multi-party communication protocols. In contrast to protocols that are typically studied with session types, they are often designed to cope with system failures. An essential behavioural property is (successful) termination, despite failures, but it is often elaborate to prove for distributed algorithms. We extend multi-party session types (and multi-party session types with nested sessions) by optional blocks that cover a limited class of link and crash failures. This allows us to automatically derive termination of distributed algorithms that come within these limits. To illustrate our approach, we prove termination for an implementation of the *rotating coordinator* Consensus algorithm.

Recommendations

• scientific article; zbMATH DE number 7075898
• CONCUR 2004 - Concurrency Theory
• Parameterised multiparty session types
• Modular session types for distributed object-oriented programming

Cited in

(6)

• A model of actors and grey failures
• Crash-stop failures in asynchronous multiparty session types
• A session type system for asynchronous unreliable broadcast communication
• A type theory for robust failure handling in distributed systems
• A typing discipline for statically verified crash failure handling in distributed systems
• MAG\(\pi\): types for failure-prone communication

This page was built for publication: Session types for link failures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5082187)