paxos草案2

master
yezhengmao 2023-05-08 17:03:07 +08:00
parent cc4691bfdd
commit e124d4198b
1 changed files with 7 additions and 2 deletions

View File

@ -1,6 +1,6 @@
+++ +++
title="Paxos算法详解" title="Paxos算法详解"
date="2023-05-02" date="2023-05-08"
+++ +++
## 前言 ## 前言
@ -84,7 +84,12 @@ date="2023-05-02"
> 若某轮提议达成一致,成为已决决议,则任意提议号大于该提议的决议都与其相同 > 若某轮提议达成一致,成为已决决议,则任意提议号大于该提议的决议都与其相同
证明(反证法): 证明(反证法):
1. 1. 假设在已决决议提议之后存在提议的决议与已决决议不同,取这些提议中提议号最小的提议,记为提议甲。
2. 提议甲中的法定节点集一定与已决决议投票节点集有交集(约束Ⅱ保证法定节点集之间有交集,已决决议保证法定节点集是投票节点集的子集)。
3. 提议甲的法定节点集中一定存在节点在大于等于已决决议提议号小于提议甲提议号之间进行了投票由2推出至少存在一个节点即在已决决议提议中进行投票的节点。取这些投票所对应的提议号距提议甲最近的一次决议记为决议乙。
4. 由约束Ⅲ的存在,决议甲的法定节点集在决议乙中进行了投票,则决议甲等于决议乙,两则与已决决议不等。
5. 违法决议甲是不同于已决决议中拥有最小提议号的假设。
## 参考 ## 参考
* Leslie, Lamport. "The part-time parliament." ACM Trans. on Computer Systems 16 (1998): 133-169. * Leslie, Lamport. "The part-time parliament." ACM Trans. on Computer Systems 16 (1998): 133-169.
* Lamport, Leslie. "Paxos made simple." ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) (2001): 51-58. * Lamport, Leslie. "Paxos made simple." ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) (2001): 51-58.