您如何对概率分布式系统进行推理？

不久前，我还对自己的分布式系统知识感到非常满意。我认为，真正需要有人来理解它们，就是透彻地理解paxos协议，并且不愿意按照TLA+的形象重塑您的大脑。也许可以添加少量无冲突的复制数据类型，这样您就知道什么是“最终一致性”。过去，只是一些优化和混搭很容易进入您被TLA+搞得头晕目眩的大脑。

多年来，这一信念被证明是出人意料的稳健，即使在分析Nano密码货币的尝试流产后也是如此。只有在遇到雪花共识协议家族后，我才意识到我的理论根本达不到挑战。问题是概率：雪花协议通过迭代随机轮询其他节点集来达成共识，而最终达成共识的论点是一个统计学论点，得出了失败概率的上限。

我不是不喜欢概率与统计学，我只是尽量保持距离。到目前为止，我在分布式系统中遇到的所有算法都涉及不确定性，当然，但不涉及概率。我以为非确定性只是一种更灵活的概率推理方式。当我学习了概率分布式系统的推理艺术时，我的这个想法将被证明是一个巨大的不必要的混乱的来源，所以我将帮你一个忙，用一句话给你整个帖子的核心教训：。

您是否曾经编写过一些多线程代码，愉快地在这里插入互斥体，在那里插入信号量，或者甚至只是使用一些很好的消息传递原语来使您的线程相处得很顺利？那么，也许您会熟悉下一步经常发生的事情。在您的脑海中划一划，一个想法--“哦，等等…。"；-正如您所意识到的，如果线程\(A\)在线程\(B\)完成其分配的任务之前设法到达某个步骤，将会发生一些奇怪的事情。不用担心！拍打另一个WaitHandle，问题就解决了。只是问题没有解决。不完全是。您考虑得更多一些--如果线程\(C\)在这个不合时宜的时候带着一条消息进来怎么办？您惊恐地意识到，您实际上是在跟踪基础中的裂缝。用互斥锁修补它们！信号量！什么都行！唉，你帮不上忙了。就在这个时候，你的大脑，瞥见组合状态爆炸的无限平面，明智地低下头，一天下来，给你留下一种头晕目眩，模糊，紧握的感觉，因为你有胆量要求它解决这一切。

我已经有过很多次这样的感觉，正式的模型是我找到的唯一解决办法。你的大脑不是为了在工作内存中容纳大量的状态空间而构建的，所以甚至不要尝试。让一个模型检查程序在所有这些状态中翻来覆去地寻找错误。在这一点上，我甚至不会接触多线程程序或分布式系统，除非迅速制定出其所需工作的TLA+规范。我只指定系统中所有可能的事件，这些事件如何影响系统状态，以及我一直想要做的事情。我们用非决定论对并发进行建模；在并发系统中，我们不知道线程\(A\)是否会在线程\(B\)之前执行一个步骤，我们可以用一个不确定的状态机来表示这一点，如下所示：

因此，如果线程\(A\)在线程\(B\)之前执行其步骤，您将处于状态\(S_3\)，如果线程\(B\)在线程\(A\)之前执行其步骤，则处于状态\(S_4)。也许\(S_3\)和\(S_4\)甚至是相同的状态，谁知道呢。模型检查器将探索这两种可能的执行顺序，并且在一个设计良好的并发系统中，我们不应该仅仅因为一个。

读者可能想知道这个模型到底是如何并发的，其中的步骤可以同时发生。简单的答案是，您必须确保模型中的所有步骤都是原子的或独立的：要么在现实世界中，您的两个步骤不可能完全同时发生(例如，通过假设使用较低级别的硬件同步原语)；要么不可能执行一个步骤来直接影响与另一个步骤相同的变量(例如，如果在不同的计算机上执行步骤的时间跨度小于它们之间的网络延迟)。如果中的步骤不可能直接影响与另一个步骤相同的变量(例如，如果在不同的计算机上执行这些步骤的时间跨度小于它们之间的网络延迟)。如果。检查所有可能的执行顺序可以准确地建模并发。如果不这样做，您需要进一步细分步骤，这样才能做到这一点。此模型很好地捕获了&；公开了有关并发的所有困难之处。

关于这种模型，我们可以问些什么问题呢？最重要的问题是可达性查询--我们会不会达到坏的状态(两个缓存在一个值上存在分歧、死锁、狗和猫住在一起等等)。这些问题被称为安全属性，如果它们是

如果其中一条线抛硬币，如果它正面做一件事，反面做另一件事怎么办？整个状态空间，被概率事件分成两部分。也许这些状态空间包含更多的硬币抛出，或其他类型的随机性。在这个系统中，您的问题可能从“有可能达到坏状态”变为“达到坏状态的概率有多大”。不幸的是，这些类型的问题不能在上面使用的非确定性模型中得到回答。你不能用不确定性来建模概率，我们必须使用一种新的模型，一种直接处理概率的状态机。

TLA+目前无法处理概率，因此，我们必须使用PRISM这样的专门建模语言来处理概率状态机。让我们看一下概率状态机的标准hello-world示例：1976年的Knuth-姚方法，用于模拟带有一系列掷硬币的公平六面骰子。这确实是一个相当巧妙的问题，我鼓励您在了解它们是如何做到这一点之前仔细考虑一下！任何\(n\)掷硬币序列都会给出一个概率为\(\frac{1}{2^。需要生成发生概率为\(\frac{1}{6}\)的事件。然后，您可能会认为此问题是不可能的，因为你不能将(2^n\)除以\(6\)作为任何\(n\)(这源于素因式分解的唯一性)。实际上，没有办法模拟具有有限数量的掷硬币的六边形骰子。我们必须使用一种算法，该算法不能保证永远终止，尽管几乎不可能不终止。它是这样的：

你可以看到，如果你以某种方式只翻头，或者只翻尾，你永远不会达到接受状态之一(这里标有它们代表的骰子编号)。有一些有趣的方法可以将你连续翻头或翻尾的概率联系起来。例如，在可观察的宇宙中，只有大约\(2^{268}\)个亚原子粒子；如果你成功地连续268次翻头，那就相当于从全宇宙的随机抽签中挑选出正确的亚原子粒子。也许你可以去看看哈勃超深场来思考这个概率。另一种方式是假设你在25-34岁之间，住在美国，你的年全因死亡率约为129/100000。假设死亡人数在一年中均匀分布，这意味着你今天死亡的可能性约为28万分之一。真的不应该担心要抛硬币很多次。

我们创建的这个概率状态机模型被称为离散时间马尔可夫链(DTMC)。在DTMC中，每个转移都有一个关联的概率，对于每个状态，所有流出转移的概率之和必须为1(接受状态可以被认为有一个概率为1的环回)。上述对终止概率的思考总结在长期运行定理中：从长远来看，有限马尔可夫链中的每条路径都以吸收状态结束，哪一个状态(或一组状态)有入口但没有出口。我们可以向DMC提出什么问题？最有趣的问题-我们在这里的原因-是“最终达到某个状态的概率是多少？”长期定理告诉我们，我们有100%的机会最终达到Knuth-姚状态机的接受状态之一。最终进入特定接受状态的概率是多少？它应该是\(\frac{1}{6}\)。是吗?。

让我们试着用基本概率来推断这一点。最终接受状态\(1\)的可能性有多大？好的，您可以通过翻转\(HHT\)到达那里。发生这种情况的概率是\(\frac{1}{2}\cdot\frac{1}{2}\cdot\frac{1}{2}=\frac{1}{8}\)。但是您也可以通过翻转\(HHHHT\)到达那里。发生这种情况的概率是\(\frac{1}{2^5}=\frac{1}{32}\)。我们必须。所以现在我们的概率是\(\frac{1}{8}+\frac{1}{32}=\frac{5}{32}\)。但是我们也可以通过翻转\(HHHHHHT\)，以概率\(\frac{1}{2^7}=\frac{1}{128}\)到达那里。我相信您可以看到这是怎么回事。我们正在处理真正可怕的事情，无穷多个产品的无穷和。如果我们重复。或者(0.16666个点)但是我们怎样才能得到一个很好的封闭形式的解决方案呢？为了避免把我的读者送进一个数学繁重的绞肉机，很少会出现什么问题，我把算法的解释推到了这篇文章的附录中(或者你可以让PRISM计算它，然后再也不想这个了)。现在只知道你可以把dmc写成一个矩阵，这个问题就变成了求解一个简单的线性方程组。Knuth-姚状态机确实准确地模拟了一个公平的六面体。这就是说，你可以把它写成一个矩阵，然后这个问题就可以归结为求解一个简单的线性方程组。Knuth-姚状态机确实准确地模拟了一个公平的六边形。

好的，所以n

让我们考虑一个同时使用概率和不确定性的非常简单的系统。我们有两个线程，A和B，这两个线程是不确定调度的。我们还有两个硬币，一个不公平的硬币，一个正面着地的几率和反面着地的几率分别为\(FRAC{3}{4}\)和\(FRAC{1}{4}\)。我们有两个硬币，一个不公平的硬币\(U\)正面着地的几率和反面着地的几率\(\FRAC{1}{4}\)，无论哪一条线先抓住不公平的硬币(U)并抛出它，第二条线抓住剩余的硬币(F\)并自己抛出。这就是MDP的样子：(F)有50%的几率落在头上或尾部。无论哪条线先抓住不公平的硬币(U\)并将其抛出，第二条线抓住剩余的硬币(F\)并自己抛出它自己。这看起来就像是一个MDP；我们用\(A_x B_y\)标记状态，其中\(x\)和\(y\)是\(\_\)、\(H\)或\(T\)之一，分别表示线程\(A\)和\(B\)的未翻转、头部或尾部：

我们可以看到这是DTMC和非确定性状态机的混合体：如果每个转移只有一个概率为1的分叉，那么MDP就会减少到我们的基本非确定性状态机；如果每个状态只有一个具有一些关联概率的传出转移，那么MDP就会减少到DTMCS。如果每个转移只有一个概率为1的分叉，那么MDP就会减少到我们的基本非确定性状态机；如果每个状态只有一个具有一些关联概率的传出转移，那么MDP就会减少到DTMCS。

Mdpmodule StrangeCoinGame//尚未翻转：0，头部：1，尾部：2 AFlip：[0.。2]初始化0；B翻转：[0..。2]init 0；//先选择其中一条线程，然后翻转不公平的硬币[]AFlip=0&；BFlip=0->；0.75：(AFlip'；=1)+0.25：(AFlip'；=2)；[]AFlip=0&；BFlip=0->；0.75：(BFlip&39；=1)+0.25：(BFlip&39；=2)；//第二个。BFlip=0->；0.5：(BFlip'；=1)+0.5：(BFlip'；=2)；[]AFlip=0&；BFlip！=0->；0.5：(AFlip'；=1)+0.5：(AFlip'；=2)；//接受状态的环回[]AFlip！=0&；BFlip！=0-&>(AFlip'；=B翻转)；结束模块。

现在是大结局！我们可以对这个模型提出什么问题？让我们从一些简单的问题开始，比如“达到状态\(A_H_B_T\)的概率是多少？”我鼓励读者仔细考虑这个问题。如果\(A\)在\(B\)之前，达到状态\(A_H B_T\)的概率是\(\frac{3}{4}\cot\frac{1}{2}=\frac{3}{8。如果\(B\)在\(A\)之前，则达到状态\(A_H B_T\)的概率为\(\frac{1}{4}\cot\frac{1}{2}=\frac{1}{8}\)。请记住，我们不知道/假设任何关于\(A\)在\(B\)之前或反之亦然的概率。我们应该回答“达到状态的概率是多少\(A_H_B_T\)”这个问题吗？我们不能回答这个问题！这是一个无效的问题！关于MDP，我们唯一能问的问题是所有可能的执行顺序中达到某一状态的最大或最小概率的问题。当您考虑如何对MDP进行模型检查时，这就更有意义了，这是通过为每个可能的执行顺序生成DTMC(昂贵！)。然后找出每一个DMC中的可达性概率，并取全局最大或最小值。因此，关于您的系统的声明变成了“它将以最多X%的概率达到坏状态”或“它总是至少有Y%的成功概率”。

实际上，使用MDP来分析Snowflake协议是值得的，因为这篇文章已经很长了，而且我还需要编写上面承诺的附录，而不是只抛出一些链接给您。这是“火箭团队”(几乎可以肯定是Emin Gün Sirer等人，让我们说真的)在IPFS上用化名发布的原始论文；它是由一家名为AVA Labs的公司制作的。以下是纽约州立大学布法罗分校研究分布式系统的教授木拉提·德米尔巴斯对协议的出色总结。

莎拉·杰米·刘易斯(Sarah Jamie Lewis)正在用MDP分析雪花协议，还有一种我们没有涵盖的模型，称为连续时间马尔可夫链(CTMC)-也许CTMC会成为另一篇文章的主题。她正在开发一种有趣的攻击，名为使用拜占庭响应延迟的降雪攻击，详细信息在这里。她的正式模型都可以在这个git Repo中找到。

就我自己而言，我在这里用PRISM将最基本的Snowflake协议(称为Slush)建模为MDP。期待未来关于我所学到的帖子-模型检查MDP非常昂贵，并且模型很难扩展！CTMC显然比MPD更具可伸缩性，尽管我仍然不是很好地理解它们，所以我不知道它们在模型保真度方面会损失什么。

最后，如果你对DTMC背后的数学和算法感兴趣，我再怎么推荐这篇论文也不为过：模型检查遇到概率：RWTH亚琛大学(RWTH Aachen University)教授约斯特-皮特·卡托恩(Joost-Pieter Katoen)的温和介绍。如果没有这篇论文，我永远不会理解这份材料，写下这篇帖子。如果你正在寻找一本包含所有关于形式模型及其检验的已知知识的巨著，

下面将是论文Model Checking Meets Probability：A Gentle Introduction中提出的算法的简化版本。调用我们的Knuth-姚DTMC：

让我们试着计算从起始状态达到接受状态\(2\)的概率。我们使用一个简单的递归算法将其转换为一个容易求解的线性方程组。首先，一些定义：

\(G\)是我们要计算其可达性概率的目标状态集。

我们的目标是找到\(x_s\)，其中\(s\)是开始状态，而\(G\)是只包含接受状态\(2\)的集合\(2\)，但要做到这一点，我们必须在DTMC中找到每个状态的\(X_S)。我们用三个简单的规则来实现：

递归情况：否则，\(x_s=\sum_{t\noin G}P(s，t)\cot x_t+\sum_{u\in G}P(s，u)\)。

递归情况下的等式看起来相当可怕，但不用担心-我们会做到这一点的。对于基本情况，将\(G\)中的所有状态标记为1是微不足道的，并且我们可以从\(G\)中的状态向后运行广度优先搜索，以找到\(G\)可到达的所有状态，并将其他状态标记为0。对于递归情况，最容易考虑将其拆分为两个子情况：对于给定的\(s\)，第一个(sum_{t\noin G})是通过某种中间状态迂回到达G的概率(这是递归的，因为它取决于从这些状态到达G的概率)；第二个(sum_{u\in G})是一步直接到达G的概率，它们加在一起就得到了x_s。

\(x_{s_2}=x_{s_5}=x_{s_6}=x_1=x_3=x_4=x_5=x_6=0\)。

这是一个线性方程组！使用高斯消元法求解\(x_{s_0}\)，我们看到它确实等于\(FRAC{1}{6}\)。上面的文章解释了如何将其机械地转换为一个矩阵，该矩阵可以通过快速调用线性代数库来求解，但我希望您能从概念上了解该算法是如何工作的。