BasicPaxos协议
赵星宇
本文是学习《Paxos理论介绍(1): 朴素Paxos算法理论推导与证明》的学习总结
其解决的问题是确定一个值。
一、数学推倒:
参数定义:
B 一轮投票
Bdec 这轮投票的目标提议
Bqrm 一轮投票获得成功所需要的投票者集合
Bvot 这轮投票实际的投票者集合
Bbal 这轮投票的编号
β 多轮投票
MaxVote(Bbal, Bqrm, β) Bqrm中每一个投票者的所有投票中编号比Bbal小的最大编号的投票
MaxVote(Bbal, Bqrm, β)dec 那个投票的提议
MaxVote(Bbal, Bqrm, β)bal 那个投票的所属轮次编号
约束条件:
B1(β) = ∀B, B’∈β: (B≠B’)=>(Bbal≠B’bal)
约束1 对属于多轮投票β的两轮投票B, B’,如果B和B’不是同一轮投票,则他们两个编号的Bbal和B’bal不相等。也就是说每轮投票有自己唯一的编号。
B2(β) = ∀B, B’∈β: Bqrm∩B’qrm≠∅
约束2 对属于多轮投票β的两轮投票B, B’,则他们两个的成功所需要的投票者集合Bqrm与B'qrm的交集不为空集。也就是说只有多数派进行了投票,本轮投票才算成功。
B3(β) = ∀B∈β: (MaxVote(Bbal, Bqrm, β)bal≠-∞) => (Bdec=MaxVote(Bbal, Bqrm, β)dec)
约束3 对于一轮编号为Bbal的投票,投票的多数派中投过的所有投票中如果存在编号比Bbal小的最大编号的投票,则将这个投票的提议作为本轮投票的提议。
证明:投票B已经投票通过后,投票B’满足B’bal>Bbal,则B’dec=Bdec。
1.假设B’bal是大于Bbal的最小编号。
2.因为B已经投票通过,因而B’qrm必然包含Bvot的至少1个元素。(B2(β))
3.MaxVote(B’bal, B’qrm, β)bal=Bbal。(1,2)
4.B’dec = MaxVote(B’bal, B’qrm, β)dec=Bdec(B3(β),3)
5.对于B’bal是大于Bbal的一般情况,因为中间的提议全是Bdec,因而B’dec=Bdec得证。(4)
二、算法提出:
伪代码:
// 提议者
class Proposer {
static int lastPrepareB = 0; // 所有Proposer最近发出的提议编号
int maxb = 0; // MaxVote(Bbal, Bqrm, β)bal
T v = null; // 投票提议
int b = 0; // 投票编号
int qrm = N/2+1;
int prepareOkNum = 0;
int acceptOkNum = 0;
void Start(T x) {
b = ++lastPrepareB;
v = x;
Prepare(b);
}
void OnPrepareResponse(int ok, int ab, T av) {
if (!ok) return;
if (ab > maxb && av != null) {
maxb = ab;
v = av;
}
prepareOkNum++;
if (prepareOkNum >= qrm) {
Accept(b, v);
}
}
void OnAcceptResponse(int ok) {
if (!ok) return;
acceptOkNum++;
if (acceptOkNum >= qrm) {
done(b, v);
}
}
}
// 投票者
class Acceptor {
int pb = 0; // 承诺不再接收编号小于pb的投票
int ab = 0; // 最大编号投票的编号
T av = null; // 最大编号投票的提议
void OnPrepare(int b) {
if (b >= pb) {
pb = b;
PrepareResponse(ok, ab, av);
} else {
PrepareResponse(reject, 0, null);
}
}
void OnAccept(int b, T v) {
if (b == pb) {
ab = b;
av = v;
AcceptResponse(ok);
} else {
AcceptResponse(reject);
}
}
}