论文使用了反证法证明了Leader Completeness特性,进而证明了State Machine Safety特性。
这个证明过程相对较绕,但是仔细阅读仍是可以理解,通过该证明保证了raft协议数据的正确性
需要证明问题:
未来Leader一定包含以前Leader commit的日志(Leader Completeness)
证明过程:
使用反正法推出矛盾,进而证明Leader Completeness的正确性
假设存在未来的Leader不包含以前Leader commit的日志,即:
term = T期间Leader commit了entry(我们就叫entryM吧),在term = U期间的Leader不包含这个entry(U为最小的比T大的不包含该entry的Leader):
LeaderU在发起election时,一定不包含entryM;
因为LeaderU成为Leader后,不会删除或者覆盖自己的日志。
LeaderT将entryM复制给大部分的机器,同时LeaderU收到了大部分机器的选票,那么就至少存在一个机器,即包含 了entryM,又投票给LeaderU;
即为上图中的S3。这点也很好理解,因为对于个数2n+1的集群,这两个行为都是需要n+1个节点参与,那么就必然会存在交集。
这个投票者(S3)必然是收到了LeaderT复制entryM的AppendEntry RPC,然后再收到LeaderU的RequestVote RPC;
因为如果是先收到RequestVote的话,自身的更新currentTerm = U,又因为U > T, 那么就无法执行来自于LeaderT的AppendEntry
这个投票者(S3)给LeaderU投票时,就一定包含了entryM;
这一点稍微有点绕。因为LeaderU是最小不包含entryM的Leader(我们的假设),所以在T~U期间的Leader(无论Leader切换过多少次)是一定包含entryM的。而无论S3之前经历了什么角色,如果是Leader,那么它就包含entryM;如果是Follower,那么日志会被同步成和Leader一样。
这个点也是下面导出矛盾的关键。
这个投票者(S3)给LeaderU投票,那么LeaderU的日志一定比它新的;
这个就是election restriction。我们在回顾一下,LeaderU日志比voter新的定义:
1).最后一个entry的term不同时,term大的为新;
2).最后一个entry的term相同时,index大的为新;
下面会列举上面两种可能都不成立。
如果它们最后一个entry的term相同,那么LeaderU的log长度至少和S3一样长,但是S3包含了entryM,但是LeaderU不包含entryM,所以LeaderU的日志长度不可能大于或者等于S3的日志长度。所以这点不成立。
这里其实有需要思考的隐藏点:有没有可能LeaderU缺少了entryM,但是entryM后面的entries又比S3多了一个,导致了最终它们的日志长度是一样的?
答案是不会的。因为如果LeaderU在entryM后面追加其他日志entry了的话,根据一致性检查原则,entryM就一定会被追加到LeaderU的日志中。
还有一种可能是,LeaderU的最后一条日志的term比S3大。我们知道,S3的最后一条日志的term至少是T, 也就是说LeaderU的最后一条日志的term是大于T,那么当LeaderU被追加这条大于T的entry时(彼时LeaderU的还不是Leader,还是一个Follower),依据一致性检查,就一定会被彼时的Leader追加entryM(因为依据假设,T~U期间的Leader,都含有entryM)。
6/7两点说明了LeaderU的日志无法比S3的新,也就是说LeaderU无法当选,最终反证不成立,进而证明了Leader Completeness的正确性。
最后Leader Completeness保证了State Machine Safety。 因为一个节点应用了一个entry,那么它的log就一定和它的Leader是一致的且这个entry是commited的。Leader Completeness保证了更高term的Leader会存储相同的entry,因此其他节点在新的term应用这个日志将会应用相同的值。
总结至此,关于raft的几点特性Election Safety, Leader Append-only, Log Matching, Leader Completeness, State Machine Safety全部讨论完毕。
理解raft协议,需要对上述的五个特性以及它们的原理实现有深刻的理解。



