导读
对于每一个分布式系统来说，safety和liveness都是核心问题，前者强调节点之间状态要满足某些约束，而后者强调诚实节点的状态不能一直停滞不前。
然而FLP定理说了这样一件事：在消息可能无限延迟的情况下（异步网络），即使系统存在一个可能故障的节点，也不存在一个满足safety又保证在有限时间内终止的确定性共识算法。
所以safety和liveness是一对矛盾，如同线段的两个端点，每一个分布式系统都落在线段某个端点上，而不能同时占据两点。
但实际上，消息不会无限延迟，大部分时间里，消息到达都有一个时间上限。因此共识算法虽然在理论上不是完美的，但在实践中已经足够了。
本文用平白的语言讨论basic-hotstuff对safety和liveness的证明，并配上图例来帮助理解。
回顾basic-hotstuff
basic-hotstuff过程如下：
- NewView
- replica通过NewViewMSG把自己的PrepareQC发送给leader
- prepare阶段：
- leader收集各节点发送的NewView，选择其中view最高的qc_high， 基于此qc_high提出自己的proposal并且广播。
- replica收到proposal，通过SAFENODE()判断是否接受。如果接受，将
self.prepareQC = qc，就返回该proposal及自己对它的签名。
- PreCommit阶段：
- leader收集到n-f个签名后计算出qc，将其广播。
- replica收到qc后，将自己的PrepareQC = qc。并且继续对
<qc.type, qc.view, qc.node>进行签名。（将type纳入签名可以防止重放攻击）。
- commit阶段:
- ledaer收集n-f个pre-commit阶段的签名，计算qc并广播。
- replica收到qc后，锁定qc.node (self.locked_qc = qc)， 继续对
<qc.type, qc.view, qc.node>进行签名。
- decide阶段：
- leader收到n-f个 commit阶段的签名，计算qc并且广播，随后leader进行view change.
- replica收到qc后，执行proposal，并且进行view change。
SAFENODE() 函数是这样的:
注意， 在调用时，参数qc == node.justify ， 也就是node之前达成的最新共识，并非对node本身达成的共识。
safety证明
节点\分支冲突
<br />如上图，分支[1, 2]与[1, 2, 3], [1, 2, 4] 不冲突，但是[1, 2, 3]与[1, 2, 4]冲突。<br />节点1与2不冲突，2与3或者4都不冲突，因为都在同一个分支上。但是3和4冲突。
Valid quorum certificate
<br />首先定义什么样的qc是有效(valid)的：
- 门限签名函数
tverify(<qc.type, qc.viewNumber, qc.node>, qc.sig)返回true，表示qc是safe的。
什么意思，可以理解为节点A收到B发来的QC，通过B的公钥验证B确实对<qc.type, qc.viewNumber, qc.node>
签名了，那这个qc就是有效的。
引理1
 <br />任意有效的qc1, qc2, 满足qc1.type = qc2.type。如果qc1.node与qc2.node冲突，那么qc1.viewNumber != qc2.viewNumber.
这个通过反证法证明：假定qc1.viewnumber == qc2.viewnumber成立。
- type相同，表示这两个qc对应于同一个view的同一个阶段。
- 某个view的某个阶段中，一个诚实节点只投一次票。
- 同一个view下同一个阶段，形成一个qc需要超过2/3的诚实节点投票，形成两个qc就说明至少有一个诚实节点投了两次票，这跟诚实节点的定义矛盾。
- 证毕。
定理2
<br />**如果两个节点w和b相互冲突，那么w和b不可能同时被一个诚实节点提交**。换句话说，一个诚实节点提交了一个分支A之后，不可能再次提交一个与A冲突的分支B。
通过反证法证明，令qc1表示节点w的commitQC，qc2表示节点b的commitQC，各自的viewnumber是v1和v2。
- 假设两个节点w和b相互冲突，它们同时被一个诚实节点提交了。
- 根据引理1，可知v1 != v2, 下面假定v1 < v2。
随后定义了一个集合
E(prepareqc)和一个qcs，其性质为：
直观地看，qcs就是分支b上第一个与分支w冲突的节点对应的有效prepareQC，
qcs.node必然存在，比如它可以是节点b对应的prepareQC的node。在所有给qc1签名的节点中，令r是第一个给qcs签名的节点。r一定存在，不然没人给qc1和qcs投票了。
- 因为qc1.view = v1 < qcs.view = vs, 那么在vs前，r的locked_qc一直为qc1（图中节点w）。
- 那么在view=vs的prepare阶段，r通过
SAFENODE(qcs.node, qcs.node.justify)来判断是否接受qcs.node。我们借助上图来说明：- qcs.node与w冲突，因此
SAFENODE()第一个判断为假 - qcs.node.justify对应的是节点2，它的view=2 < w.view， 因此
SAFENODE()第二个判断为假
- qcs.node与w冲突，因此
- 所以
SAFENODE()返回假，因此r不可能接受qcs.node。 - 因此，不存在这样的r；这与上面的r一定存在相矛盾，因此假设不成立。
Liveness证明
在basic-hotstuff中没有明确定义选主和进入nextView，这两个函数不影响算法的safety，但是可能影响到liveness。
在证明中，假定系统有 n = 3f+1个节点。
match
证明liveness需要用到一个概念匹配(match):
- qc1与qc2匹配，等价于qc1和qc2都是有效的，而且他们的node和viewnumber都是一致的。
那么在一个view中， prepareQC, precommitQC, lockedQC, commitQC都相互匹配。
引理3
<br />证明很简单：按照算法流程，如果锁定了qc，那么在这个view的prepare阶段有 `n-f = 2f+1` 个给PrepareQC的投票，因为恶意节点最多f个，那么至少有f+1个诚实节点投给了prepareQC，也就是说：至少f+1个正确节点有prepareQC。那么下一个Leader收集的n-f个NewView，**必定包含了之前最新的QC-high。**
但是，不保证NewView中的qc-high是最新的，这要求leader告知所有节点，NewView可能返回一个安全的locked的QC，但不是最新的qc-high，可能产生临时分叉。解决办法：
- 引入decide阶段，让leader告知n-f个节点最新的qc-high。这是完整的hostuff实现需要的
- non-leader节点等待一段时间，提高leader抢先进入下一视图的概率。 （hotstuff-consensus没有实现decide阶段leader广播的操作，所以要等一等）
定理4
<br />如果网络环境进入稳定（GST之后），系统存在一段有界的持续时间T，在T之内所有节点都进入了view=v中，而且此时leader是诚实节点，那么在T内就可以达成共识。
啥意思？这个定理讨论了hotstuff进行view-change时的一些保证，就是在GST之后，上一轮消息可以传到下一轮，在若干个GST之后proposal会被提交。
证明过程：
- GST之后，所有节点都同步在view=v+1，leader也是诚实节点，这是前提。
- 假设在先前的view中，诚实节点中最高的lockedqc=qc，那么根据引理3，至少有f+1个诚实节点有匹配的prepareQC
在NewView阶段，leader收集n-f个newViewMsg，那么f+1个诚实节点会把qc发给leader, 因此leader一定收到了qc。
随后leader基于qc提出自己的proposal并且进行广播。那么根据前提，所有诚实的replica都会对其进行
SAFENODE()检查，如果判断成立，那么所有诚实节点都会接受这个proposal。- 这样，不断重复，总有一天会有三个连续proposal的确认，从而提交前面所有proposal。
那么SAFENODE()能否通过呢？论文中的论述是SAFENODE()的第二个分支也就是 qc.viewNumber > locked.viewNumber必定成立，从而SAFENODE()必定为真。
但是笔者举了个例子发现这个论断不一定满足：前一个view产生了lockedQC但是没有产生commitQC就进入下一个view，新leader发过来一个proposal其父节点是上一个view的proposal，那么此时判断不成立，因为qc == lockedQC.
笔者起初认为是自己没有理解论证过程，但是花了一些时间发现不对劲。后来查阅文献发现https://www.jianshu.com/p/0458a3bd9dc2这篇文章有人已对此提出质疑：27行的判断不一定成立，例子与笔者所想相近。但这不影响最终的结果，因为qc==lockedQC, 那么说明prop延伸自lockedQC.node, 因此第一个判断为真，因此SAFENODE()仍然为真。
上文的作者给出了一个修改的证明， SAFENODE(prop, prop.justify)中满足: prop.justify.viewNumber >= lockedQC.viewNumber。
那么被锁定的qc.node会被丢弃吗？不会：
- 上一轮共识已经生成了commitQC=qc，那qc已被提交执行。
- 如果上一轮共识中qc被锁定但未提交，那会不会出现下面这种情况？
如上图，a锁定在节点3， b在view=4时形成了prepareQC。a不会切换到分支[2, 4]， 因为 SAFENODE() 两个判断都为假。随后4还没进入下一阶段就发生了view change。新leader c基于节点4提出了proposal 5：
节点a收到proposal 5，进行 SAFENODE() 判断，第一个判断为假，但是第二个判断为真，因此进行分支切换，丢弃节点3。
这是不可能出现的，由引理3得知，a锁定在node 3，那么在node 3的prepare阶段有至少f+1个诚实节点投给了prepareQC, 剩下 2f < n-f 个节点，这些节点可能没收到node3， 但是它们全部加起来也不能给node 4生成prepareQC，因此不会出现后面的情况。
那么什么时候出现分支切换？如上图，如果3没有走到locked，那么就会出现分支切换。因为没有走到lock阶段，b的locked_qc.node = node 2。
其他
view\height与node的对应关系？
准确的表述是：
- 一个处于locked\committed的proposal，必定对应唯一一个view\height。
- 已锁定分支上的节点的view严格单调递增（不一定连续）。
- view相同的多个proposal，最多只有一个能形成qc。
1、2可通过safety算法中的两个fencing token来保证：
- vheight，只有大于vheight的节点才可能被节点接受。
- locked_node.height, 新节点的height只有大于这个height才可能被锁定。那么
v1 < v2 < v3 ...这种严格单调递增数列，一定是单射。
举个例子说明3：
- 第一种，就是这些节点p1, p2是冲突的。这可以由引理1保证。
- 第二中，类似
3<-4<-4<-4这条分支，思路还是引理1的反证法，任意两个quorum的交集至少有f+1个节点，其中至少有一个诚实节点它不会投给第二个4。但是第二个4仍然可以用来更新其前置节点的状态。
若有收获，就点个赞吧
0 人点赞
