A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems

Malte Viering; Tzu-Chun Chen; Patrick Eugster; Raymond Hu; Lukasz Ziarek

doi:10.1007/978-3-319-89884-1_28

A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems

Malte Viering, Tzu-Chun Chen, Patrick Eugster, Raymond Hu, Lukasz Ziarek

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

86 Downloads (Pure)

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.

Original language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings
Editors	Amal Ahmed
Publisher	Springer Nature Link
Pages	799-826
Number of pages	27
Volume	10801
Edition	1
ISBN (Electronic)	978-3-319-89884-1
ISBN (Print)	978-3-319-89883-4, 3319898833
DOIs	https://doi.org/10.1007/978-3-319-89884-1_28
Publication status	Published - 14 Apr 2018
Event	27th European Symposium on Programming - Makedonia Palace, Thessaloniki, Greece Duration: 16 Apr 2018 → 19 Apr 2018 Conference number: 27 https://www.etaps.org/2018/esop

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	10801
ISSN (Print)	0302-9743

Conference

Conference	27th European Symposium on Programming
Abbreviated title	ESOP 2018
Country/Territory	Greece
City	Thessaloniki
Period	16/04/18 → 19/04/18
Internet address	https://www.etaps.org/2018/esop

Access to Document

10.1007/978-3-319-89884-1_28Licence: CC BY

Viering2018_Chapter_ATypingDisciplineForStaticallyFinal published version, 1.09 MBLicence: CC BY

Cite this

Viering, M., Chen, T.-C., Eugster, P., Hu, R., & Ziarek, L. (2018). A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems. In A. Ahmed (Ed.), Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings (1 ed., Vol. 10801, pp. 799-826). (Lecture Notes in Computer Science; Vol. 10801). Springer Nature Link. https://doi.org/10.1007/978-3-319-89884-1_28

Viering, Malte ; Chen, Tzu-Chun ; Eugster, Patrick et al. / A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems. Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. editor / Amal Ahmed. Vol. 10801 1. ed. Springer Nature Link, 2018. pp. 799-826 (Lecture Notes in Computer Science).

@inproceedings{f8004308a6794527b87059a122c67042,

title = "A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems",

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 inregards 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 imageof 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 explicitfailure 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 toprogress in a consistent manner with the remaining participants.",

author = "Malte Viering and Tzu-Chun Chen and Patrick Eugster and Raymond Hu and Lukasz Ziarek",

note = " {\textcopyright} The Author(s) 2018 ; 27th European Symposium on Programming, ESOP 2018 ; Conference date: 16-04-2018 Through 19-04-2018",

year = "2018",

month = apr,

day = "14",

doi = "10.1007/978-3-319-89884-1_28",

language = "English",

isbn = "978-3-319-89883-4",

volume = "10801",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature Link",

pages = "799--826",

editor = "Amal Ahmed",

booktitle = "Programming Languages and Systems",

address = "Netherlands",

edition = "1",

url = "https://www.etaps.org/2018/esop",

}

Viering, M, Chen, T-C, Eugster, P, Hu, R & Ziarek, L 2018, A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems. in A Ahmed (ed.), Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 1 edn, vol. 10801, Lecture Notes in Computer Science, vol. 10801, Springer Nature Link, pp. 799-826, 27th European Symposium on Programming, Thessaloniki, Greece, 16/04/18. https://doi.org/10.1007/978-3-319-89884-1_28

A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems. / Viering, Malte; Chen, Tzu-Chun; Eugster, Patrick et al.
Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. ed. / Amal Ahmed. Vol. 10801 1. ed. Springer Nature Link, 2018. p. 799-826 (Lecture Notes in Computer Science; Vol. 10801).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems

AU - Viering, Malte

AU - Chen, Tzu-Chun

AU - Eugster, Patrick

AU - Hu, Raymond

AU - Ziarek, Lukasz

N1 - Conference code: 27

PY - 2018/4/14

Y1 - 2018/4/14

N2 - 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 inregards 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 imageof 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 explicitfailure 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 toprogress in a consistent manner with the remaining participants.

AB - 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 inregards 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 imageof 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 explicitfailure 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 toprogress in a consistent manner with the remaining participants.

U2 - 10.1007/978-3-319-89884-1_28

DO - 10.1007/978-3-319-89884-1_28

M3 - Conference contribution

SN - 978-3-319-89883-4

SN - 3319898833

VL - 10801

T3 - Lecture Notes in Computer Science

SP - 799

EP - 826

BT - Programming Languages and Systems

A2 - Ahmed, Amal

PB - Springer Nature Link

T2 - 27th European Symposium on Programming

Y2 - 16 April 2018 through 19 April 2018

ER -

Viering M, Chen TC, Eugster P, Hu R, Ziarek L. A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems. In Ahmed A, editor, Programming Languages and Systems: 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 1 ed. Vol. 10801. Springer Nature Link. 2018. p. 799-826. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-89884-1_28

A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this