Raft正确性证明以及流程说明

正确性证明

Raft 算法正确性的核心在于证明 状态机安全性 (State Machine Safety)：如果一个节点已经将给定索引位置的日志条目应用到了其状态机中，则其他任何节点都不会在该索引位置应用不同的日志条目。

证明过程建立在五个严格约束的单调递进属性之上。

1. 选举安全性 (Election Safety)

• 定义：在任意一个特定的任期 (Term) 内，最多只能选出一个 Leader。
• 证明：一个 Candidate 必须获得集群中多数派 (Majority) 的选票才能成为 Leader。由于集群中任意两个多数派必然存在至少一个交集节点，而每个节点在一个 Term 内只能投出一票，因此交集节点不可能同时投票给两个 Candidate。故同一个 Term 内不可能产生两个 Leader。得证。

2. Leader 日志只增不减 (Leader Append-Only)

• 定义：Leader 永远不会覆盖或者删除自己日志中的条目，只执行追加操作。
• 证明：由 Raft 协议规则硬性约束，Leader 节点不暴露任何删除自身日志的接口。得证。

3. 日志匹配特性 (Log Matching)

• 定义：如果两个节点的日志中有两个条目具有相同的索引 (Index) 和任期 (Term)，那么这两个节点在该索引及之前的所有日志条目完全相同。
• 证明：通过数学归纳法及 AppendEntries RPC 的一致性检查机制保证。Leader 发送新日志时会携带前一条日志的 $(Index, Term)$。如果 Follower 发现不匹配，会拒绝接收，Leader 则会递减 Index 重新发送，直到找到共同匹配点再进行强制覆盖。得证。

---

4. Leader 完整性 (Leader Completeness) —— 【证明核心】

• 定义：如果一个日志条目在某个 Term 中被提交 (Committed)，那么该条目必然出现在未来所有拥有更高 Term 的 Leader 的日志中。
• 证明 (反证法)： 假设日志条目 $e$ 在 $Term\ T$ 被 Leader $L_T$ 提交，但在未来的某个 $Term\ U$ ($U > T$) 中，Leader $L_U$ 的日志里没有条目 $e$。

1. 设 $Term\ U$ 是首个满足“Leader 缺失 $e$”条件的任期。
2. 因为 $e$ 在 $Term\ T$ 被提交，意味着 $e$ 已经被复制到了一个多数派节点集合 $S_1$ 中。
3. $L_U$ 能够当选 $Term\ U$ 的 Leader，意味着它获得了另一个多数派节点集合 $S_2$ 的投票。
4. 必然存在交集节点 $V$，满足 $V \in S_1 \cap S_2$。节点 $V$ 既拥有条目 $e$，又把票投给了 $L_U$。
5. 根据 Raft 的投票规则限制 (RequestVote RPC)：选民只会把票投给日志至少和自己一样新的 Candidate（比较最后一条日志的 Term，若 Term 相同则比较 Index 长度）。
6. 因为 $V$ 投票给了 $L_U$，所以 $L_U$ 的日志必须比 $V$ 的日志更新或一样新。
7. 节点 $V$ 包含 $Term\ T$ 提交的条目 $e$。由于我们假设 $Term\ U$ 是首个缺失 $e$ 的任期，在此之前的所有 Leader 都包含了 $e$，因此 $V$ 最后一条日志的 $Term \ge T$。
8. 如果 $L_U$ 的日志比 $V$ 新，则 $L_U$ 最后一条日志的 Term 必须大于或等于 $V$ 最后一条日志的 Term（即 $\ge T$）。根据上述假设（$Term\ U$ 是首个缺失 $e$ 的），$L_U$ 如果拥有 $Term \ge T$ 的日志，根据日志匹配特性，它就必须包含 $Term\ T$ 的条目 $e$。
9. 这与假设“$L_U$ 没有条目 $e$”绝对矛盾。因此，假设不成立。得证。

---

5. 状态机安全性 (State Machine Safety)

• 证明：假设节点 A 在 Index $i$ 处将日志条目 $e$ 应用于状态机。这说明 $e$ 已经被标记为 Committed。 根据 Leader 完整性 (属性 4)，未来所有的 Leader 都将包含该日志 $e$ 在 Index $i$ 的位置。 由于 Leader 拥有绝对独裁权（强制 Follower 复制自己的日志），并且永远不改变已有日志（属性 2），后续所有节点在 Index $i$ 处只可能接收到日志 $e$。因此，没有其他节点会在 Index $i$ 处应用与 $e$ 不同的日志。得证。

节点视角的流程说明

Raft 算法的运转依赖于两种核心 RPC（远程过程调用）消息和三种节点角色的状态机转换。

为了不讲废话，我们先定义好系统中流通的两种核心消息结构，然后直接代入到三种角色的第一视角。

一、 核心消息结构 (RPCs)

1. RequestVote (请求投票 RPC) Candidate 发起选举时使用。

• term: Candidate 当前的任期号。
• candidateId: 请求投票的 Candidate 的 ID。
• lastLogIndex: Candidate 最后一条日志的索引。
• lastLogTerm: Candidate 最后一条日志的任期号（这俩参数用于比较谁的日志更新）。
• 返回值: term (接收方的当前任期)，voteGranted (布尔值，是否同意投票)。

2. AppendEntries (追加日志 / 心跳 RPC) Leader 复制日志和发送心跳时使用（日志条目为空即为心跳）。

• term: Leader 当前的任期号。
• leaderId: Leader 的 ID（让 Follower 知道应该把客户端请求重定向给谁）。
• prevLogIndex: 新日志条目前一条日志的索引。
• prevLogTerm: prevLogIndex 对应的任期号（这俩参数用于日志一致性检查）。
• entries[]: 需要被存储的日志条目（心跳时为空）。
• leaderCommit: Leader 已提交的最高日志索引。
• 返回值: term (接收方的当前任期)，success (布尔值，Follower 内部是否包含了匹配 prevLogIndex 和 prevLogTerm 的日志)。

---

二、 Raft 运转流程：第一人称视角

1. Follower（跟随者）视角：安静的打工人

核心任务：被动接收指令，维持状态，伺机篡权。

• 初始化：我刚启动，或者刚从其他状态退下来，我是个纯打工人。我启动我的选举超时定时器（一个随机值，比如 150-300ms）。

• 收到 AppendEntries (Leader 来活了/心跳)：

• 如果你带的 term 比我的小，滚（返回 false），你不配当 Leader。

• 如果你带的 prevLogIndex 和 prevLogTerm 跟我的本地日志对不上，说明我的日志缺失或有冲突，报错（返回 false）。

• 如果对上了，我把你发来的 entries[] 追加到我的日志里（如果有冲突日志就覆盖）。

• 如果你告诉我 leaderCommit 更新了，我也更新我的本地 commitIndex，把日志应用到我的状态机。

• 最重要的是：只要收到合法的 AppendEntries，我就重置我的选举超时定时器，继续安心打工。

• 收到 RequestVote (有人来拉票)：

• 如果你带的 term 比我的小，滚，不投。

• 如果我这个任期内已经投过票了，滚，不投。

• 看看你的 lastLogIndex 和 lastLogTerm。如果你的日志没有我的新，滚，不投。

• 如果一切都没问题，我把票投给你（voteGranted=true），并重置我的选举超时定时器。

• 突发情况：如果我的选举超时定时器归零了（说明太久没收到 Leader 心跳了），老板肯定挂了。我要造反！切换为 Candidate 状态。

---

2. Candidate（候选者）视角：野心勃勃的政客

核心任务：拉票，不择手段成为 Leader。

• 起义瞬间：

• 我立刻把我的当前任期号 term + 1。

• 我先给自己投一票。

• 我重置我的选举定时器。

• 我向集群内所有其他人疯狂发送 RequestVote RPC。

• 等待结果的煎熬（有三种结局）：

• 结局 A（上位成功）：我收到了集群内多数派（Majority）的选票！我立刻切换为 Leader 状态。

• 结局 B（被人截胡）：我正在等选票，突然收到别人发来的 AppendEntries。我一看他的 term 大于或等于我的 term，说明人家已经合法当选了。我认怂，立刻退回 Follower 状态。

• 结局 C（选票瓜分）：我的选举定时器又超时了，但此时我既没拿到多数票，也没新 Leader 压制我（比如有几个 Candidate 同起事，选票平分了）。我只能把 term 再 + 1，重新发起一轮选举。

---

3. Leader（领导者）视角：独裁的暴君

核心任务：接客，发号施令，强推日志，镇压叛乱。

• 登基瞬间：

• 我立刻向全员发送空的 AppendEntries（心跳），宣示主权，防止他们超时造反。

• 我为每个 Follower 维护两个数组：nextIndex[] (我要发给他的下一条日志索引，初始化为我最后一条日志+1) 和 matchIndex[] (他已经跟我同步的最高日志索引，初始化为 0)。

• 接客与推日志（收到客户端请求）：

• 我把客户端发来的指令写进我自己的本地日志。

• 我向所有 Follower 并发发送带有这段日志的 AppendEntries。

• 处理 Follower 的回复：

• 如果 Follower 返回 success=true：太好了，我更新他的 nextIndex 和 matchIndex。

• 如果超过半数的节点都同步成功了：我把这条日志标记为 Committed，应用到我的状态机，然后给客户端返回成功。

• 如果 Follower 返回 success=false（他的日志跟我的脱节了）：我把他的 nextIndex 减 1，带着更早的日志再次发 AppendEntries，一直倒退尝试，直到找到我们日志完全一致的地方，然后强制用我的日志覆盖他后面的所有垃圾日志。

• 日常维稳：必须按时（远小于选举超时时间）疯狂发空 AppendEntries 给所有 Follower。

• 退位：如果在任何时候（无论是收到 RPC 还是别人的回复），我发现里面带了一个比我现在的 term 更大的任期号（说明网络分区恢复，出现了新朝代的 Leader），我立刻认清现实，乖乖降级为 Follower。