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

共识协议与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。
依此类推。

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

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

注意，如果进程未收到它期望接收的消息，它无法知道消息是 simply delayed还是发送者已崩溃。

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

证明

这里，我们尝试给出FLP结果证明的直观理解。我们的描述 intentionally a little fast and loose。更详细的解释，我们推荐Henry Robinson的博客文章《FLP不可能性简要导览》。

考虑作者的中心引理，其 essentially 说明以下内容。如果C是一个二价配置——意味着决策值0和1都可能——且e是在C中可传递的事件，则e可以以导致二价配置的方式传递。更精确地说，存在一个以e结尾的事件序列，这些事件在C中可传递并导致二价配置。使用这一引理，作者表明，可以以从未达成任何值的方式传递所有消息。

引理的证明 essentially 如下。让C是任何可能达成0或1的配置，让e是任何在C中可传递的事件。考虑通过传递以e结尾的事件序列产生的配置。通过矛盾，假设任何此类配置只允许0或1达成一致，但 no such configuration allows both possibilities（即，没有此类配置是二价的）。

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

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

（此时瞥一眼图1可能有帮助。）

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

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

另一方面，虽然进程p可能崩溃，但它可能不会；往返p的消息可能 simply be delayed。回想一下，其他进程无法区分这两种情况。因此，如果往返p的消息 simply delayed，配置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假设阻碍的情况下，对手无法被击败。换句话说，在上述游戏中，对手总是有一个（可能无限的）获胜移动序列。

让我们给对手一个面孔。什么样的对手可能延迟消息或导致进程崩溃？我们喜欢想到 electrical storm。

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

图2：作为 electrical storm，对手可以使用 electrical interference 导致消息必须重传，从而延迟。

图3：对手可能导致一个不幸的房屋（进程）崩溃（即停止响应消息）。

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

我们的下一个问题是，我们如何 level the playing field？我们可以对对手施加什么限制以给协议获胜的机会？

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

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

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

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

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

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

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

现在，我们并非建议应追求数学优雅 over truth。我们 simply noting that，当以这种方式看待时，GST假设是优雅的。此外，考虑到下一节的观察，这种优雅 simply icing on the cake。

从延迟中恢复

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

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

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

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

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

请记住，任何可能由延迟导致的配置并不意味着任何配置。例如，如果p可能从未发送m，对手 cannot put the protocol into a configuration in which p has sent m。尽管如此，可能配置的数量可能巨大，能够从任何 of them 达成决策相当惊人。

结论

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

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

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

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

作为最后一点，在准备本文时，我们遇到了Ittai Abraham的《部分同步的风味》，它从 slightly different perspective 看待GST假设。我们鼓励您也阅读他的文章。

致谢

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

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

深入解析全局稳定时间（GST）假设及其在共识协议中的关键作用

本文探讨了分布式共识协议中的全局稳定时间（GST）假设，分析了其如何规避FLP不可能性结果，并阐述了GST假设在实际协议恢复和决策达成中的重要意义。