TLA+ 入门教程（6）：Raft

与上一节讨论 Paxos 时一样，本文不介绍 Raft 协议基本知识，读者需已经了解 Raft 协议，如无这部分背景知识，请阅读 Raft 论文或参见《条分缕析Raft算法》。

注：文末有投票，接下来想看什么？

Raft 协议的 TLA+ 规约

本文参考 Diego Ongaro 提供的 TLA+ 规约：https://github.com/ongardie/raft.tla

常量

Raft 的 TLA+ 规约将系统抽象为以下几个常量：

Server，节点 ID 集合
Value，客户端的一系列请求，发送到 Raft 状态机的值
Follower, Candidate, Leader，Raft 节点的三个状态
Nil，空的消息
四种消息类型 RequestVoteRequest, RequestVoteResponse, AppendEntriesRequest, AppendEntriesResponse

变量

Raft 的 TLA+ 规约包括的变量主要还是和论文 Figure 2 相对应。

所有节点都有：

currentTerm，当前任期，需要持久化；
votedFor，投票信息，需要持久化；
log，日志，需要持久化；
state，节点状态，三种 Follower, Candidate, Leader；

Candidate 变量：

votesResponded，候选者在当前任期收到的 RequestVote 响应；
votesGranted，候选者收到来自 RequestVote 的投票；

Leader 变量：

nextIndex，发送给 Follower 的下一个日志；
matchIndex，领导者用来统计计算 commitIndex。如果超过半数节点的 matchIndex >= N 且任期一致，那么可以更新 commitIndex = N。

动作

Raft 的动作较多，我们重点看节点是如何处理 RequestVote 和 AppendEntries 的。

领导者选举的关键就是判断 logOk 和 grant。logOk 需要找出日志最新并且最完整的节点，最新就是任期最大，最完整就是日志最长。grant 就是在 logOk 正确的情况下，需要任期相同，并且没投过票或投票给请求节点。

之后，候选者收集请求响应，判断是否收到超过半数的选票，来决定是否成为领导者。

HandleAppendEntriesRequest 比较长，我们一步步来看。

首先，根据 Receive(m)，如果消息体中的任期大于当前节点的任期，会先调用 UpdateTerm(i, j, m) 更新一些变量。之后，消息体中的任期小于等于当前节点的任期的情况。

这里的 logOk 与 RequestVote 的检查不同，主要进行日志的一致性检查，AppendEntries 请求会包含新日志之前一条日志的索引(记为 prevLogIndex)和任期(记为 prevLogTerm)；跟随者收到请求后，会检查自己最后一条日志的索引和任期号是否与 prevLogIndex 和 prevLogTerm 相匹配，匹配则接收该记录；否则拒绝。

该流程被称为一致性检查，如下图所示。