University of Hertfordshire

By the same authors

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

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

Documents

  • Malte Viering
  • Tzu-Chun Chen
  • Patrick Eugster
  • Raymond Hu
  • Lukasz Ziarek
View graph of relations
Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication27th 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
EditorsAmal Ahmed
PublisherSpringer
Pages799-826
Number of pages27
Volume10801
Edition1
ISBN (Electronic)978-3-319-89884-1
ISBN (Print)978-3-319-89883-4, 3319898833
DOIs
Publication statusPublished - 14 Apr 2018
Event27th 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

NameLecture Notes in Computer Science
PublisherSpringer
Volume10801
ISSN (Print)0302-9743

Conference

Conference27th European Symposium on Programming
Abbreviated titleESOP 2018
CountryGreece
CityThessaloniki
Period16/04/18 → 19/04/18
Internet address

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

© The Author(s) 2018

ID: 16788609