LNT中筏式分布式共识协议的建模
Modeling the Raft Distributed Consensus Protocol in LNT
摘要：
共识协议对于可靠的分布式系统至关重要，因为它们可以让它们处理网络和服务器故障。几十年来，大多数共识协议都被设计为开创性的Paxos的变体，但在2014年，Raft被作为一个新的、“可理解的”协议提出，这意味着比众所周知的微妙的Paxos家族更容易实现。此后，Raft被用于各种工业项目，例如Hashicorp的Consul或etcd（由Google的Kubernetes使用）。Raft的正确性是基于协议的TLA+规范通过手动证明建立的。本文报告了我们在LNT进程代数中对Raft建模的经验。我们发现了一对夫妇的问题与原来的TLA+规格的筏，这已被纠正以来。更一般地说，这个练习提供了一个很好的机会来讨论如何最好地使用LNT形式语言和相关的CADP验证工具箱的功能来建模分布式协议，包括网络和服务器故障。
英文摘要：
Consensus protocols are crucial for reliable distributed systems as they let them cope with network and server failures. For decades, most consensus protocols have been designed as variations of the seminal Paxos, yet in 2014 Raft was presented as a new, "understandable" protocol, meant to be easier to implement than the notoriously subtle Paxos family. Raft has since been used in various industrial projects, e.g. Hashicorp's Consul or etcd (used by Google's Kubernetes). The correctness of Raft is established via a manual proof, based on a TLA+ specification of the protocol. This paper reports our experience in modeling Raft in the LNT process algebra. We found a couple of issues with the original TLA+ specification of Raft, which has been corrected since. More generally, this exercise offers a great opportunity to discuss how to best use the features of the LNT formal language and the associated CADP verification toolbox to model distributed protocols, including network and server failures.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
