Page 178 - 《软件学报》2021年第6期

1752 Journal of Software 软件学报 Vol.32, No.6, June 2021

如果回复中不包含任何提议,则提议者可以任选一个值(通常是该提议者收到的用户命令);否则,
提议者选择编号最大的回复对应的值.设提议者选择的值为 v,则提议者向所有接受者发送内容
为〈b,v〉的 Accept 请求;
¾ 子阶段 Phase2b:接受者收到编号为 b 的 Accept 请求.如果接受者没有收到过编号大于 b 的请求,
则可以接受该 Accept 请求;否则,接受者忽略该 Accept 请求.
1.4 Multi-Paxos协议
Multi-Paxos 针对每个日志项运行一个独立的 Paxos 实例,从而支持副本服务器对日志(日志项的序列)达成
共识.由于各个 Paxos 实例是并行独立运行的,Multi-Paxos 允许乱序提交用户命令.也就是说,它允许副本服务器
先就编号较大的日志项对应的用户命令达成共识,而无需等待之前的日志项完成共识.
在实际实现时,常常通过将 phase1 的消息分批(batching)的方式提高性能.此时,系统包含一个恢复阶段,恢
复阶段本质上是将不同实例的 phase1 消息集中处理的过程.
模块 MultiPaxos 描述了 Multi-Paxos 协议.其中包括 3 个常量.
• Acceptors:所有接受者构成的集合;
• Value:所有可能的提议值构成的集合;
• Nil:特殊记号,不属于 Value.
我们使用自然数表示可能的提议编号以及每个实例的编号,即 Ballots Nat,Instances Nat.Quorums 定义了
一种特殊的议会系统(quorum system):它的每个元素都是由超过半数的接受者构成的集合.
Multi-Paxos 的规约中包括 6 个变量.
• ballot:ballot[a]表示接受者 a 记录的最大的提议编号,也是 a 可以接受的最小的提议编号;
• vote:vote[a][i][b]表示接受者 a 对编号为 i 的实例在 a 的提议编号为 b 时接受的提议值.如果 a 在提议
编号为 b 时,没有对编号为 i 的实例接受任何值,则 vote[a][i][b]=Nil;
• leaderVote:leaderVote[b][i]为提议者在提议编号为 b 时,为编号为 i 的实例提出的值与提议编号 b 组成
的二元组.初始状态下,对所有的提议编号 b 与实例编号 i,leaderVote[b][i]=〈−1,Nil〉;
• 1amsgs,1bmsgs,2amsgs:不同类型的消息集合.
----------------------------- MODULE MultiPaxos -----------------------------------
EXTENDS Integers, FiniteSets
CONSTANTS Acceptors, Nil, Value
Ballots==Nat
Instances==Nat
Quorums=={Q\in SUBSET Acceptors: Cardinality(Q)>Cardinality(Acceptors)\2}
Max(s)==CHOOSE x\in s:\for all y\in s:x\geq y
VARIABLES ballot, vote, leaderVote, 1amsgs, 1bmsgs, 2amsgs
-------------------------------------------------------------------------------------------------
协议定义的主要动作包括:
• Phase1a(b):对应 Paxos 的 Phase1a 阶段.提议者选取提议编号 b,并且向其他节点发送 Prepare 请求,提
议的编号为 b;
• Phase1b(a,b):对应 Paxos 的 Phase1b 阶段.节点 a 收到编号为 b 的投票请求.若 b>ballot[a],a 设置
ballot[a]为 b,并且对于每一个实例编号 i,a 将它接受过的提议编号最大的提议值与提议编号回复给提
议者.
--------------------------------------------------------------------------------------------
Phase1a(b)==
/\1amsgs′=1amsgs\cup {〈〈b〉〉}