论文标题
在LNT中对筏分布共识方案进行建模
Modeling the Raft Distributed Consensus Protocol in LNT
论文作者
论文摘要
共识协议对于可靠的分布式系统至关重要，因为它们让它们应对网络和服务器故障。几十年来，大多数共识协议一直被设计为开创性Paxos的变体，但在2014年，木筏被作为一种新的“可理解”协议呈现，比臭名昭著的微妙的Paxos家族更容易实施。此后，木筏已用于各种工业项目，例如Hashicorp的领事或ETCD（由Google的Kubernetes使用）。根据协议的TLA+规范，通过手动证明建立了筏的正确性。本文报告了我们在LNT过程代数中建模木筏建模的经验。从那以后，我们发现了木筏的原始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.
