More Web Proxy on the site http://driver.im/

Article

A Type Theory for Robust Failure Handling in Distributed Systems

Authors:

Patrick EugsterAuthors Info & Claims

36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems - Volume 9688

Pages 96 - 113

https://doi.org/10.1007/978-3-319-39570-8_7

Published: 06 June 2016 Publication History

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.

References

[1]

Bettini, L., Coppo, M., D'Antoni, L., De Luca, M., Dezani-Ciancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: van Breugel, F., Chechik, M. eds. CONCUR 2008. LNCS, vol. 5201, pp. 418---433. Springer, Heidelberg 2008

Digital Library

[2]

Caires, L., Vieira, H.T.: Conversation types. In: Castagna, G. ed. ESOP 2009. LNCS, vol. 5502, pp. 285---300. Springer, Heidelberg 2009

Digital Library

[3]

Capecchi, S., Giachino, E., Yoshida, N.: Global escape in multiparty sessions. MSCS 29, 1---50 2015

[4]

Carbone, M., Honda, K., Yoshida, N.: Structured interactional exceptions in session types. In: van Breugel, F., Chechik, M. eds. CONCUR 2008. LNCS, vol. 5201, pp. 402---417. Springer, Heidelberg 2008

Digital Library

[5]

Carbone, M., Yoshida, N., Honda, K.: Asynchronous session types: exceptions and multiparty interactions. In: Bernardo, M., Padovani, L., Zavattaro, G. eds. SFM 2009. LNCS, vol. 5569, pp. 187---212. Springer, Heidelberg 2009

Digital Library

[6]

Collet, R., Van Roy, P.: Failure handling in a network-transparent distributed programming language. In: Cheraghchi, H.S., Lindskov Knudsen, J., Romanovsky, A., Babu, C.S. eds. Exception Handling. LNCS, vol. 4119, pp. 121---140. Springer, Heidelberg 2006

Digital Library

[7]

Colombo, C., Pace, G.J.: Recovery within long-running transactions. ACM Comput. Surv. 453, 28: 1---28: 35 2013

Digital Library

[8]

Deniélou, P.-M., Yoshida, N.: Dynamic multirole session types. In: POPL 2011, pp. 435---446 2011

Digital Library

[9]

Technical report. Long version of this paper. https://github.com/Distributed-Systems-Programming-Group/paper/blob/master/2016/forte16_long_dsp.pdf

[10]

Gärtner, F.C.: Fundamentals of fault-tolerant distributed computing in asynchronous environments. ACM Comput. Surv. 311, 1---26 1999

Digital Library

[11]

Guidi, C., Lanese, I., Montesi, F., Zavattaro, G.: On the interplay between fault handling and request-response service invocations. In: 8th International Conference on Application of Concurrency to System Design, 2008, ACSD 2008, pp. 190---198, June 2008

[12]

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL 2008, pp. 273---284. ACM 2008

Digital Library

[13]

Hu, R., Neykova, R., Yoshida, N., Demangeon, R., Honda, K.: Practical interruptible conversations. In: Legay, A., Bensalem, S. eds. RV 2013. LNCS, vol. 8174, pp. 130---148. Springer, Heidelberg 2013

[14]

Jakšić, S., Padovani, L.: Exception handling for copyless messaging. Sci. Comput. Program. 84, 22---51 2014

Digital Library

[15]

Lanese, I., Montesi, F.: Error handling: from theory to practice. In: Margaria, T., Steffen, B. eds. ISoLA 2010, Part II. LNCS, vol. 6416, pp. 66---81. Springer, Heidelberg 2010

Digital Library

[16]

Lanese, I., Montesi, F., Zavattaro, G.: Amending choreographies. In: WWV 2013, vol. 123 of EPTCS, pp. 34---48 2013

[17]

Mostrous, D.: Session Types, in Concurrent Calculi: Higher-Order Processes and Objects. Ph.D. thesis, Imperial College London 2009

[18]

Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge 2002

Digital Library

[19]

Takeuchi, K., Honda, H., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, Constantinos, Philokyprou, G., Maritsas, D., Theodoridis, Sergios eds. PARLE 1994. LNCS, vol. 817. Springer, Heidelberg 1994

Digital Library

[20]

Vieira, H.T., Caires, L., Seco, J.C.: The conversation calculus: a model of service-oriented computation. In: Drossopoulou, S. ed. ESOP 2008. LNCS, vol. 4960, pp. 269---283. Springer, Heidelberg 2008

Digital Library

[21]

Yoshida, N., Vasconcelos, V.T.: Language primitives and type discipline for structured communication-based programming revisited: two systems for higher-order session communication. Electr. Notes Theor. Comput. Sci. 1714, 73---93 2007

Digital Library

Cited By

Le Brun MDardha O(2024)MAG!: The Role of Replication in Typing Failure-Prone CommunicationFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-031-62645-6_6(99-117)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-62645-6_6
Peters KNestmann UWagner C(2022)Fault-Tolerant Multiparty Session TypesFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-031-08679-3_7(93-113)Online publication date: 13-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-08679-3_7
Fowler SLindley SMorris JDecova S(2019)Exceptional asynchronous session types: session types without tiersProceedings of the ACM on Programming Languages10.1145/32903413:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290341
Show More Cited By

A Type Theory for Robust Failure Handling in Distributed Systems
1. Theory of computation

Recommendations

Quasi-synchronous checkpointing and failure recovery in distributed systems
On the Implementation of Unreliable Failure Detectors in Partially Synchronous Systems

Unreliable failure detectors were proposed by Chandra and Toueg as mechanisms that provide information about process failures. Chandra and Toueg defined eight classes of failure detectors, depending on how accurate this information is, and presented an ...
Checkpointing and Rollback-Recovery for Distributed Systems
Special issue on distributed systems

We consider the problem of bringing a distributed system to a consistent state after transient failures. We address the two components of this problem by describing a distributed algorithm to create consistent checkpoints, as well as a rollback-recovery ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

36th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems - Volume 9688

June 2016

274 pages

ISBN:9783319395692

Editors:
Elvira Albert
Complutense University of Madrid, Madrid, Spain
,
Ivan Lanese
University of Bologna/Inria, Bologna, Italy

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 06 June 2016

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Le Brun MDardha O(2024)MAG!: The Role of Replication in Typing Failure-Prone CommunicationFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-031-62645-6_6(99-117)Online publication date: 17-Jun-2024
https://dl.acm.org/doi/10.1007/978-3-031-62645-6_6
Peters KNestmann UWagner C(2022)Fault-Tolerant Multiparty Session TypesFormal Techniques for Distributed Objects, Components, and Systems10.1007/978-3-031-08679-3_7(93-113)Online publication date: 13-Jun-2022
https://dl.acm.org/doi/10.1007/978-3-031-08679-3_7
Fowler SLindley SMorris JDecova S(2019)Exceptional asynchronous session types: session types without tiersProceedings of the ACM on Programming Languages10.1145/32903413:POPL(1-29)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290341
Thiemann PShin SShin DLencastre M(2017)Interleaving sessions with predicatesProceedings of the Symposium on Applied Computing10.1145/3019612.3019804(1312-1318)Online publication date: 3-Apr-2017
https://dl.acm.org/doi/10.1145/3019612.3019804

View Options

View options

Media

Figures

Other

Tables

View Table of Contents