21.7 Raft:安全性证明

一句话

Raft 的安全性是一条四步链——多数派相交 ⇒ 一个任期一个 leader;AppendEntries 的前缀检查 ⇒ 日志匹配;选举限制 ⇒ 新 leader 含所有已提交条目;前三条 ⇒ 不会有两个节点在同一位置应用不同命令;"只提交当前任期的条目"是这条链上唯一需要额外打补丁的地方。

五条安全性性质

性质 内容 由哪条机制保证
选举安全(Election Safety) 一个任期最多一个 leader 一个任期一票 + 多数派相交
leader 只追加(Leader Append-Only) leader 不覆盖、不删除自己的日志 leader 只 append
日志匹配(Log Matching) 两个日志有相同的 (index, term) ⇒ 之前所有条目相同 AppendEntries 的 prevLogIndex/prevLogTerm 检查
leader 完整性(Leader Completeness) 已提交条目一定出现在之后所有 leader 的日志里 选举限制(日志至少一样新)
状态机安全(State Machine Safety) 同一 index 不会有两个节点 apply 不同命令 前四条合起来

记住这条链的依赖方向:前三条是"局部规则",第四条是"归纳",第五条是"结论"。面试里被问"Raft 为什么安全",按这个顺序答就不会散。

证明骨架

引理 1(选举安全):同一任期不可能有两个 leader。 证明:成为 leader 需要多数派投票,且每个节点在同一 term 只投一票;两个 leader 需要两个多数派,由相交引理(21.2 Quorum 与 W + R > N 的证明)它们必有交集,交集中的节点投了两次票,矛盾。∎

引理 2(日志匹配):若两个日志在 (index, term) 相同,则它们 index 之前的全部条目相同。 证明:对 index 归纳。index = 0 平凡成立。设 (i, t) 相同且 i-1 之前相同。产生 (i, t) 的那次 AppendEntries 一定带着 prevLogIndex = i-1, prevLogTerm = t',接收方只有在自己的 i-1 处也是 t' 时才接受,所以写入后 i-1 也相同;再由归纳假设,i-1 之前全相同。∎

引理 3(leader 完整性):若某条目在 index i 被提交,则之后任意 term 的 leader 的日志都包含它。 证明(归纳,按 leader 的 term 递推):设条目在 term T 提交,落在多数派 Q_c 上。考虑任意 term U > T 的 leader L_U,它由多数派 Q_v 选出。

  • Q_c ∩ Q_v ≠ ∅(相交引理),取其中节点 x:x 有该条目,且在投票时没有删除过它(已提交条目只会在 leader 日志里,AppendEntries 的删除只发生在"与 leader 冲突",而 leader 若没有该条目,x 的日志就更"新",不会投给它)。
  • L_U 要当选,必须拿到 Q_v 中多数票;而 x 只会投票给"日志至少和自己一样新"的候选人。x 有 index i(term T),所以 L_U 的 lastTerm/lastIndex 必须 ≥ 它,即 L_U 的日志至少覆盖到 i。
  • 再由引理 2(日志匹配),L_U 在 i 处的条目与 x 在 i 处的条目相同。 归纳成立。∎

定理(状态机安全):不会有两个节点在同一 index apply 不同命令。 证明:设 (i, t) 与 (i, t') 都被 apply,则它们都被某个 leader 提交过。由引理 1,提交它们的是不同 term 的 leader;由引理 3,后一个 leader 的日志必包含前一个已提交的 (i, t);但一个 leader 在 index i 只能有一条日志,所以 t' = t,命令也相同(引理 2)。∎

🔑 这条链里最容易断的是引理 3 的第二步:x "只投给不比自己旧的候选人"。如果投票比较写错(先比长度、或只比 lastIndex),x 就可能投给一个缺条目的候选人,引理 3 直接失效。

图 8:为什么"多数派复制"不足以提交旧任期条目

Raft 论文用 Figure 8 说明:leader 不能通过"某条旧任期条目已在多数派上"就判定它已提交。下面把这段时序完整跑了一遍(5 节点、每步打印日志的 term 序列):

package main

import "fmt"

type srv struct {
	name string
	log  []int // 只记每个位置的 term
}

func last(l []int) (term, idx int) {
	if len(l) == 0 {
		return 0, 0
	}
	return l[len(l)-1], len(l)
}

// Raft 的选举限制:候选人的日志必须「至少一样新」
func upToDate(voter, cand []int) bool {
	vt, vi := last(voter)
	ct, ci := last(cand)
	if ct != vt {
		return ct > vt
	}
	return ci >= vi
}

func show(step string, ss []srv) {
	fmt.Printf("%s\n", step)
	for _, s := range ss {
		fmt.Printf("  %s: %v\n", s.name, s.log)
	}
}

func main() {
	ss := []srv{
		{"S1", []int{1, 2}},
		{"S2", []int{1, 2}},
		{"S3", []int{1}},
		{"S4", []int{1}},
		{"S5", []int{1}},
	}
	show("(a) S1(term 4)把 index 2 的旧任期条目复制给 S2:", ss)

	// (b) S5 当选 term 3(S3、S4 投票),追加并复制 index 2、3(都是 term 3)
	ss[4].log = []int{1, 3, 3}
	ss[2].log = []int{1, 3, 3}
	ss[3].log = []int{1, 3, 3}
	show("\n(b) S5 当选 term 3,在 index 2、3 写入 term 3 的条目并复制给 S3、S4:", ss)

	// (c) S1 重启,term 4 当选(S2、S3、S4 投票),把 index 2 的 term 2 条目复制给 S3
	ss[2].log = []int{1, 2}
	show("\n(c) S1 当选 term 4,把 index 2(term 2)复制给 S3 → {S1,S2,S3} 三个节点都有它:", ss)

	// 规则 A:多数派复制即提交
	fmt.Println("\n规则 A(错):「多数派已复制」就提交 → index 2(term 2)被判为已提交")

	// (d) S5 重启并竞选 term 5
	fmt.Println("\n(d) S5 竞选 term 5,用「日志至少一样新」逐票判定:")
	// S1 再次崩溃,不参与投票
	n := 1
	yes := []string{"S5(自己)"}
	candLog := ss[4].log
	for i, s := range ss {
		if i == 0 || i == 4 {
			continue
		}
		ok := upToDate(s.log, candLog)
		fmt.Printf("  %s 的日志 %v vs S5 的 %v → %v\n", s.name, s.log, candLog, ok)
		if ok {
			n++
			yes = append(yes, s.name)
		}
	}
	fmt.Printf("  得票 %d/5(%v)→ %s\n", n, yes, map[bool]string{true: "当选 term 5", false: "选不上"}[n >= 3])

	// S5 当选后用自己的日志覆盖 index 2
	if n >= 3 {
		for i := range ss {
			if i == 0 {
				continue
			}
			if len(ss[i].log) >= 2 && ss[i].log[1] != 3 {
				fmt.Printf("  覆盖 %s 的 index 2:term %d → term 3\n", ss[i].name, ss[i].log[1])
				ss[i].log[1] = 3
			}
		}
	}
	show("\n最终状态(规则 A 下,已被判定「提交」的 index 2 term 2 被覆盖):", ss)
	fmt.Println("\n规则 B(对):「只有当前任期的条目才能靠多数派直接提交」")
	fmt.Println("  (c) 时 leader 的 term 是 4,而 index 2 的 term 是 2 → 不算提交;")
	fmt.Println("  要等 S1 在 term 4 写入并提交一个新条目,index 2 才被「间接」提交。")
	fmt.Println("  图里 S1 在做到这件事之前就崩了 → index 2 从未提交 → (d) 的覆盖合法,不变式成立。")
}

输出(本机实测):

(a) S1(term 4)把 index 2 的旧任期条目复制给 S2:
  S1: [1 2]
  S2: [1 2]
  S3: [1]
  S4: [1]
  S5: [1]

(b) S5 当选 term 3,在 index 2、3 写入 term 3 的条目并复制给 S3、S4:
  S1: [1 2]
  S2: [1 2]
  S3: [1 3 3]
  S4: [1 3 3]
  S5: [1 3 3]

(c) S1 当选 term 4,把 index 2(term 2)复制给 S3 → {S1,S2,S3} 三个节点都有它:
  S1: [1 2]
  S2: [1 2]
  S3: [1 2]
  S4: [1 3 3]
  S5: [1 3 3]

规则 A(错):「多数派已复制」就提交 → index 2(term 2)被判为已提交

(d) S5 竞选 term 5,用「日志至少一样新」逐票判定:
  S2 的日志 [1 2] vs S5 的 [1 3 3] → true
  S3 的日志 [1 2] vs S5 的 [1 3 3] → true
  S4 的日志 [1 3 3] vs S5 的 [1 3 3] → true
  得票 4/5([S5(自己) S2 S3 S4])→ 当选 term 5
  覆盖 S2 的 index 2:term 2 → term 3
  覆盖 S3 的 index 2:term 2 → term 3

最终状态(规则 A 下,已被判定「提交」的 index 2 term 2 被覆盖):
  S1: [1 2]
  S2: [1 3]
  S3: [1 3]
  S4: [1 3 3]
  S5: [1 3 3]

规则 B(对):「只有当前任期的条目才能靠多数派直接提交」
  (c) 时 leader 的 term 是 4,而 index 2 的 term 是 2 → 不算提交;
  要等 S1 在 term 4 写入并提交一个新条目,index 2 才被「间接」提交。
  图里 S1 在做到这件事之前就崩了 → index 2 从未提交 → (d) 的覆盖合法,不变式成立。

为什么 S5 能当选?因为 S2、S3 的 lastTerm 是 2,低于 S5 的 3 —— 按"至少一样新"的规则,它们必须投赞成。于是规则 A 判定为"已提交"的条目,被一个合法当选的 leader 覆盖了。

规则 判定依据 图 8 里 index 2 (term 2) 结果
A(错) 多数派已复制 {S1,S2,S3} → 已提交 被 S5 覆盖 → 违反不变式
B(对) 多数派 + 当前任期 term 2 ≠ term 4 → 未提交 覆盖合法 → 不变式成立

补丁的实际形式:leader 只把"当前任期的条目"按多数派直接提交;旧任期条目在"某个当前任期条目提交"时被间接提交(因为日志是前缀关系)。这就是新 leader 上任要先提交一条 no-op 的原因。

证明成立依赖的工程前提

前提 违反的后果 怎么保证
currentTerm / votedFor / 日志 持久化 重启后重复投票或丢日志 → 引理 1/3 失效 每次变更先 fsync 再回复
follower 先落盘再 ACK "多数派持久化"变成"多数派内存里有" 写日志 → fsync → 回成功
同一 term 只投一票(含重启后) 一个 term 两个 leader votedFor 持久化
提交判定用当前任期 图 8 覆盖 代码里显式判断 log[ci].term == currentTerm
日志匹配检查包含 prevLogTerm 分叉被静默接受,日志前缀性质失效 不能只比 prevLogIndex

边界:什么会打破这套证明

场景 为什么会破 正确做法
直接切换配置(如 3→5 一次改两个) 新旧配置的多数派可能不相交 → 两个 leader 一次改一个,或联合共识(21.8 Raft:成员变更与快照)
快照不记录 lastIncludedTerm 恢复后无法校验 prevLogTerm,日志匹配断裂 快照必须存 lastIncludedIndex + lastIncludedTerm
用未提交的日志覆盖已提交日志("冲突就截断"滥用) 违反引理 3 只有 leader 能决定覆盖,且 leader 必含已提交条目
把 commitIndex 落盘当真相 重启后可能"提交"了实际未提交的条目 用日志 + 多数派重新推导
非确定性状态机 同一日志在不同节点产生不同状态 状态机必须确定性(时间、随机数要注入)

反模式

反模式 后果
用"多数派有"直接提交旧任期条目 图 8:已提交条目被覆盖,出现"回滚"
投票比较先比长度、不看 term 落后候选人当选,引理 3 失效
只在内存里记 votedFor 崩溃重启后一 term 投两票 → 双 leader
follower 先 ACK 后 fsync 掉电丢已提交日志
新 leader 不提交 no-op 就开始服务读 读到落后状态,破坏线性一致
把"安全性证明"当成"实现正确" 证明假设了持久化与单调时钟等工程前提,代码写错照样出事

自检

Q1 用一句话说清"为什么一个任期最多一个 leader",并指出它用了哪条更基础的结论。

▸ 答案:两个 leader 需要两个多数派各自投票,而每个节点在一个任期只投一票;两个多数派必相交(2q > N),交集节点被要求投两票,矛盾。它依赖的是 21.2 的相交引理,与 Raft 的具体实现无关——任何多数派协议都共享这一步。

Q2 图 8 的反例里,S5 凭什么能当选?它违反了哪条规则吗?

▸ 答案:没有违反任何规则。S5 的 lastTerm 是 3,S2/S3 的 lastTerm 是 2,S4 与它相同(3);按"日志至少一样新",S2、S3、S4 都必须投赞成,加上自己共 4 票,合法当选。问题不在选举,而在规则 A 的提交判定:它把"多数派复制了旧任期条目"当成"已提交",而这个判定没有经过当前任期条目的确认,所以随后被合法当选的 S5 覆盖。

Q3 为什么"只提交当前任期的条目"不会导致旧条目永远无法提交?

▸ 答案:因为日志是前缀关系。leader 一旦在 term T 提交了 index j 的条目,那么 j 之前的所有条目(包括旧任期的)都随之确定——它们的复制位置必然 ≥ j,而 j 已经有多数派。所以旧条目不是"不能提交",而是"不能单独凭多数派提交",要搭当前任期条目的顺风车。新 leader 提交 no-op 就是这个顺风车。

Q4 日志匹配性质里,只检查 prevLogIndex 而漏掉 prevLogTerm 会怎样?举一个能通过检查的分叉。

▸ 答案:会接受一个"长度够但内容不同"的日志。例如 follower 在 index 3 是 (t3, x=9),leader 在 index 3 是 (t2, c=3):只比 index 时,leader 发 prevLogIndex=3 就能通过,随后把 index 4 起的条目接在一条错误的历史后面,此后两个节点的日志在 index 3 处分叉却都"合法"。prevLogTerm 是唯一能区分同长度不同历史的信息,所以必须一起比。

Q5 证明里假设了哪些"代码之外"的东西?挑两个说说违反后的现象。

▸ 答案:① 持久化:currentTerm、votedFor、日志必须先落盘再回复;违反后重启会重复投票(双 leader)或丢已提交日志(数据回滚)。② 确定性状态机:所有副本对同一日志必须产生同一状态;违反后(例如状态机里用了本地时间/随机数)会看到"日志一致但数据不一致",且无法通过重放修复。另外还有"fsync 真落盘""时钟只用于超时、不用于定序"等前提。

关联