A typing discipline for statically verified crash failure handling in distributed systems
File(s)Viering2018_Chapter_ATypingDisciplineForStatically.pdf (1.09 MB)
Published version
Author(s)
Viering, M
Chen, T-C
Eugster, P
Hu, R
Ziarek, L
Type
Conference Paper
Abstract
A key requirement for many distributed systems is to be resilient toward partial failures, allowing a system to progress despite the failure of some components. This makes programming of such systems daunting, particularly in regards to avoiding inconsistencies due to failures and asynchrony. This work introduces a formal model for crash failure handling in asynchronous distributed systems featuring a lightweight coordinator, modeled in the image of widely used systems such as ZooKeeper and Chubby. We develop a typing discipline based on multiparty session types for this model that supports the specification and static verification of multiparty protocols with explicit failure handling. We show that our type system ensures subject reduction and progress in the presence of failures. In other words, in a well-typed system even if some participants crash during execution, the system is guaranteed to progress in a consistent manner with the remaining participants.
Date Issued
2018-04-14
Date Acceptance
2017-12-22
Citation
Programming Languages and Systems, 2018, 10801, pp.799-826
ISBN
9783319898834
ISSN
0302-9743
Publisher
Springer
Start Page
799
End Page
826
Journal / Book Title
Programming Languages and Systems
Volume
10801
Copyright Statement
© The Author(s) 2018. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter’s Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter’s Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
The images or other third party material in this chapter are included in the chapter’s Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter’s Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
License URL
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
ERI 025567 (EP/K034413/1)
PO 20131167
EP/K011715/1
EP/N027833/1
20103649
Source
ESOP 2018
Subjects
Artificial Intelligence & Image Processing
Publication Status
Published
Start Date
2018-04-14
Finish Date
2018-04-20
Coverage Spatial
Thessaloniki, Greece
Date Publish Online
2018-04-14