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_A和obj_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_B写obj_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

找到发给自己的”try-pre-accept”的请求tpa，首先找到自己日志中所有Instance等于tpa.inst的条目oldRec，进行校验：

  1. tpa的ballot number要大于等于所有oldRec中的ballot number
  2. 所有oldRec中的状态不能是{“accepted”, “committed”, “executed”}

然后进行讨论：

  1. 如果在oldRec之外，存在某个rec，和tpa是冲突的
    如果tpa.inst不属于rec.deps，并且要么rec.inst不属于tpa.deps，要么rec.seq大于tpa.seq。那么rec和tpa是冲突的。
    如果存在冲突的话，则执行状态转换：
    1. sentMsg
      消费掉tpa消息，并且回复”try-pre-accept-reply消息。
      此时，status为rec.status。
    2. cmdLog
      不做改动，可以认为是拒绝了这个消息。
  2. 如果对于oldRec之外的的所有rec，都和tpa不冲突
    执行状态转换：
    1. sentMsg
      消费掉tpa消息，并且回复”try-pre-accept-reply”消息。
      注意，status的值是”OK”，这个和冲突情况不一样。【Q】如果此时status的值为”pre-accepted”，那么在FinalizeTryPreAccept中，这条日志仍有被提交的希望？
    2. cmdLog
      删除所有的oldRec，也就是自己日志中所有有关Instance的日志。
      新增一条”pre-accepted”日志，这就相当于走完了StartPhase1。
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

选出自己Instance为i的日志rec，在所有”try-pre-accept-reply”回复中，取出Instance为i且ballot为rec.ballot的回复，构成集合tprs。
那么对于Q中的任意一个r，tprs中肯定有一条消息是从r中发出的。也就是说必须得Q中每一个Replica都回复了”try-pre-accept-reply”，这个也是老生常谈的条件。

下面是三种情况的讨论：

  1. \A tpr \in tprs: tpr.status = "OK"
    这说明在ReplyTryPreaccept中，大家都没冲突。这个类似于PrepareFinalize中的accept流程，也就是论文中所谓的Paxos-Accept phase。执行状态转换：
    1. sentMsg
      直接发送”accept”消息给Q，后面就是走Phase2Reply的流程。
    2. cmdLog
      设置status为”accepted”
  2. 如果在tpr中存在某个status为{“accepted”, “committed”, “executed”}的消息
    走StartPhase1
  3. 如果tpr.status不全是”OK”，也有”pre-accepted”
    这里应该是冲突了，所以直接干掉。
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+的说明