一种无领导并发原子广播算法的形式化描述与安全性证明
Formal Specification and Safety Proof of a Leaderless Concurrent Atomic Broadcast Algorithm
摘要：
协议在处理共同任务的分布式系统中起着核心作用。现代分布式系统的规模不断增加，使得它们更容易受到单个组件故障的影响。容错分布式协议主要依赖于基于领导者的原子广播算法，如Paxos。这种协议主要用于数据复制，只需要少量的服务器就可以达成协议。然而，它们的中心化性质使它们不适合大规模的分布式协议。最近引入的原子广播算法AllAccuur在完全分散的同时实现了分布式协议的高吞吐量。在本文中，我们从两个方面扩展了AllCONNECT的工作。首先，我们提供了一个正式的规范，使更好地理解该算法的AllConcur。其次，在此规范的基础上，形式化地证明了AllConcur的安全性。因此，我们的工作不仅确保了运营商安全使用AllCONNECT，而且有利于进一步改进基于AllCONNECT的分布式协议。
英文摘要：
Agreement plays a central role in distributed systems working on a common task. The increasing size of modern distributed systems makes them more susceptible to single component failures. Fault-tolerant distributed agreement protocols rely for the most part on leader-based atomic broadcast algorithms, such as Paxos. Such protocols are mostly used for data replication, which requires only a small number of servers to reach agreement. Yet, their centralized nature makes them ill-suited for distributed agreement at large scales. The recently introduced atomic broadcast algorithm AllConcur enables high throughput for distributed agreement while being completely decentralized. In this paper, we extend the work on AllConcur in two ways. First, we provide a formal specification of AllConcur that enables a better understanding of the algorithm. Second, we formally prove AllConcur's safety property on the basis of this specification. Therefore, our work not only ensures operators safe usage of AllConcur, but also facilitates the further improvement of distributed agreement protocols based on AllConcur.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
