激励全局稳定化 - The Trail of Bits Blog

共识协议与GST假设

共识协议在许多应用中扮演着关键角色。Fischer、Lynch和Paterson的经典不可能性结果表明，在合理假设下，协议可能无法达成共识。在Dwork、Lynch和Stockmeyer的论文《部分同步下的共识》（DLS论文）中，作者通过引入以下“全局稳定时间”（GST）假设绕过了这一不可能性结果：

对于每次执行，存在一个处理器未知的全局稳定时间（GST），使得消息系统从GST时刻起遵守上界Δ。

换句话说，GST是一个时间点，此后所有网络消息的延迟最多为Δ。Dwork、Lynch和Stockmeyer表明，在这一假设下，可以构建一个保证达成共识的协议。

但表面上看，这一假设可能显得不切实际。毕竟，真实网络并非如此运作！想想你家或办公室的网络。不太可能在某神奇时间点后，网络从此永远可靠响应。

那么，为什么你应该关心？尽管GST假设看似不现实，但它具有巨大效用，正如我们在本文中解释的：

可以将共识视为两个玩家之间的游戏，而GST假设是限制其中一个玩家移动的手段。从这个角度看，该假设非常自然，甚至优雅。
在这一假设下达成共识的协议展现出非常有用的属性：它们可以从任何由延迟导致的配置中恢复。因此，在这一假设下证明协议正确性不仅具有理论意义，还具有具体实际意义。

我们首先回顾Fischer、Lynch和Paterson的经典不可能性结果，这为DLS论文奠定了基础。然后，我们在两个玩家的游戏背景下讨论GST假设，将GST作为限制其中一个玩家移动的手段。最后，我们阐明在GST假设下证明协议正确性的实际意义。

FLP不可能性结果

在《具有一个故障过程的分布式共识不可能性》中，Fischer、Lynch和Paterson表明，在非常温和的假设下，一组过程可能无法达成共识。这被称为FLP不可能性结果。DLS论文引入了GST假设，使得绕过这一结果成为可能，正如EATCS在2007年授予该论文Edsger W. Dijkstra分布式计算奖的引文中所强调的：

本文引入的最终同步[假设GST]方法……此后被确立为绕过FLP不可能性结果并解决异步共识、原子广播和状态机复制的主要方法。

在本节中，我们描述Fischer、Lynch和Paterson证明的主要思想，为DLS论文的工作提供背景。

模型

在FLP模型中，两个或更多过程交换消息，试图就值0或1达成一致。每个过程都有一个一次性写入的输出寄存器，初始为空。一旦过程认为值已达成一致，就将该值写入其输出寄存器。

如果至少一个过程将值写入其输出寄存器，且没有其他过程将相反值写入其自己的输出寄存器，则过程达成共识。注意，这一定义极其宽松。例如，可能期望所有过程必须将相同值写入其输出寄存器。采用如此宽松的定义强化了FLP结果。

配置包括所有过程的内部状态（包括其输出寄存器）以及所有已发送但尚未传递的消息。事件e是一对(p, m)，由消息m和过程p组成。在后续证明讨论中，我们使用“e被传递”而非“m被传递给p”的语言。此外，我们说“e0, e1, …在配置C0中被传递”表示以下含义：

e0在配置C0中被传递，导致某些配置C1。
e1在配置C1中被传递，导致某些配置C2。
依此类推。

协议可能以两种方式出错：

任何消息可能被延迟任意但有限的时间。
一个过程可能崩溃；即，一个过程可能停止响应消息。

注意，如果过程未收到预期消息，它无法知道消息是简单延迟还是发送方已崩溃。

Fischer、Lynch和Paterson表明，在此模型中，无法保证共识。

证明

这里，我们尝试给出FLP结果证明的直观理解。我们的描述故意有些快速和松散。更详细的解释，我们推荐Henry Robinson的博客文章《FLP不可能性简要导览》。

考虑作者的中心引理，其基本含义如下。如果C是双价配置——意味着决策值0和1都可能——且e是在C中可传递的事件，则e可以以导致双价配置的方式传递。更精确地说，存在以e结尾的事件序列，这些事件在C中可传递并导致双价配置。使用这一引理，作者表明可以以永远无法达成一致值的方式传递所有消息。

引理的证明基本如下。设C是任何可能达成0或1的配置，设e是任何在C中可传递的事件。考虑通过传递以e结尾的事件序列产生的配置。通过反证法，假设任何此类配置只允许达成0或1，但没有任何此类配置允许两种可能性（即，没有此类配置是双价的）。

作者表明，在这些假设下，两种类型的配置都必须存在：只允许达成0的配置和只允许达成1的配置。事实上，作者表明必须存在配置C0、与e相同过程的事件e’以及值i ∈ {0, 1}，使得以下成立：

如果在C0中传递e，则只能达成i。
如果在C0中传递e’然后e，则只能达成1 – i。

（此时查看图1可能有帮助。）

本质上，在C0中传递e将过程锁定到值i，而在C0中传递e’然后e将过程锁定到值1 – i。（我们发现jbapple的StackExchange回答有助于理解证明的这一部分。）

现在，设p是e和e’中指定的接收过程。因为过程p可能崩溃，必须存在在C0中可传递的事件序列σ，不涉及p，并导致协议。设A为结果配置，设j为达成值。注意，这里达成j不涉及e或e’，因为两者都不在σ中。

另一方面，虽然过程p可能崩溃，但它可能不会；往返p的消息可能只是延迟。回想一下，其他过程无法区分这两种情况。因此，如果往返p的消息只是延迟，配置A应该可达。此外，事件e和e’应该在A中可传递。

考虑在A中传递e产生的配置。此配置应与在C0中传递e然后σ产生的配置相同，因为σ不涉及p。接下来，考虑在A中传递e’然后e产生的配置。同样，因为σ不涉及p，结果应与在C0中传递e’、然后e、然后σ的结果相同。（参见图1。）

图1：FLP结果中心引理证明中使用的图表

总结，从C0出发，有三个关键路径点：

如果传递e，过程达成i（D0）。
如果传递e’然后e，过程达成1 – i（D1）。
如果传递σ，过程达成j（A）。（记住，e和e’都不在σ中。）

但e和e’在A中可传递。在A中传递e应导致达成i（E0），而在A中传递e’然后e应导致达成1 – i（E1）。然而，j已在A中达成，且j不能同时是i和1 – i。因此，产生矛盾。

限制对手

让我们回到DLS论文，其中包含以下段落：

将每种情况视为协议设计者和对手之间的游戏是有帮助的。……如果Δ最终成立[即GST假设成立]，对手选择Δ，设计者（知道Δ）提供共识协议，对手选择Δ必须开始成立的时间T。

我们可以进一步扩展这个比喻。在承诺时间T（GST）后，对手模拟提供的共识协议。回想一下，协议可能以两种方式出错：消息可能被延迟，一个过程可能崩溃。可以将延迟消息或使过程崩溃视为对手可用的移动。如果对手能使协议违反其正确性条件之一，则对手获胜。具体来说，如果对手能使两个过程将不同值写入其输出寄存器，或能使模拟无限运行而没有任何过程将值写入其输出寄存器，则对手获胜。

考虑到这一点，人们可能将FLP结果解释为：在没有GST假设阻碍的情况下，对手无法被击败。换句话说，在上述游戏中，对手总是有（可能无限的）获胜移动序列。

让我们给对手一个形象。什么样的对手可能延迟消息或导致过程崩溃？我们喜欢想到电气风暴。

想象一群住宅试图通过电话线通信。（这曾经是件事。）风暴可能通过电磁干扰将噪声引入线路，导致消息必须重传从而延迟（图2）。此外，闪电可能击中一个不幸的住宅，导致它……嗯，停止响应消息（图3）。

图2：作为电气风暴，对手可以使用电磁干扰导致消息必须重传从而延迟。

图3：对手可以使一个不幸的住宅（过程）崩溃（即停止响应消息）。

GST如何融入这个类比？GST的到来意味着天空已放晴。这里，类比不完美，所以我们必须稍微歪曲现实。通常，人们可以望向窗外看到天空已放晴，但就我们的目的而言，图2和图3中的居民没有窗户！回想一下上面引用的段落，协议设计者在对手选择GST之前提供协议。因此，实际上，对手知道GST，但执行协议的过程不知道。

我们的下一个问题是，我们如何平衡竞争环境？我们可以对对手施加什么限制以给协议获胜的机会？

对手已经在某些方面受到限制。例如，虽然它可以延迟无限多条消息，但它只能延迟任何消息有限的时间。如果这种有限性限制扩展到对手可以影响的消息集合会怎样？也就是说，如果对手仅限于延迟有限数量的消息有限的时间会怎样？

这一提议实际上是陈述GST假设的另一种方式，DLS论文表明以这种方式受限的对手可以被击败。换句话说，存在在GST假设下保证达成共识的协议。在电气风暴比喻的背景下，如果天空最终放晴，可以达成决策（图4）。

图4：直观上，DLS结果表明如果天空最终放晴，可以达成决策。

假设GST如何绕过FLP结果？回想一下，证明的中心引理依赖于过程无法区分另一个过程p是否已崩溃，或往返p的消息是否延迟。在GST假设下，这一推理在GST之前有效，但在之后无效。更精确地说，过程无法区分以下两种情况：

过程p已崩溃。
往返p的消息延迟且GST尚未到来。

回想一下，过程无法知道GST何时到来，因此拥有GST假设与不拥有它之间的差异非常微妙。尽管如此，DLS论文表明这种差异足以保证可以达成共识。

从这个角度看，GST假设非常优雅。它是对逻辑公式的微小调整。它扩展了模型中已经存在的概念，即有限性。

现在，我们并非建议应追求数学优雅而非真理。我们只是注意到，当以这种方式看待时，GST假设是优雅的。此外，考虑到下一节的观察，这种优雅只是锦上添花。

从延迟中恢复

在将共识协议视为与对手游戏时，协议获胜意味着什么？

回想一下，对手可以延迟任何消息任意但有限的时间直到GST。在GST时，对手必须离开。因为对手选择GST，它可以使协议处于任何可能由延迟导致的配置。

接下来，回想正确的协议必须最终达成决策；即，某些过程必须将值写入其输出寄存器。因此，如果协议在GST假设下被证明正确，它必须无论其在GST时的配置如何都能达成决策。如上所述，协议在GST时的配置可能是任何可能由延迟导致的配置。

因此，如果协议可以击败对手，它可以从任何可能由延迟导致的配置中达成决策。

这一点值得强调，因为此类协议的存在相当显著。想象所有消息可能被延迟的方式。注意，消息传递的及时性可能影响随后产生的消息。换句话说，过程可能根据超时是否在收到某些其他消息之前发生来决定发送哪条消息。因此，很可能，可能由延迟导致的配置数量巨大。选择任何此类配置，将协议放入该配置，并让其运行。如果协议在GST假设下被证明正确，它将最终达成决策。

请记住，任何可能由延迟导致的配置并不意味着任何配置。例如，如果p从未发送m，对手无法将协议置于p已发送m的配置中。尽管如此，可能配置的数量可能巨大，能够从任何其中达成决策相当惊人。

结论

虽然GST假设可能显得人为，它只是对逻辑公式的优雅调整。此外，在GST假设下证明协议正确性具有深远意义：无论延迟如何施加于协议，只要它们消退，协议就可以恢复并达成决策。

当然，GST假设可能不适用于所有协议，例如那些预期在延迟无休止且过于频繁以致GST假设无意义的环境中运行的协议。此类协议可能需要一些其他假设来证明其正确性。

此外，证明协议正确性并不意味着其实现正确。例如，开发人员可能认为他们假设GST，而实际上他们假设了更强的东西。例如，开发人员可能对GST何时到来做出假设。

在Trail of Bits，我们建议对每个共识协议实现进行安全审计。如果我们可以在这方面帮助您，请联系！

最后说明，在准备本文时，我们遇到了Ittai Abraham的帖子《部分同步的风味》，从稍不同的视角看待GST假设。我们鼓励您也阅读他的帖子。

致谢

这项研究由Trail of Bits进行，基于DARPA根据合同号HR001120C0084支持的工作（分发声明A，批准公开发布：分发无限制）。本材料中表达的任何意见、发现、结论或建议均为作者的观点，不一定反映美国政府或DARPA的观点。

如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News

全局稳定时间（GST）假设：突破FLP不可能性，实现分布式共识

本文深入探讨了分布式共识中的全局稳定时间（GST）假设，解释了其如何绕过FLP不可能性结果，并分析了其在协议恢复和实际应用中的重要性。文章还通过游戏理论视角和电气风暴类比，生动阐述了GST的优雅性和实用性。