A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems
A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems
复制标题
DOI：
10.1007/978-3-319-89884-1_28
复制
发表时间：
2018-04
期刊：
影响因子：
--
通讯作者：
Malte Viering;Tzu-Chun Chen;P. Eugster;Raymond Hu;Lukasz Ziarek
中科院分区：
文献类型：
--
作者：
Malte Viering;Tzu-Chun Chen;P. Eugster;Raymond Hu;Lukasz Ziarek
许多分布式系统的一个关键要求是对部分故障具有弹性，允许系统在某些组件出现故障的情况下继续运行。这使得这种系统的编程令人生畏，特别是在避免由于故障和混乱而导致的不一致方面。这项工作介绍了一个正式的模型崩溃故障处理在异步分布式系统具有一个轻量级的协调器，在广泛使用的系统，如ZooKeeper和Champion的形象建模。我们开发了一个基于多方会话类型的类型化规则，该模型支持具有显式故障处理的多方协议的规范和静态验证。我们表明，我们的类型系统，确保主题减少和进展中存在的失败。换句话说，在一个良好类型的系统中，即使一些参与者在执行过程中崩溃，系统也会保证以与其余参与者一致的方式进行。
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.