A Type Theory for Robust Failure Handling in Distributed Systems - Formal Techniques for Distributed Objects, Components, and Systems
Conference Papers Year : 2016

A Type Theory for Robust Failure Handling in Distributed Systems

Abstract

This paper presents a formal framework for programming distributed applications capable of handling partial failures, motivated by the non-trivial interplay between failure handling and messaging in asynchronous distributed environments. Multiple failures can affect protocols at the level of individual interactions (alignment). At the same time, only participants affected by a failure or involved in its handling should be informed of it, and its handling should not be mixed with that of other failures (precision). This is particularly challenging, as through the structure of protocols, failures may be linked to others in subsequent or concomitant interactions (causality). Last but not least, no central authority should be required for handling failures (decentralisation). Our goal is to give developers a description language, called protocol types, to specify robust failure handling that accounts for alignment, precision, causality, and decentralisation. A type discipline is built to statically ensure that asynchronous failure handling among multiple endpoints is free from orphan messages, deadlocks, starvation, and interactions are never stuck.
Fichier principal
Vignette du fichier
426757_1_En_7_Chapter.pdf (866.92 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Loading...

Dates and versions

hal-01432930 , version 1 (12-01-2017)

Licence

Identifiers

Cite

Tzu-Chun Chen, Malte Viering, Andi Bejleri, Lukasz Ziarek, Patrick Eugster. A Type Theory for Robust Failure Handling in Distributed Systems. 36th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), Jun 2016, Heraklion, Greece. pp.96-113, ⟨10.1007/978-3-319-39570-8_7⟩. ⟨hal-01432930⟩
216 View
242 Download

Altmetric

Share

More