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

    77 Downloads (Pure)


    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 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 Nature
    Number of pages27
    ISBN (Electronic)978-3-319-89884-1
    ISBN (Print)978-3-319-89883-4, 3319898833
    Publication statusPublished - 14 Apr 2018
    Event27th European Symposium on Programming - Makedonia Palace, Thessaloniki, Greece
    Duration: 16 Apr 201819 Apr 2018
    Conference number: 27

    Publication series

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


    Conference27th European Symposium on Programming
    Abbreviated titleESOP 2018
    Internet address


    Dive into the research topics of 'A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems'. Together they form a unique fingerprint.

    Cite this