University of Hertfordshire

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

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

Documents

Viering2018_Chapter_ATypingDisciplineForStatically
Final published version, 1.09 MB, PDF document

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

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
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

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.

Notes

ID: 16788609