raft学习（15）——安全性证明

raft学习（15）——安全性证明

5.4.3 安全性讨论

这里就是想证明未来的leader肯定都包含以前的leader commit 的所有log entry

给定了完整的raft算法，我们可以更加准确地讨论leader的完整性是成立的（这个讨论时基于safety proof的；看9.2节）。我们假设leader completeness性质不成立，那么我们就要证明一个矛盾。假设term T的leader在它的term里提交了一个log entry， 但这个log entry并没有存储在未来term的leader中。我们考虑最小的term U > T其中U的leader并没有存储这个entry

1.在leaderU进行election的时候，这个committed entry必须absent（因为leader从不delete或overwrite）
2.leaderT复制了entry给大多数的cluster，然后leaderU收到了大多数cluster的vote。因此，至少有一个voter时既收到leaderT的entry也给leaderU投票的，正如图9所示，这些vote就是形成一个矛盾的关键。

图9：如果S1（term T的leader）在它的term里提交了一个新的log entry，然后S5是termU中被选中的leader，那么一定存在这个S3又收到了S1的log又投票给S5，这就是传说中的抽屉原理！！！

3.voter必须先接受了leaderT的ecommitted entry然后再投票给leaderu，否则他就会拒绝leaderT的appendentries request（因为它现在的term会比T更高）

4.当voter给leaderu投票的时候，它会store住entty，因为每一个中间的leader都包含了entry，leader从不remove entries，然后follower只把和leader不一样的entries remove掉

5.voter把它的vote给了leaderu，所以leaderu的log一定是up-to-date和voter的，这就出现了第一个矛盾！！（因为voter有leaderT的log，但leaderU没有！）

6.首先，如果voter和leaderu共享相同的最后的log term，那么leaderu的log至少和voter的一样长，所以leaderu的log就会包含voter log里面的所有内容。这是一个矛盾，因为voter有leaderT的log，但leaderU没有！

7.否则，leaderU的最后的log term必须大于voter的。进而，U肯定大于T的log term，因为voter的最近的log term至少也是T（因为它包含了term T的commited entry）。那个leaderU最后的一个log entry肯定是某个T之后的leader给他的，那这个leader一定也会包含T的commited entry啊！所以，通过log matching原则，leaderu的log一定会包含committed entry，也是一个矛盾！

8.这就完善了整个矛盾。因此，那些具有比T term更高得leader一定会包含termT所有的entries并是在TermT提交的

9.这个log matching 性质保证了未来的leader也会包含已经committed过的entries

考虑倒leader 完整性性质，我们可以证明state machine 安全性，这个表述了如果一个server应用了给定index的log entry给它的state machine， 没有其他server还会应用同一个index的其他log entry。这时候一个server应用了一个log entry给state machine，它的log必须是和leaders 的log一样的，然后这个entry也是committed的。现在考虑任何server应用一个给定log index的最低term；log 完整性质保证所有有更高term的leader都会存有相同的log entry，所以server应用后面terms的index将会应用相同的value。因此，state machine safety性质成立。

最后，raft需要servers去应用log index order中的entries。和state machine safety性质结合，这意味着所有的server都会apply 相同的log entries序列（对他们的state machine），并且以同样的顺序。