TY - GEN
T1 - A type theory for robust failure handling in distributed systems
AU - Chen, Tzu Chun
AU - Viering, Malte
AU - Bejleri, Andi
AU - Ziarek, Lukasz
AU - Eugster, Patrick
N1 - Publisher Copyright: © IFIP International Federation for Information Processing 2016.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
KW - Distributed systems
KW - Partial failure handling
KW - Session types
UR - https://www.scopus.com/pages/publications/84977566431
U2 - 10.1007/978-3-319-39570-8_7
DO - 10.1007/978-3-319-39570-8_7
M3 - Conference contribution
SN - 9783319395692
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 96
EP - 113
BT - Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016 Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016, Proceedings
A2 - Albert, Elvira
A2 - Lanese, Ivan
PB - Springer Verlag
T2 - 36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2016 and Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, DisCoTec 2016
Y2 - 6 June 2016 through 9 June 2016
ER -