EPaxos介绍

简单介绍EPaxos算法。

Epaxos的简介

EPaxos是一个Leaderless的算法,具有以下的优点:

  1. Client可以任意选择一个节点发送Command,这个Command的Commit的路径大部分都不会干扰到其他的Command。而在诸如Raft的算法中,必须有一个Master显式向其他节点复制日志。并且也避免了Client可能和一个跨地区的Master交互的情况。
  2. 因为没有Leader选举的过程,所以整个集群的可用性变高了。

讨论Basic Paxos算法,当收到来自Client的Command后,某个replica会尝试成为一个尚未被使用过的instance的Leader,方式是发送Prepare消息。其他replica对Prepare的返回值,首先包含了它们认为的已经被chosen的Command(如果出现这种情况,Leader后面也需要使用这个Command)。在返回值中还会包含不会再ack早前的Leader发送的更旧的消息的承诺。在收到majority的对Prepare的ack之后,这个Leader会发送Accept消息。当Accept消息再被majority确认后,Leader会在本地记录Command已被Commit,并且异步通知Peer和Client。

容易发现,Paxos算法需要Prepare和Accept两个阶段,才能完成一个Command的提交。这是不经济的,因为即使从Raft的经验来看,只要Leader一直存在,那么一轮就可以决定一个instance,也就是Log Entry的值了。此外Basic Paxos中如果多个Leader打架,那2轮都不够。因此MultiPaxos中引入了stable leader(又称为distinguished proposer)的机制来处理。

EPaxos的设计目标是:

  1. 减少Commit时延
  2. 优化Load Balance
  3. 对于较慢甚至故障的节点,提供一个优雅的降级方案

为此,EPaxos需要做到:

  1. 每个节点都可以同时作为Proposer(Command Leader)
  2. 每个Proposer在和最小数量的节点交流后就可以Commit,并且交流的次数也要最小化
    类似generic broadcast算法,以及Generalized Paxos算法,会广播消息。但如果两个Command不互相影响,实际上并没有必要强制他们有一个consistent的顺序。
    而在实际workload上,可以认为大部分的Command是这样的,也就是说它们修改的是不同的对象。
  3. Quorum的组成应当是可变的

EPaxos做到这些,得益于它给Command定序的方案。在这之前,诸如MultiPaxos和GenerizedPaxos选择通过一个Leader来选择顺序;而在 canonical Paxos和Mencius中选择将这些Command放入已经预先分配好的instance空间中。

EPaxos的方案是当对一个Command投票时,每个参与者需要附带上对这个Command的Order Constraints。EPaxos能够保证所有正常的节点能够以提交同样的Command和Order Constraints。

简介一下EPaxos的方案。当一个Command被发送给某个replica时,该replica就被称为Command Leader。这个称呼特意区别于MultiPaxos中的Leader,因为显而易见,同时可能存在多个Command Leader。

如果Command之间不冲突,如下图的左边所示,两个Command分别更新obj_Aobj_B。为了Commit这个Command,可以走论文中说的Fast Path。Command Leader需要和F + floor((F + 1) / 2)(称为fast-path quorum)个Peer交互。其中F是允许失败的节点的个数,对应到下图,F为2。特别地,对于常见的3节点集群,Fast-path Quorum为2;对于5节点集群,Fast-path Quorum为3,都等于传统的简单多数。

【Q】这里有个疑问,不同对象的先后顺序,有影响么?比如实际上一个Client先于obj_Bobj_A,但obj_B先于obj_A被Commit,当Client收到obj_B的时候读取obj_A,那么可能读到obj_A的stale的数据呢?可以看下面的Execution linearizability说明。

如果两个Command互相冲突,如下图的右边所示,C3和C4同时更新obj_A,就不能走Fast Path了。在提交的时候需要附带上Order Constraint。为了保证所有的Replica在存在部分节点故障的情况下,都能提交相同的Order Constraint,需要另一轮的通信。这一轮通信中,Command Leader需要和F + 1个Peer交互。这就是Slow Path,F + 1也就是传统意义上的简单多数Quorum。

EPaxos和其他算法的比较

在MultiPaxos中,Leader会负责Propose所有的Command。这样会导致Leader处理O(n)个请求,同时非Leader节点只会处理O(1)个请求,负载十分不均衡。

为了解决MultiPaxos的问题,Mencius选择逐Command将Paxos Leader在多个节点之间轮换。也就是说节点
R_id拥有instance i,当i满足(i mod N) = R_id。这里的坏处是,每一次Commit Command A之前都需要询问所有节点。否则按照这个轮换顺序,另一个依赖于A的Command B可能在Command A之前被提交。这个询问过程会产生两个后果,首先是整个Commit的速度由最慢的那个Replica决定;其次是当一个节点Fail后,整个过程将block住,直到其他节点发现这个节点Fail掉了,并替他返回一个NoOp。

FastPaxos为了解决从Propose到Commit的延迟,选择让Client同时向所有的Replica发送Propose。MultiPaxos一样使用了Stable Leader,不仅用来开启voting round,也用来仲裁各个Acceptor的顺序(考虑到每个Acceptor可能以不同顺序收到)。

Generalized Paxos的方案是当Command之间不互相影响时,对它们乱序提交。Replicas learn commands after just two message
delays—which is optimal—as long as they do not interfere。TODO 后面看不懂了。

EPaxos相对于Generalized Paxos有三点优势:

  1. EPaxos的Fast Path Quorum Size比Generalized Paxos的正好小一个,能够减小延迟(应该是木桶效应吧),以及总的消息量
  2. EPaxos解决冲突,也就是Slow Path只需要额外一轮,但Generalized Paxos需要两轮
  3. 对于three-site replication而言,EPaxos即使在所有Command都冲突的情况下,只需要和距离Proposer最近的Replica通信一轮,即可Commit

EPaxos和Fast/Generalized Paxos的Fast Path的一个重要区别是,EPaxos需3 message delays来Commit,但Fast等只需要2个。但一般EPaxos的第一个Delay可以忽略掉,因为Client和最接近的Replica通常都在一个数据中心中。

S-Paxos TODO

EPaxos的实现

结合了两篇论文的内容

预备内容

在允许F个失效节点的分布式系统中,至少存在N=2F+1个节点。对于每一个节点R,它拥有的instance写为序列R1, R2, …。在每个instance中,只有一个Command能被选出。需要注意的是,R1、R2等instance的order,并不是已经确定的,而是由协议来动态确定。

Commands γ和δ是interfere的,当存在一系列指令Σ使得顺序执行Σ,γ,δ不等价于顺序执行Σ,δ,γ。这里不等价包含它们会导致不同的状态机状态,或者导致在这些序列中读取到的值是不同的。

性质

  1. Nontriviality
    所有被Commit的Command都由Client发出。
  2. Stability
    对于任意Replica,不会丢失已经Commit的数据。
    进一步地,如果在t1时刻,Replica R在Q.i这个instance上提交了Command Y,那么在t1之后的任意时刻t2,R上的instanceQ.i的值也是Command Y。
    【Q】这里有个疑问,Q是哪里来的?不应该是R么?应该不矛盾,作为Acceptor,R也会有Q拥有的instance的信息的,不然怎么投票?
  3. Consistency
    同一个instance在Commit之后,就在各个Replica上的值都是一样的。
  4. Execution consistency
    如果两个interfere的Command Y和Z在任意Replica上被成功Commit了,那么所有Replica上的执行顺序是一样的。
  5. Execution linearizability
    如果Client对Command Y和Command Z是serialized的,比如说在Command Y被Commit之后,才会Propose Command Z,那么所有的Replica都会先执行Y再执行Z。
  6. Liveness
    活性

基础版本

基础版本的fast-path quorum是2F,后面优化版本的才是F + floor((F + 1) / 2)

Commit Protocol

Commit Protocol解决两个问题:

  1. Commit Command
  2. Determine Order Between Commands

在论文的Figure2中描述了Commit Protocol的整个过程,在Commit过程中,并不是每个过程都会走到。如果一个Command没有冲突,就可以走Fast Path,这也意味着走完Phase 1就能够直接提交了。Slow Path还需要额外的Phase 2(Paxos-Accept phase)。如果我们进行failure recovery,则需要运行Figure3描述的Explicit Prepare过程。

当一个Replica收到来自Client的Command γ后,会给这个Command γ分配一个全局唯一的instance number,例如R1、Q2等。全局唯一是通过组合Replica的名字,以及在Replica中递增的序列号保证的。这里Replica是可以将多个操作组合到一个instance中的。除了分配instance number之外,Replica还会给Command分配一个dependency set(deps)和一个sequence number(seq),称为attribute。Dependency set包含了每个Replica中最高的和自己冲突的instance编号。Sequence number会选取一个大于dependency set中所有值的值作为初始值。The originating replica derives the dependency set and sequence number for a new instance from all other instances it has knowledge of。对于每个修改了新Command操作对象的Replica,需要持久化它们的最高的instance number和sequence number。

Command Leader通过PreAccept消息,即(γ,seqγ,depsγ,pre-accepted),将Command以及deps和seq发送给至少fast-path quorum(在这里是2F)个Replica。每个Replica在收到后,会根据自己的cmds log来更新Command γ的deps和seq,并将γ和新的attribute记录在自己的log中,然后回复给Command Leader。

如果Command Leader满足了fast-path quorum,并且所有更新了的attribute(seq和deps)是一样的(根据Figure2的第10行代码,不包括Command Leader),那么可以直接Commit。否则就需要走Slow Path。

在运行Slow Path前,我们得更新seq和deps。其中deps是从每个Replica之间的union,seq取每个Replica过来的最大的seq。然后在Slow Path中,Command Leader会给另外F个Replica发送Accept请求,让它们Accept三元组(γ,seq,deps)。其实这个过程类似于Basic Paxos的Accept阶段。

在Slow Path完成了取得了F + 1票后,就可以和Fast Path会师了。此时Command Leader会发送Commit消息给所有的Replica,并且返回给Client。

类似于经典的Paxos,EPaxos也会给每个消息(message)分配一个ballot number。每个Replica会忽略小于它们已经见过的最大的ballot number。这个ballot number格式为epoch.b.R,其中:

  1. epoch
    如果集群的配置有变动,那么epoch会变化
  2. b
    如果某个replica R,在做Explicit Prepare时,需要创建一个新的ballot时,会自增b
  3. R
    表示这个Replica

每个Replica是自己拥有的instance的初始Leader,换言之,对于每个instance R.i,隐式存在一个epoch.0.R

Explicit Prepare过程

【这一块还包含了优化部分,比较难懂】
假如说Replica L可能宕机了,那么Replica Q会尝试接管它的instance L.i。

首先,将ballot number设置为epoch.(b + 1).Q,其中epoch.b.R是Q知道的L.i中最大的ballot number。然后,发送Prepare(epoch.(b + 1).Q,L.i)给包括自己在内的所有Replica,并且等待至少floor(N/2) + 1个回复。令R等于the set of replies w/ the highest ballot number:

  1. 如果R中包含了(γ,seqγ,depsγ,committed),则在L.i对(γ,seqγ,depsγ)运行Commit Phase。
  2. 再如果R中包含了(γ,seqγ,depsγ,accepted),运行Paxos-Accept phase。
  3. 再如果R包含了至少floor(N / 2)个不同的对L.i上默认的ballot即epoch.0.L的回复(γ,seqγ,depsγ,pre-accepted),并且没有一个回复是来自于L的,则运行Paxos-Accept phase。
    【优化算法】此时,只需要包含floor((F + 1) / 2)个PreAccept了(γ,seqγ,depsγ)这个三元组的Replica即可。在发现他们后,新的Command Leader Q会尝试向其他Replica发送TryPreAccept消息。在某个Replica收到TryPreAccept消息后,会判断这个三元组是否和自己已有的log冲突:一个Command的deps中不包括γ,并且depsγ中也不包括这个Command(简单来说两个Command的deps互相不包含),那么这个Command就和γ冲突;或者这个Command虽然在depsγ中,但是它的seq大于等于seqγ,那么也是和γ冲突的。只有当自己的log中没有这些冲突Command时,这个Replica才会回复TryPreAccept。
    如果真的存在某个Command和三元组冲突,并且这个Command被Commit了,那么Q就知道γ不能再fast path中被提交。但如果这个Command没有被Commit,那么新的Comamnd Leader Q就会defer,知道这个Command被Commit。最后,如果Q能够得到F + 1个Replica(在计算F时,老Command Leader也被计算在内)的PreAccept票后,就可以运行Paxos-Accept phase了。
    这里有一个Corner case,也即是当deps中的某个Command修改它的seq,然后比需要Recover的Command γ的seq还要大了。为了阻止这个情况,对于depsγ中的所有Command,至少需要有一个Acceptor记录为Commit状态后,才允许Command Leader走Fast Path提交。对于N小于7的情况,更有效的方案是将更新后的deps放到Accept和AcceptReply消息中,并且保证这些消息的接收方都去缓存了它们。这些信息只会被用来辅助Recovery。
    【Q】为啥优化算法只改这一个分支?
  4. 再如果R包含了至少一个(γ,seqγ,depsγ,pre-accepted),则在L.i上执行Phase1,Command为γ,并且避免fast path。
  5. 最终,则在L.i上执行Phase1,Command为noop,并且避免fast path。

Replica R, 在收到来自Q的Prepare(epoch.b.Q,L.i)后:

  1. 如果epoch.b.Q比最近接受到来自L.i的请求epoch.x.Y大,则返回PrepareOK(cmdsR[L][i], epoch.x.Y,L.i)
  2. 否则返回NAC

Execution Protocol

为了执行在R.i这个instance上提交的Command γ,需要执行下面的步骤:

  1. 等待R.i被提交,或者运行Explicit Prepare过程强制这个过程
  2. 构造γ的依赖图,其中需要加入γ的dependency set中的所有Command
    注意,这个过程是递归的,也就是我们需要考虑依赖的依赖
  3. 找到所有的SCC,并对这些SCC进行拓扑排序
  4. 根据逆拓扑序,执行:
    1. 对于SCC中的所有命令,按照sequence number(seq)从低到高排序
    2. 按照这个顺序执行所有尚未被执行的Command,并标记他们为已被执行

关于性质的(Informal)证明

Nontriviality

Stability和Consistency

先证明命题1:如果Replica R通过instance Q.i提交了Commit γ(这里R和Q可能是同一个Replica),那么对于任意的提交Q.i的Replica R’,它提交的Command γ’一定等于γ。

证明简要:如果说Command γ能被在Q.i这个instance中提交,一定是因为γ的Phase 1是在instance Q.i中被启动的。这是因为:

  1. 对于每个新Command,Q会自增instance number,也就是这里的i
  2. 如果Q宕机并重启了,那么根据”4.7 Reconfiguring the Replica Set”,它会被分配得到一个新的identifier
    【TODO】这里需要详细解释下。

可以看到,命题1实际上暗示了consistency。进一步地,在Replica崩溃时,Command可能被丢失,所以当Command Log被保存在持久化存储上时,也暗示了stability。

首先引入一个定义。如果Command γ具有seqγ和depsγ,如果元组(γ,seqγ,depsγ)是Q.i这个instance上唯一被或者可能被commit的元组,那么我们称元组(γ,seqγ,depsγ)在Q.i这个instance上是safe的。

下面证明命题2:Replica只会提交safe的tuple。首先知道(γ,seqγ,depsγ)如果在Q.i被提交,那么它要么在Paxos Accept phase提交,或者在Phase 1之后提交。

  1. 对于第一种情况,即Slow Path。此时有多于半数的Replica写入了值(Figure2的L20),这对应了经典Paxos的要求。
  2. 对于第二种情况,即Fast Path。此时Coomand Leader收到了不含自己的N-2个相同的回复(Figure2的L11)。如果此时另外的Replica需要接管这个instance,通常这是因为初始的Leader宕机了,那么新Leader必须执行Prepare过程,并且会发现至少floor(N/2)个Replica都返回(γ,seqγ,depsγ)这个元组。因此新的Leader会认为这个元组可能提交了,并在Paxos-Accept过程中使用这个元组。

至此我们可以发现,元组们,包括他们的attributes,都会在各个Replica之间被consistently和stable地提交。

下面我们证明这些consistent和stable的attributes能够保证所有互相interfere的Command,在每个Replica上都按照同样的顺序被提交。

Execution consistency和Execution linearizability

引理1 (Execution consistency):
如果互相interfere的两个Command γ和δ都被成功Commit了(并不一定通过同一个Replica提交),那么他们在任意Replica上都会以相同的顺序被执行

如果两个Command互相interfere,至少有一个Command的deps中能找到另一个Command。Phase1在这个命令被至少简单多数(注意我们现在讲的还是基础版本的EPaxos,其中Phase1的Fast Path Quorum为2F)个Replica Pre-Accepted后结束,并且这个命令最终的deps集是由至少简单多数个Replica的deps的union。这也同样适用于recovery过程中使用的Explicit Prepare(L32)的情况,因为所有的依赖都是基于那些被可能宕机的Leader初始设置的集合计算得到。所以至少一个Replica同时PreAccept γ和δ,并且它的PreAcceptReplies被用来构造γ和δ的最终的deps集。

通过执行Execution Algorithm,一个命令只有在自己dependency graph中的所有命令都被Commit后才会执行。主要有三个场景:

  1. 两个Command都在彼此的dependency graph中,这也意味着dependency graph是identical的,并且γ和δ在同一个SCC中。所以当执行一个Command时,另一个Command也会被执行,并且是根据sequence number来执行的。根据命题2,这些已Commit的Command的attribute在所有Replica上都是stable和consistent的。所以所有dependency graph相同的Replica都会在相同的顺序中执行γ和δ。
  2. γ在δ的dependency graph中(δ依赖γ),但δ不在γ的dependency graph中。也就是说dependency graph有一个从δ到γ的路径,反之不成立。因此γ和δ来自不同的SCC,在逆拓扑序即实际的执行顺序中,γ在δ前面。补充一点,在一些Replica中,γ在δ被Commit之前就被执行了,这样的场景是没毛病的,因为γ并不依赖于δ。
  3. δ在γ前面,这个就是上面的对称形式。

引理2 (Execution linearizability):
如果两个Command γ和δ,被客户端指定了顺序,例如只有在γ被任意Replica Commit之后才会Propose δ,这样的话我们要求所有的Replica都要在δ之前执行γ。

证明。因为δ是在γ Commit之后被Propose的,所以在任何Replica收到Command δ的PreAccept时,γ的Sequence Number应该是Stable和Consist的。因为一个包含γ的元组,以及它最终的sequence number至少被majority个Replica记录,那么δ的sequence number会最终被更新到大于γ的值,并且delta的deps中会包含γ。所以在执行δ时,δ的dependency graph必须包含γ,并且:

  1. 它们在同一个SCC中
  2. 按照逆拓扑序,γ在δ前面的一个SCC中。

无论那种情况,γ都会在δ前面执行。

Liveness

只要不是大多数Replica有故障,那么Client会一直重试某个Command,直到被Accept。

优化版本

优化版本会修改Recovery过程,也就是Explicit Prepare Phase。我已经写到“Explicit Prepare过程”上面了。

当F个Replica宕机后,在Fast Quorum中就只有floor((F + 1) / 2)个存活的成员(可以翻翻前面Fast-Path Quorum的定义),那么就不能在剩下的Replica中形成多数了。所以,当Command Leader向所有Replica(而不只是Fast Quorum中的Replica)发送PreAccept消息后,Recovery过程不一定能正确地发现,老的Command Leader,是通过哪些Replica的回复,从而Commit了这个instance的。 Still, such redundancy is sometimes desirable because the command leader may not know in advance which replicas are still live or which replicas will reply faster。
对于这种情况,需要修改Fast Path的条件:当Command Leader收到F + floor((F + 1) / 2) - 1个满足initial ordering attributes的PreAccept的回复,才会选择Fast Path。并且这些Replica需要被记录到Log中,以便在Recovery过程中只考虑这些Replica。
在不发送redundant PreAccept的时候(【Q】什么时候会发送?),一个三副本的系统永远可以通过Fast Path提交,这是因为在做还有一个Acceptor的集合中肯定不存在disagreement。

EPaxos的TLA+简介

如果光读论文就能读懂,那我感觉你真的挺厉害的,反正我是半懂不懂的,特别是对Recovery部分。所以我转过来看TLA+了。

定义

下面是对SlowQuorum和FastQuorum的定义。对于某个Replica r,SlowQuorum(r)表示它作为Command Leader时,所有可能的Slow Path Quorum组成的集合,也就是类似于{ {r,a}, {r,b} }这样的东西。那么,SlowQuorum(r)必须是SUBSET Replica的子集,换句话说,就是不能出现Replica之外的元素。然后对于SlowQuorum中的任意的Quorum SQ,它必须包含r,并且大小为N/2+1,其中N为集群大小。
同理,FastQuorum中的大小为N/2 + (N/2+1)/2,这个其实就是把F = N/2带入进去就得到了。

1
2
3
4
5
6
7
8
9
10
11
12
13
CONSTANTS FastQuorums(_), SlowQuorums(_)
ASSUME \A r \in Replicas:
/\ SlowQuorums(r) \subseteq SUBSET Replicas
/\ \A SQ \in SlowQuorums(r):
/\ r \in SQ
/\ Cardinality(SQ) = (Cardinality(Replicas) \div 2) + 1

ASSUME \A r \in Replicas:
/\ FastQuorums(r) \subseteq SUBSET Replicas
/\ \A FQ \in FastQuorums(r):
/\ r \in FQ
/\ Cardinality(FQ) = (Cardinality(Replicas) \div 2) +
((Cardinality(Replicas) \div 2) + 1) \div 2

下面是对一些状态的定义。Commands是一个常量,表示所有可能的命令,在运行前由我们给出。none是一个none Command(也许是Noop?),对它的定义还挺新颖的,如果是我,可能选择直接CONSTANT了一个Nil的值。
Instance是做了一个笛卡尔积,没啥讲的。
Status标记了Log中的某个Command可能处于的状态。

1
2
3
4
CONSTANTS Commands
none == CHOOSE c : c \notin Commands
Instances == Replicas \X (1..Cardinality(Commands))
Status == {"not-seen", "pre-accepted", "accepted", "committed"}

下面是Replica之间可能发送的消息。这里的TLA+语法可以参考TwoPhase章节

  1. pre-accept、pre-accept-reply
    Phase1由Command Leader发起的消息和回复,即(γ,seqγ,depsγ,pre-accepted)
    注意要区分这里的committed字段,和全局的committed变量
  2. accept、accept-reply
    Phase2由Commmand Leader发起的消息和回复,即(γ,seqγ,depsγ,accepted)
  3. commit
    Commit阶段由Command Leader发起的消息,即(γ,seqγ,depsγ,committed)
  4. prepare、prepare-reply
    Explicit Prepare阶段由新的Command Leader Q发起的消息。
  5. try-pre-accept、try-pre-accept-reply
    优化算法

一些常见字段的说明:

  1. src和dst都属于Replicas。
  2. inst属于Instances表示当前操作的实例。
  3. ballot应该是指的ballot number,不是epoch.b.R么?看起来是吧epoch和b合并了?
  4. cmd应该是指instance中包含的command。
  5. deps和seq就是所谓的attribute,没啥讲的。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
Message ==
[type: {"pre-accept"}, src: Replicas, dst: Replicas,
inst: Instances, ballot: Nat \X Replicas,
cmd: Commands \cup {none}, deps: SUBSET Instances, seq: Nat]
\cup [type: {"accept"}, src: Replicas, dst: Replicas,
inst: Instances, ballot: Nat \X Replicas,
cmd: Commands \cup {none}, deps: SUBSET Instances, seq: Nat]
\cup [type: {"commit"},
inst: Instances, ballot: Nat \X Replicas,
cmd: Commands \cup {none}, deps: SUBSET Instances, seq: Nat]
\cup [type: {"prepare"}, src: Replicas, dst: Replicas,
inst: Instances, ballot: Nat \X Replicas]
\cup [type: {"pre-accept-reply"}, src: Replicas, dst: Replicas,
inst: Instances, ballot: Nat \X Replicas,
deps: SUBSET Instances, seq: Nat, committed: SUBSET Instances]
\cup [type: {"accept-reply"}, src: Replicas, dst: Replicas,
inst: Instances, ballot: Nat \X Replicas]
\cup [type: {"prepare-reply"}, src: Replicas, dst: Replicas,
inst: Instances, ballot: Nat \X Replicas, prev_ballot: Nat \X Replicas,
status: Status,
cmd: Commands \cup {none}, deps: SUBSET Instances, seq: Nat]
\cup [type: {"try-pre-accept"}, src: Replicas, dst: Replicas,
inst: Instances, ballot: Nat \X Replicas,
cmd: Commands \cup {none}, deps: SUBSET Instances, seq: Nat]
\cup [type: {"try-pre-accept-reply"}, src: Replicas, dst: Replicas,
inst: Instances, ballot: Nat \X Replicas, status: Status \cup {"OK"}]

下面是定义变量,可以结合TypeOK和Init条件看出类型

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
VARIABLES cmdLog, proposed, executed, sentMsg, crtInst, leaderOfInst,
committed, ballots, preparing

TypeOK ==
/\ cmdLog \in [Replicas -> SUBSET [inst: Instances,
status: Status,
ballot: Nat \X Replicas,
cmd: Commands \cup {none},
deps: SUBSET Instances,
seq: Nat]]
/\ proposed \in SUBSET Commands
/\ executed \in [Replicas -> SUBSET (Nat \X Commands)]
/\ sentMsg \in SUBSET Message
/\ crtInst \in [Replicas -> Nat]
/\ leaderOfInst \in [Replicas -> SUBSET Instances]
/\ committed \in [Instances -> SUBSET ((Commands \cup {none}) \X
(SUBSET Instances) \X
Nat)]
/\ ballots \in Nat
/\ preparing \in [Replicas -> SUBSET Instances]

Init ==
/\ sentMsg = {}
/\ cmdLog = [r \in Replicas |-> {}]
/\ proposed = {}
/\ executed = [r \in Replicas |-> {}]
/\ crtInst = [r \in Replicas |-> 1]
/\ leaderOfInst = [r \in Replicas |-> {}]
/\ committed = [i \in Instances |-> {}]
/\ ballots = 1
/\ preparing = [r \in Replicas |-> {}]
  1. cmdLog
    每个Replica上的日志。
    每条日志中包含对应的Instance、Status,ballot、Command、以及deps和seq
  2. proposed
    已经被被Propose了的Command
  3. executed
    每个Replica上已经被execute的Command
  4. sentMsg
    所有被发送,但是还没有被接受的消息,理解成Message类型对象的集合
  5. crtInst
    对于每个Replica,它下一个可以使用的instance number(一个数字),初始值是1
  6. leaderOfInst
    这是从Replicas到SUBSET Instances的一个映射,表示对于每个Replica,它发起但是还没有完成的Instance的集合
  7. committed
    【Q】maps commands to set of commit attributs tuples
    从实现上来看,应该是个三元组,表示每个Command被提交时的deps和seq
  8. ballots
    所有Replica中,最大的ballot number,这里指的应该是epoch.b
  9. preparing
    对于每个Replica,它目前正在preparing(例如recovering)的所有Instance

验证

Nontriviality的验证,对于任意的Instance,始终(因为有[])有:在committed中的所有Command,它要么是在proposed集合中(也就是被某个Command Leader主动Propose的),或者为none

1
2
3
Nontriviality ==
\A i \in Instances :
[](\A C \in committed[i] : C \in proposed \/ C = none)

Stability的验证,是个三层大循环,遍历所有的Replica/Instances/Commands,此时我们检查(replica, i, C),始终满足:
在replica的cmdLog[replica]中任选一条记录rec1,它的(inst,cmd)等于(replica, i),并且status为committed或者executed,那么始终存在另一个满足条件的rec2。

1
2
3
4
5
6
7
8
9
10
11
12
Stability ==
\A replica \in Replicas :
\A i \in Instances :
\A C \in Commands :
[]((\E rec1 \in cmdLog[replica] :
/\ rec1.inst = i
/\ rec1.cmd = C
/\ rec1.status \in {"committed", "executed"}) =>
[](\E rec2 \in cmdLog[replica] :
/\ rec2.inst = i
/\ rec2.cmd = C
/\ rec2.status \in {"committed", "executed"}))

Consistency的验证,对于所有的Instance i,始终满足它最多只会被commit一次。

1
2
3
4
5
Consistency ==
\A i \in Instances :
[](Cardinality(committed[i]) <= 1)

THEOREM Spec => ([]TypeOK) /\ Nontriviality /\ Stability /\ Consistency

总体的Action

可以选择执行Command Leader的某个动作,或者普通Replica的某个动作。Command Leader肯定属于Replica,但我们是按照行为来区分的。

1
2
3
Next == 
\/ CommandLeaderAction
\/ ReplicaAction

首先是Command Leader的所有可能的动作:

  1. 检查Commands \ proposed,也就是Commands中所有还没被propose的Command,如果存在,则选择一个C(\E可以表示选出一个的意思):
    选出一个cleader,对C做状态转移Propose(C, cleader)
  2. 在Replicas中选出一个cleader,在cleader为Command Leader的instance中选出一个instance,可以执行下面任意的状态转移:
    1. 可能走Fast Path
    2. 可能走Slow Path
    3. 可能走Phase2Finalize
      【Q】Phase2的Accept啥时候发送的?
    4. 可能走优化路径FinalizeTryPreAccept
1
2
3
4
5
6
7
8
CommandLeaderAction ==
\/ (\E C \in (Commands \ proposed) :
\E cleader \in Replicas : Propose(C, cleader))
\/ (\E cleader \in Replicas : \E inst \in leaderOfInst[cleader] :
\/ (\E Q \in FastQuorums(cleader) : Phase1Fast(cleader, inst, Q))
\/ (\E Q \in SlowQuorums(cleader) : Phase1Slow(cleader, inst, Q))
\/ (\E Q \in SlowQuorums(cleader) : Phase2Finalize(cleader, inst, Q))
\/ (\E Q \in SlowQuorums(cleader) : FinalizeTryPreAccept(cleader, inst, Q)))

下面是ReplicaAction,选择一个Replica:

  1. 可能回复Phase1
  2. 可能回复Phase2
  3. 可能对于某个Instance i,i[1]表示Instance这个tuple的第一个元素,也就是Replica;crtInst[i[1]]表示它对应的Replica下一个可以使用的instance number,如果大于i本身的instance number。
    这个条件说明这个instance被自己原来的owner start。
    则通过SlowQuorum个节点进行SendPrepare。
    【Q】不太懂什么意思,但这里无疑就是Explicit Prepare里面的Prepare过程了。
  4. 可以ReplyPrepare
  5. 选择一个正在preparing的Replica
    通过SlowQuorum个节点进行PrepareFinalize
  6. 回复ReplyTryPreaccept
1
2
3
4
5
6
7
8
9
10
11
12
13
ReplicaAction ==
\E replica \in Replicas :
(\/ Phase1Reply(replica)
\/ Phase2Reply(replica)
\/ \E cmsg \in sentMsg : (cmsg.type = "commit" /\ Commit(replica, cmsg))
\/ \E i \in Instances :
/\ crtInst[i[1]] > i[2] (* This condition states that the instance has *)
(* been started by its original owner *)
/\ \E Q \in SlowQuorums(replica) : SendPrepare(replica, i, Q)
\/ ReplyPrepare(replica)
\/ \E i \in preparing[replica] :
\E Q \in SlowQuorums(replica) : PrepareFinalize(replica, i, Q)
\/ ReplyTryPreaccept(replica))

Phase 1

Propose

从上文看到,CommandLeaderAction的一个可能的状态转移是Propose。
此时,生成newInst和newBallot。新生成的newInst的instance number为crtInst[cleader],newBallot的epoch.b部分始终为0,看来是不考虑epoch了。
然后,将要Propose的Command C添加进proposed中,并且在FastQuorum里面选择一个Quorum,尝试走FastPath。
然后,我们自增crtInst,这里的@就是crtInst[cleader],实际上是一个简写。

1
2
3
4
5
6
7
8
Propose(C, cleader) ==
LET newInst == <<cleader, crtInst[cleader]>>
newBallot == <<0, cleader>>
IN /\ proposed' = proposed \cup {C}
/\ (\E Q \in FastQuorums(cleader):
StartPhase1(C, cleader, Q, newInst, newBallot, {}))
/\ crtInst' = [crtInst EXCEPT ![cleader] = @ + 1]
/\ UNCHANGED << executed, committed, ballots, preparing >>

对Phase1的处理起始于StartPhase1,这个状态转移触发的条件有很多,比如上面的Propose。
首先,构建依赖deps和seq:

  1. newDeps是Command Leader即cleader中所有Command的Instance,即rec.inst
    【Q】这是不是太强了点?按照协议,首先要是冲突的,然后只要包含最高冲突Instance的编号就行啊。
  2. newSeq是cleader中所有Command的seq的最大值,然后还要加1,这是符合协议的论述的。
  3. oldRecs表示cleader中所有和当前Command的Instance相同的Command。

然后进行状态转移:

  1. cmdLog
    需要修改cleader的Log。具体来说,需要把同Instance的所有的旧的日志全部干掉。【Q】为啥可能会有同Instance的日志呢?
    然后,我们把新的Command加上到日志中,并且设置status为”pre-accepted”。也就是说cleader我PreAccept了这个日志,并不代表其他Replica也PreAccept了这个日志。
  2. leaderOfInst
    显然,对于这个Instance,cleader我是它的Leader。这是显然的,因为Instance二元组里面,Replica是cleader,然后instance number也是自增的。
    应该加入到leaderOfInst,表示是我发起的,但还没有完成的Instance。
  3. sentMsg
    显然要往其他的Replica发消息。在此之前,我们先要把oldMsg干掉。如果我们是走Propose过来的,那么oldMsg是空的。但如果是走Explicit Prepare过来的,那么是会传入oldMsg的,这个到时候再说。
    这里需要注意,消息的定义是src: Replicas, dst: Replicas,但我们传进来的src和dst实际上是两个集合,这会导致产生一系列新Msg。可以参考TLA的文档。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
StartPhase1(C, cleader, Q, inst, ballot, oldMsg) ==
LET newDeps == {rec.inst: rec \in cmdLog[cleader]}
newSeq == 1 + Max({t.seq: t \in cmdLog[cleader]})
oldRecs == {rec \in cmdLog[cleader] : rec.inst = inst} IN
/\ cmdLog' = [cmdLog EXCEPT ![cleader] = (@ \ oldRecs) \cup
{[inst |-> inst,
status |-> "pre-accepted",
ballot |-> ballot,
cmd |-> C,
deps |-> newDeps,
seq |-> newSeq ]}]
/\ leaderOfInst' = [leaderOfInst EXCEPT ![cleader] = @ \cup {inst}]
/\ sentMsg' = (sentMsg \ oldMsg) \cup
[type : {"pre-accept"},
src : {cleader},
dst : Q \ {cleader},
inst : {inst},
ballot: {ballot},
cmd : {C},
deps : {newDeps},
seq : {newSeq}]

Phase1Reply

Propose是发送PreAccept请求,Phase1Reply是其他Replica处理该请求。
任选一个发给replica的type为”pre-accept”的消息msg。
oldRec为replica日志中,inst等于msg对应的Instance的日志组成的集合。
那么对于oldRec中所有的日志rec,要么它的ballot等于msg里的ballot,要么比msg传过来的ballot要小。否则这个消息就应该被忽略。

构造newDeps为msg传来的deps,加上当前replica所有的log中的Instance(除去msg.inst)。
构造newSeq为Max(msg.seq, replica的所有日志中最大的seq+1)。
构造instCom,为replica自己日志中所有status为”committed”或”executed”(其实就是已提交)的日志对应的Instance构成的集合。

下面是状态转移:

  1. 修改当前replica的cmdLog
    主要是将status变成”pre-accepted”,然后deps和seq设置为刚算出来的newDeps和newSeq。
  2. 发送消息
    发送一条”pre-accept-reply”消息给msg.src,实际上就是刚才发命令过来的cleader。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
Phase1Reply(replica) ==
\E msg \in sentMsg:
/\ msg.type = "pre-accept"
/\ msg.dst = replica
/\ LET oldRec == {rec \in cmdLog[replica]: rec.inst = msg.inst} IN
/\ (\A rec \in oldRec :
(rec.ballot = msg.ballot \/rec.ballot[1] < msg.ballot[1]))
/\ LET newDeps == msg.deps \cup
({t.inst: t \in cmdLog[replica]} \ {msg.inst})
newSeq == Max({msg.seq,
1 + Max({t.seq: t \in cmdLog[replica]})})
instCom == {t.inst: t \in {tt \in cmdLog[replica] :
tt.status \in {"committed", "executed"}}} IN
/\ cmdLog' = [cmdLog EXCEPT ![replica] = (@ \ oldRec) \cup
{[inst |-> msg.inst,
status |-> "pre-accepted",
ballot |-> msg.ballot,
cmd |-> msg.cmd,
deps |-> newDeps,
seq |-> newSeq]}]
/\ sentMsg' = (sentMsg \ {msg}) \cup
{[type |-> "pre-accept-reply",
src |-> replica,
dst |-> msg.src,
inst |-> msg.inst,
ballot|-> msg.ballot,
deps |-> newDeps,
seq |-> newSeq,
committed|-> instCom]}
/\ UNCHANGED << proposed, crtInst, executed, leaderOfInst,
committed, ballots, preparing >>

Phase1Fast

Phase1Fast是cleader在其他Replica处理该请求后,尝试通过FastPath提交这个请求。里面包含了是否能够进行FastPath提交的判断,以及提交的状态转移。
首先,是一部分简单的Enable条件,校验cleader是不是Instance i的Leader,并检查Q是不是cleader的FastQuorums。
然后,选择cleader的某条日志record,日志中的Instance为i、Status为”pre-accepted”、ballot的为0。这些日志肯定是从StartPhase1设置的。并且因为ballot为0,所以肯定是从Propose设置的。
Q通过刚才的Phase1Reply发回来的replies,它们是”pre-accept-reply”类型的消息,并且ballot等于record对应的ballot,我们进行下面的检查:

  1. 对于Q中除了cleader之外的replica,在replies中都会有从它发给cleader的”pre-accept-reply”消息。
    也就是说Q中的Replica,都回复了cleader的pre-accept请求。
    这个检查是必要的,如果说之前cleader通过StartPhase1发过去的ballot比较小,那么有的replica就不会回复,因此这条Enable条件就过不了。
  2. 并且replies中任意两个消息r1和r2,它们的deps和seq是相等的。
    这是走FastPath的要求,只有满足该要求,才能进下一步。
    这个实际上也是Enable条件,如果不满足那么根本就不会有下面的状态转移。
  3. CHOOSE replies中的某一个r,基于它构造新的r.deps:
    这里可以CHOOSE,是因为大家的deps和seq都一样。
    注意已提交的日志,指的是status为”committed”和”executed”的日志。
    1. localCom
      cleader的所有的已提交日志的Instance构成集合。
    2. extCom
      Phase1Reply中,replica在回复时,会带上自己日志中所有已提交的日志对应的Instance构成的集合。
      extCom是这些的并集。
    3. 然后构造新的r.deps集合,为localCom和extCom中所有的Instance

然后基于r构造状态转移:

  1. cmdLog
    更新这个日志状态为committed。
    更新当前的record的attribute为r.deps和r.seq。
  2. sentMsg
    产生一条Commit信息,这个消息可能是直接给Client的,所以没有dst和src。
  3. leaderOfInst
    在leaderOfInst[cleader]中移除掉当前的Instance i,表示这个Instance已经提交了。
  4. committed
    <<record.cmd, r.deps, r.seq>>加入已提交的数组中。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
Phase1Fast(cleader, i, Q) ==
/\ i \in leaderOfInst[cleader]
/\ Q \in FastQuorums(cleader)
/\ \E record \in cmdLog[cleader]:
/\ record.inst = i
/\ record.status = "pre-accepted"
/\ record.ballot[1] = 0
/\ LET replies == {msg \in sentMsg:
/\ msg.inst = i
/\ msg.type = "pre-accept-reply"
/\ msg.dst = cleader
/\ msg.src \in Q
/\ msg.ballot = record.ballot} IN
/\ (\A replica \in (Q \ {cleader}):
\E msg \in replies: msg.src = replica)
/\ (\A r1, r2 \in replies:
/\ r1.deps = r2.deps
/\ r1.seq = r2.seq)
/\ LET r == CHOOSE r \in replies : TRUE IN
/\ LET localCom == {t.inst:
t \in {tt \in cmdLog[cleader] :
tt.status \in {"committed", "executed"}}}
extCom == UNION {msg.committed: msg \in replies} IN
(r.deps \subseteq (localCom \cup extCom))
/\ cmdLog' = [cmdLog EXCEPT ![cleader] = (@ \ {record}) \cup
{[inst |-> i,
status |-> "committed",
ballot |-> record.ballot,
cmd |-> record.cmd,
deps |-> r.deps,
seq |-> r.seq ]}]
/\ sentMsg' = (sentMsg \ replies) \cup
{[type |-> "commit",
inst |-> i,
ballot |-> record.ballot,
cmd |-> record.cmd,
deps |-> r.deps,
seq |-> r.seq]}
/\ leaderOfInst' = [leaderOfInst EXCEPT ![cleader] = @ \ {i}]
/\ committed' = [committed EXCEPT ![i] =
@ \cup {<<record.cmd, r.deps, r.seq>>}]
/\ UNCHANGED << proposed, executed, crtInst, ballots, preparing >>

Phase1Slow

Phase1Slow是cleader在其他Replica处理该请求后,尝试通过SlowPath提交这个请求。
前面的条件都一样,不再赘述。

主要不一样的地方是从finalDeps开始的。这里大家的deps和seq都不一定一样了,所以不能像FastPath一样CHOOSE了,而要老老实实取并集、取最大值。

  1. finalDeps
    就是所有来自Replica的回复中的deps的并集。
  2. finalSeq
    就是所有回复中最大的seq。

下面构造状态转移:

  1. cmdLog
    更新日志状态为”accepted”。
    注意,在FastPath中,能够直接进入commited状态,但这里得先是”accepted”,后面再走一轮Phase2才行。
  2. sentMsg
    往除自己之外的SlowQuorum成员发送”accept”形式的消息。并且带上deps和seq为finalDeps和finalSeq。这个消息会在Phase2Reply被Replica处理。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
Phase1Slow(cleader, i, Q) ==
/\ i \in leaderOfInst[cleader]
/\ Q \in SlowQuorums(cleader)
/\ \E record \in cmdLog[cleader]:
/\ record.inst = i
/\ record.status = "pre-accepted"
/\ LET replies == {msg \in sentMsg:
/\ msg.inst = i
/\ msg.type = "pre-accept-reply"
/\ msg.dst = cleader
/\ msg.src \in Q
/\ msg.ballot = record.ballot} IN
/\ (\A replica \in (Q \ {cleader}): \E msg \in replies: msg.src = replica)
/\ LET finalDeps == UNION {msg.deps : msg \in replies}
finalSeq == Max({msg.seq : msg \in replies}) IN
/\ cmdLog' = [cmdLog EXCEPT ![cleader] = (@ \ {record}) \cup
{[inst |-> i,
status |-> "accepted",
ballot |-> record.ballot,
cmd |-> record.cmd,
deps |-> finalDeps,
seq |-> finalSeq ]}]
/\ \E SQ \in SlowQuorums(cleader):
(sentMsg' = (sentMsg \ replies) \cup
[type : {"accept"},
src : {cleader},
dst : SQ \ {cleader},
inst : {i},
ballot: {record.ballot},
cmd : {record.cmd},
deps : {finalDeps},
seq : {finalSeq}])
/\ UNCHANGED << proposed, executed, crtInst, leaderOfInst,
committed, ballots, preparing >>

Phase2

Phase2Reply

Phase2Reply处理在SlowPath中,从Command Leader发过来的”accept”消息。

这里的Enable条件是,在自己的日志cmdLog[replica]中按照msg.inst找到对应的记录,要求消息的ballot要么等于,要么大于日志中的ballot。

如果满足Enable条件,则可以进行状态转移:

  1. cmdLog
    修改自己的日志,状态为”accepted”,并且更新deps和seq为msg中传入的值。这个值是由finalDeps和finalSeq一起计算得到的。
  2. sentMsg
    发送”accept-reply”消息给cleader。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
Phase2Reply(replica) ==
\E msg \in sentMsg:
/\ msg.type = "accept"
/\ msg.dst = replica
/\ LET oldRec == {rec \in cmdLog[replica]: rec.inst = msg.inst} IN
/\ (\A rec \in oldRec: (rec.ballot = msg.ballot \/
rec.ballot[1] < msg.ballot[1]))
/\ cmdLog' = [cmdLog EXCEPT ![replica] = (@ \ oldRec) \cup
{[inst |-> msg.inst,
status |-> "accepted",
ballot |-> msg.ballot,
cmd |-> msg.cmd,
deps |-> msg.deps,
seq |-> msg.seq]}]
/\ sentMsg' = (sentMsg \ {msg}) \cup
{[type |-> "accept-reply",
src |-> replica,
dst |-> msg.src,
inst |-> msg.inst,
ballot|-> msg.ballot]}
/\ UNCHANGED << proposed, crtInst, executed, leaderOfInst,
committed, ballots, preparing >>

Phase2Finalize

Phase2Finalize是整个SlowQuorum过程的终点,cleader会收集各个Replica的消息,并提交Command。即对于cleader下的某个Instance i,和SlowQuorum Q,尝试完成Phase2的最终提交。

照例还是Enable条件,在自己的日志里面看看能不能找到i对应的状态为”accepted”的日志,如果找不到,那么也不用往下看了。
如果能找到,就需要在sentMsg中找出所有和这个Instance相关的,类型为”accept-reply”的消息(也就是各个Replica在Phase2Reply过程中发出的消息)。显然,对于Q中除cleader之外的replica,都需要发一条这样的消息才能继续提交。

下面就是状态转移,和Phase1Fast基本一致,就不另外说明了。

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
Phase2Finalize(cleader, i, Q) ==
/\ i \in leaderOfInst[cleader]
/\ Q \in SlowQuorums(cleader)
/\ \E record \in cmdLog[cleader]:
/\ record.inst = i
/\ record.status = "accepted"
/\ LET replies == {msg \in sentMsg:
/\ msg.inst = i
/\ msg.type = "accept-reply"
/\ msg.dst = cleader
/\ msg.src \in Q
/\ msg.ballot = record.ballot} IN
/\ (\A replica \in (Q \ {cleader}): \E msg \in replies:
msg.src = replica)
/\ cmdLog' = [cmdLog EXCEPT ![cleader] = (@ \ {record}) \cup
{[inst |-> i,
status |-> "committed",
ballot |-> record.ballot,
cmd |-> record.cmd,
deps |-> record.deps,
seq |-> record.seq ]}]
/\ sentMsg' = (sentMsg \ replies) \cup
{[type |-> "commit",
inst |-> i,
ballot |-> record.ballot,
cmd |-> record.cmd,
deps |-> record.deps,
seq |-> record.seq]}
/\ committed' = [committed EXCEPT ![i] = @ \cup
{<<record.cmd, record.deps, record.seq>>}]
/\ leaderOfInst' = [leaderOfInst EXCEPT ![cleader] = @ \ {i}]
/\ UNCHANGED << proposed, executed, crtInst, ballots, preparing >>

Recovery

下面是Recovery相关操作。

SendPrepare

这里的replica就是论文里面的Replica L。其中,Enable条件:

  1. replica并不是i这个Instance的Leader
    这里注释掉一句,是replica并没有prepare这个instance。【Q】我不清楚为什么这个被注释掉。
  2. 目前使用过的ballots不超过MaxBallot
    这个应该是防止最后算法不会终止
  3. replica当前的日志中,不存在任何Instance为i的日志是已提交的(即其status为”committed”和”executed”)。

状态转移:

  1. sentMsg
    从这个replica向一个SlowQuorum,即Q发送”prepare”消息。
    这里注意,更新ballot为<< ballots, replica >>,这里的ballots是全局最大的ballot值。
  2. ballots
    更新全局最大的ballots,自增1。
  3. preparing
    将当前replica的preparing集合中增加Instance i。
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
SendPrepare(replica, i, Q) ==
/\ i \notin leaderOfInst[replica]
\*/\ i \notin preparing[replica]
/\ ballots <= MaxBallot
/\ ~(\E rec \in cmdLog[replica] :
/\ rec.inst = i
/\ rec.status \in {"committed", "executed"})
/\ sentMsg' = sentMsg \cup
[type : {"prepare"},
src : {replica},
dst : Q,
inst : {i},
ballot : {<< ballots, replica >>}]
/\ ballots' = ballots + 1
/\ preparing' = [preparing EXCEPT ![replica] = @ \cup {i}]
/\ UNCHANGED << cmdLog, proposed, executed, crtInst,
leaderOfInst, committed >>

ReplyPrepare

ReplyPrepare处理来自SendPrepare里面replica的”prepare”消息。下面进行讨论:

  1. 如果自己的日志中,存在一条对应于msg里面instance的日志,并且消息中的ballot要大于日志中的ballot。
    状态转移:
    1. sentMsg
      将来自SendPrepare里面replica的”prepare”消息删除,并重新发送一条”prepare-reply”消息给msg.src。
      消息中的ballot为自己的msg.ballot,prev_ballot为rec.ballot。根据前文,msg.ballot肯定是大于rec.ballot的。
      消息中的deps和seq沿用自己本地日志中的。【Q】这里很奇怪,似乎我们不在ReplyPrepare阶段对deps和seq决议。
    2. cmdLog
      删除自己日志中的rec,并且增加一条新条目。这个新条目和rec大致一样,只是将ballot更新为msg中的ballot。
    3. leaderOfInst
      如果日志中的instance的Command Leader是replica,那么将它移出leaderOfInst[replica]。否则保持不变。
      【Q】这里是啥意思,重新选一个Command Leader,还是直接走Basic Paxos那一套提交呢?
  2. 如果在自己日志中,不存在对应于msg里面instance的日志。
    状态转移:
    1. sentMsg
      发送”prepare-reply”消息。
      ballot为消息中传来的ballot,并且prev_ballot为<< 0, replica >>,相当于是一开始的ballot。【Q】msg.ballot肯定是大于rec.ballot的么?
      其他的字段也是设置成默认值:status为”not-seen”。cmd为none。deps为{},seq为0。
    2. cmdLog
      参照sentMsg的变更
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
ReplyPrepare(replica) ==
\E msg \in sentMsg :
/\ msg.type = "prepare"
/\ msg.dst = replica
/\ \/ \E rec \in cmdLog[replica] :
/\ rec.inst = msg.inst
/\ msg.ballot[1] > rec.ballot[1]
/\ sentMsg' = (sentMsg \ {msg}) \cup
{[type |-> "prepare-reply",
src |-> replica,
dst |-> msg.src,
inst |-> rec.inst,
ballot|-> msg.ballot,
prev_ballot|-> rec.ballot,
status|-> rec.status,
cmd |-> rec.cmd,
deps |-> rec.deps,
seq |-> rec.seq]}
/\ cmdLog' = [cmdLog EXCEPT ![replica] = (@ \ {rec}) \cup
{[inst |-> rec.inst,
status|-> rec.status,
ballot|-> msg.ballot,
cmd |-> rec.cmd,
deps |-> rec.deps,
seq |-> rec.seq]}]
/\ IF rec.inst \in leaderOfInst[replica] THEN
/\ leaderOfInst' = [leaderOfInst EXCEPT ![replica] =
@ \ {insrec.t}]
/\ UNCHANGED << proposed, executed, committed,
crtInst, ballots, preparing >>
ELSE UNCHANGED << proposed, executed, committed, crtInst,
ballots, preparing, leaderOfInst >>

\/ /\ ~(\E rec \in cmdLog[replica] : rec.inst = msg.inst)
/\ sentMsg' = (sentMsg \ {msg}) \cup
{[type |-> "prepare-reply",
src |-> replica,
dst |-> msg.src,
inst |-> msg.inst,
ballot|-> msg.ballot,
prev_ballot|-> << 0, replica >>,
status|-> "not-seen",
cmd |-> none,
deps |-> {},
seq |-> 0]}
/\ cmdLog' = [cmdLog EXCEPT ![replica] = @ \cup
{[inst |-> msg.inst,
status|-> "not-seen",
ballot|-> msg.ballot,
cmd |-> none,
deps |-> {},
seq |-> 0]}]
/\ UNCHANGED << proposed, executed, committed, crtInst, ballots,
leaderOfInst, preparing >>

PrepareFinalize

SendPrepare里面的replica,也就是所谓的Replica L,在收到对端的”prepare-reply”消息后,会走到PrepareFinalize中。这个函数也是最为复杂的。

Enable条件:

  1. i要在preparing[replica]中
    也就是确认当前replica是Replica L
  2. replica的日志中有i这个Instance,并且还没被提交
  3. Q中所有的replica都给当前replica的发送”prepare-reply”回复(replies),并且:
    下面会讨论四种情况,总体是”越来越惨”的
    1. 如果这些replies中的某个com的status是已提交(即”committed”, “executed”)
      【Q】为什么会有这种情况?感觉应该是因为在FastPath的Phase1Fast或者SlowPath的Phase2Finalize之后,cleader宕机导致的。
      那么就将这个Instance i移出preparing[replica]。并且在sentMsg中删除所有的replies。
      【Q】感觉这就相当于直接让它往后提交了?
    2. 如果这些replies中没有status是已提交(即”committed”, “executed”),但是存在acc是**”accepted”**的。
      同时还需要检查acc的prev_ballot大于等于(如果其他消息不是”accept”状态,那么就默认acc的大)所有其他消息的prev_ballot
      状态转移:
      1. sentMsg
        删除所有的replies,并且对除当前replica之外的所有Q,都发送一条”accept”消息。
        这个消息的ballot为自己日志中的ballot。
        关键内容,即cmd、deps和seq,都设置为acc传过来的。
        【Q】为什么replies里面prev_ballot最大的那个消息是”accpeted”,就可以以它为准走”accept流程”?
      2. cmdLog
        参照sentMsg创建一个新条目。

因为太长了,所以后面两种情况拆到下面讨论

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
PrepareFinalize(replica, i, Q) ==
/\ i \in preparing[replica]
/\ \E rec \in cmdLog[replica] :
/\ rec.inst = i
/\ rec.status \notin {"committed", "executed"}
/\ LET replies == {msg \in sentMsg :
/\ msg.inst = i
/\ msg.type = "prepare-reply"
/\ msg.dst = replica
/\ msg.ballot = rec.ballot} IN
/\ (\A rep \in Q : \E msg \in replies : msg.src = rep)
/\ \/ \E com \in replies :
/\ (com.status \in {"committed", "executed"})
/\ preparing' = [preparing EXCEPT ![replica] = @ \ {i}]
/\ sentMsg' = sentMsg \ replies
/\ UNCHANGED << cmdLog, proposed, executed, crtInst, leaderOfInst,
committed, ballots >>
\/ /\ ~(\E msg \in replies : msg.status \in {"committed", "executed"})
/\ \E acc \in replies :
/\ acc.status = "accepted"
/\ (\A msg \in (replies \ {acc}) :
(msg.prev_ballot[1] <= acc.prev_ballot[1] \/
msg.status # "accepted"))
/\ sentMsg' = (sentMsg \ replies) \cup
[type : {"accept"},
src : {replica},
dst : Q \ {replica},
inst : {i},
ballot: {rec.ballot},
cmd : {acc.cmd},
deps : {acc.deps},
seq : {acc.seq}]
/\ cmdLog' = [cmdLog EXCEPT ![replica] = (@ \ {rec}) \cup
{[inst |-> i,
status|-> "accepted",
ballot|-> rec.ballot,
cmd |-> acc.cmd,
deps |-> acc.deps,
seq |-> acc.seq]}]
/\ preparing' = [preparing EXCEPT ![replica] = @ \ {i}]
/\ leaderOfInst' = [leaderOfInst EXCEPT ![replica] = @ \cup {i}]
/\ UNCHANGED << proposed, executed, crtInst, committed, ballots >>

下面是后两种情况:

  1. Q中所有的replica都给当前replica的发送”prepare-reply”回复(replies),并且:
    1. 第一种情况;已经讨论
    2. 第二种情况:已经讨论
    3. 如果这些replies中,同时没有”committed”、”executed”、”accept”状态,但是有”pre-accepted”
      将replies中所有的”pre-accepted”提出来为preaccepts,又分为三种情况:
      1. preaccepts里面任意两个的cmd、deps和seq都相等。并且preaccepts中没有一个消息是从Instance i最初的Command Leader即i[1]发出的。并且Q中所有的replica都发了”pre-accepted”给当前的replica。
        执行状态转移:
        1. sentMsg
          从当前replica向Q中所有其他replica发送”accept”。
          cmd、deps和seq取其中任意一个就行,因为都相等。
        2. cmdLog
          参照sentMsg
        3. preparing
          在preparing[replica]移除掉Instance i。
        4. leaderOfInst
          在leaderOfInst[replica]移除掉Instance i。
      2. 如果和之前一样,但Q中只有大于Cardinality(Q) \div 2个replica发送了”pre-accepted”
        执行状态转移:
        1. sentMsg
          这也是全局唯一会走到ReplyTryPreaccept流程里面的情况,对应了优化算法
          从当前replica向Q中所有其他replica发送”try-pre-accept”。
          注意,这个消息也要发送给自己,所以和上一个情况是不同的处理策略。
          cmd、deps和seq的处理办法和上面是一样的。
      3. 如果preaccepts不为空,并且满足下面三个条件之一:连cmd、deps和seq都不完全一样了,或者Cardinality(preaccepts)也小于Cardinality(Q) \div 2或者preaccepts中存在一个消息是从Instance i最初的Command Leader即i[1]发出的
        执行状态转移:
        1. 在preaccepts中CHOOSE一个cmd不为none的pac,执行StartPhase1
          但是和Propose的处理不同,这里会带上rec.ballot, replies作为Ballot和oldMsg参数。
          而replies会在StartPhase1中被直接干掉(从sendMsg里面删除掉)。
        2. preparing
          去掉i
    4. 如果这些replies中,状态都是”not-seen”的
      执行状态转移:
      1. 同样执行StartPhase1,但cmd为none。
      2. preparing
        去掉i
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
...
\/ /\ ~(\E msg \in replies :
msg.status \in {"accepted", "committed", "executed"})
/\ LET preaccepts == {msg \in replies : msg.status = "pre-accepted"} IN
(\/ /\ \A p1, p2 \in preaccepts :
p1.cmd = p2.cmd /\ p1.deps = p2.deps /\ p1.seq = p2.seq
/\ ~(\E pl \in preaccepts : pl.src = i[1])
/\ Cardinality(preaccepts) >= Cardinality(Q) - 1
/\ LET pac == CHOOSE pac \in preaccepts : TRUE IN
/\ sentMsg' = (sentMsg \ replies) \cup
[type : {"accept"},
src : {replica},
dst : Q \ {replica},
inst : {i},
ballot: {rec.ballot},
cmd : {pac.cmd},
deps : {pac.deps},
seq : {pac.seq}]
/\ cmdLog' = [cmdLog EXCEPT ![replica] = (@ \ {rec}) \cup
{[inst |-> i,
status|-> "accepted",
ballot|-> rec.ballot,
cmd |-> pac.cmd,
deps |-> pac.deps,
seq |-> pac.seq]}]
/\ preparing' = [preparing EXCEPT ![replica] = @ \ {i}]
/\ leaderOfInst' = [leaderOfInst EXCEPT ![replica] = @ \cup {i}]
/\ UNCHANGED << proposed, executed, crtInst, committed, ballots >>
\/ /\ \A p1, p2 \in preaccepts : p1.cmd = p2.cmd /\
p1.deps = p2.deps /\
p1.seq = p2.seq
/\ ~(\E pl \in preaccepts : pl.src = i[1])
/\ Cardinality(preaccepts) < Cardinality(Q) - 1
/\ Cardinality(preaccepts) >= Cardinality(Q) \div 2
/\ LET pac == CHOOSE pac \in preaccepts : TRUE IN
/\ sentMsg' = (sentMsg \ replies) \cup
[type : {"try-pre-accept"},
src : {replica},
dst : Q,
inst : {i},
ballot: {rec.ballot},
cmd : {pac.cmd},
deps : {pac.deps},
seq : {pac.seq}]
/\ preparing' = [preparing EXCEPT ![replica] = @ \ {i}]
/\ leaderOfInst' = [leaderOfInst EXCEPT ![replica] = @ \cup {i}]
/\ UNCHANGED << cmdLog, proposed, executed,
crtInst, committed, ballots >>
\/ /\ \/ \E p1, p2 \in preaccepts : p1.cmd # p2.cmd \/
p1.deps # p2.deps \/
p1.seq # p2.seq
\/ \E pl \in preaccepts : pl.src = i[1]
\/ Cardinality(preaccepts) < Cardinality(Q) \div 2
/\ preaccepts # {}
/\ LET pac == CHOOSE pac \in preaccepts : pac.cmd # none IN
/\ StartPhase1(pac.cmd, replica, Q, i, rec.ballot, replies)
/\ preparing' = [preparing EXCEPT ![replica] = @ \ {i}]
/\ UNCHANGED << proposed, executed, crtInst, committed, ballots >>)
\/ /\ \A msg \in replies : msg.status = "not-seen"
/\ StartPhase1(none, replica, Q, i, rec.ballot, replies)
/\ preparing' = [preparing EXCEPT ![replica] = @ \ {i}]
/\ UNCHANGED << proposed, executed, crtInst, committed, ballots >>

ReplyTryPreaccept

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
ReplyTryPreaccept(replica) ==
\E tpa \in sentMsg :
/\ tpa.type = "try-pre-accept"
/\ tpa.dst = replica
/\ LET oldRec == {rec \in cmdLog[replica] : rec.inst = tpa.inst} IN
/\ \A rec \in oldRec : rec.ballot[1] <= tpa.ballot[1] /\
rec.status \notin {"accepted", "committed", "executed"}
/\ \/ (\E rec \in cmdLog[replica] \ oldRec:
/\ tpa.inst \notin rec.deps
/\ \/ rec.inst \notin tpa.deps
\/ rec.seq >= tpa.seq
/\ sentMsg' = (sentMsg \ {tpa}) \cup
{[type |-> "try-pre-accept-reply",
src |-> replica,
dst |-> tpa.src,
inst |-> tpa.inst,
ballot|-> tpa.ballot,
status|-> rec.status]})
/\ UNCHANGED << cmdLog, proposed, executed, committed, crtInst,
ballots, leaderOfInst, preparing >>
\/ /\ (\A rec \in cmdLog[replica] \ oldRec:
tpa.inst \in rec.deps \/ (rec.inst \in tpa.deps /\
rec.seq < tpa.seq))
/\ sentMsg' = (sentMsg \ {tpa}) \cup
{[type |-> "try-pre-accept-reply",
src |-> replica,
dst |-> tpa.src,
inst |-> tpa.inst,
ballot|-> tpa.ballot,
status|-> "OK"]}
/\ cmdLog' = [cmdLog EXCEPT ![replica] = (@ \ oldRec) \cup
{[inst |-> tpa.inst,
status|-> "pre-accepted",
ballot|-> tpa.ballot,
cmd |-> tpa.cmd,
deps |-> tpa.deps,
seq |-> tpa.seq]}]
/\ UNCHANGED << proposed, executed, committed, crtInst, ballots,
leaderOfInst, preparing >>

FinalizeTryPreAccept

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
FinalizeTryPreAccept(cleader, i, Q) ==
\E rec \in cmdLog[cleader]:
/\ rec.inst = i
/\ LET tprs == {msg \in sentMsg : msg.type = "try-pre-accept-reply" /\
msg.dst = cleader /\ msg.inst = i /\
msg.ballot = rec.ballot} IN
/\ \A r \in Q: \E tpr \in tprs : tpr.src = r
/\ \/ /\ \A tpr \in tprs: tpr.status = "OK"
/\ sentMsg' = (sentMsg \ tprs) \cup
[type : {"accept"},
src : {cleader},
dst : Q \ {cleader},
inst : {i},
ballot: {rec.ballot},
cmd : {rec.cmd},
deps : {rec.deps},
seq : {rec.seq}]
/\ cmdLog' = [cmdLog EXCEPT ![cleader] = (@ \ {rec}) \cup
{[inst |-> i,
status|-> "accepted",
ballot|-> rec.ballot,
cmd |-> rec.cmd,
deps |-> rec.deps,
seq |-> rec.seq]}]
/\ UNCHANGED << proposed, executed, committed, crtInst, ballots,
leaderOfInst, preparing >>
\/ /\ \E tpr \in tprs: tpr.status \in {"accepted", "committed", "executed"}
/\ StartPhase1(rec.cmd, cleader, Q, i, rec.ballot, tprs)
/\ UNCHANGED << proposed, executed, committed, crtInst, ballots,
leaderOfInst, preparing >>
\/ /\ \E tpr \in tprs: tpr.status = "pre-accepted"
/\ \A tpr \in tprs: tpr.status \in {"OK", "pre-accepted"}
/\ sentMsg' = sentMsg \ tprs
/\ leaderOfInst' = [leaderOfInst EXCEPT ![cleader] = @ \ {i}]
/\ UNCHANGED << cmdLog, proposed, executed, committed, crtInst,
ballots, preparing >>

Reference

  1. There Is More Consensus in Egalitarian Parliaments
  2. EPaxos Revisited
  3. https://github.com/efficient/epaxos/blob/master/tla%2B/EgalitarianPaxos.tla
    一份TLA+的说明