PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms
PSYNC: A Partially Synchronous Language for Fault-Tolerant Distributed Algorithms
复制标题
DOI：
10.1145/2914770.2837650
复制
发表时间：
2016-01-01
影响因子：
--
通讯作者：
Zufferey, Damien
中科院分区：
文献类型：
--
作者：
Dragoi, Cezara;Henzinger, Thomas A.;Zufferey, Damien
容错分布式算法在许多关键/高可用性应用中扮演着重要的角色。本文介绍了一种基于已知模型的领域专用语言PSYNC，该语言将异步故障系统视为具有敌意环境的同步系统，通过丢弃消息来模拟异步和故障。我们为PSYNC定义了一个在异步网络上高效执行的运行时系统。我们从观测精化的角度形式化了运行时系统和PSYNC之间的关系。PSYNC引入的高级锁步抽象简化了容错分布式算法的设计和实现，并实现了自动化的形式化验证。我们用一个异步网络运行时系统实现了PSYNC在Scala编程语言中的嵌入。我们通过实现几种重要的容错分布式算法来展示PSYNC的适用性，并在代码大小、运行效率和验证方面与其他语言实现的一致性算法进行了比较。
Fault-tolerant distributed algorithms play an important role in many critical/high-availability applications. These algorithms are notoriously difficult to implement correctly, due to asynchronous communication and the occurrence of faults, such as the network dropping messages or computers crashing.We introduce PSYNC, a domain specific language based on the Heard-Of model, which views asynchronous faulty systems as synchronous ones with an adversarial environment that simulates asynchrony and faults by dropping messages. We define a runtime system for PSYNC that efficiently executes on asynchronous networks. We formalize the relation between the runtime system and PSYNC in terms of observational refinement. The high-level lockstep abstraction introduced by PSYNC simplifies the design and implementation of fault-tolerant distributed algorithms and enables automated formal verification.We have implemented an embedding of PSYNC in the SCALA programming language with a runtime system for asynchronous networks. We show the applicability of PSYNC by implementing several important fault-tolerant distributed algorithms and we compare the implementation of consensus algorithms in PSYNC against implementations in other languages in terms of code size, runtime efficiency, and verification.