ACM通信
贡献的文章
解构面包房构建分布式状态机
图片来源:Andrij Borys Associates, Shutterstock
在本文中，读者和我将在20世纪70年代的两个并发算法之间旅行，这些算法至今仍在研究。旅程从烘焙算法开始9最后给出了实现分布式状态机的算法。12我希望我们能享受这次航行，也许还能学到一些东西。
烘焙算法确保进程一次执行一个关键代码段。试图执行该代码的进程选择一个它认为比其他类似进程选择的数字要高的数字。编号最低的进程优先，按进程名打破连接。在分布式状态机算法中，每个进程维护一个逻辑时钟，通过让进程在其发送的消息中包含其时钟值来同步时钟。状态机的命令是根据进程发出命令时的时钟值排序的，并按进程名断开连接。
烘焙算法的数字和状态机算法的时钟之间的相似性已经被注意到了，但我不知道它们之间以前没有严格的联系。我们的旅行建立了这种联系，通过一系列算法从烘焙算法到状态机算法，每一个(除了第一个)都来自于前一个算法。
旅途中的第一个算法是烘焙算法的简单概括，主要是允许一个进程以任意顺序读取其他进程的数字。然后，我们通过让每个进程维护其编号的多个副本(每个进程一个副本)来解构这个算法。接下来是分解后的算法的分布式版本，它是通过每个过程的副本获得的我的数字由读取它的程序保存，其中我通过向另一个进程发送消息来写入存储在该进程中的值。然后，我们修改了这个分布式算法，以确保每次执行临界段时数字都会增加。最后，我们通过忘记临界区而只使用数字作为逻辑时钟来得到分布式状态机算法。
我们的算法不仅可以追溯到20世纪70年代，而且它们之间的路径也是当时可以遵循的。此后所做的大量相关工作既没有影响也没有排除该路线的任何部分。在我们旅程的最后，总结部分讨论了相关的工作，以及为什么开始和结束我们的路径的算法仍然被研究到今天。在我们的旅程中，正确性的证明是非正式的，就像在20世纪70年代一样。最后一节讨论了更现代、更严格的证明。
原始烘焙算法
面包店算法解决了Edsger Dijkstra算法引入并求解的互斥问题。3.该问题假设一组进程在执行非关键代码段和关键代码段之间交替执行。进程最终必须退出临界区，但它可能永远留在非临界区。基本要求是，在任何时候，最多只能有一个进程在执行临界部分。互斥问题的解决方案几乎是所有多进程编程的核心。
烘焙算法假设流程由从1到1的数字命名N。图1包含进程号的代码我，几乎和最初的论文一模一样。变量的值数量而且选择是数组索引的进程号，与数量［我),选择［我的初始值为0我。这种关系是按数字对按字典顺序排列的，因此(1,3)(2,2)(2,4);它是对所有整数对的集合的非自反总排序。
图1。过程我最初的烘焙算法。
互斥可以很简单地通过不允许任何进程进入临界段来实现。互斥算法也需要满足一定的进度条件。Dijkstra算法满足的条件是死锁的自由，这意味着如果一个或多个进程试图进入临界区，其中一个必须成功。后期的算法大多满足较强的要求饥饿的自由，这意味着每个试图进入临界区的进程最终都会进入临界区。在讨论互斥之前，我们证明了面包房算法是无饥饿的。但首先，一些术语。
我们说过程是在门口当它执行语句时M。在它完成执行之后米直到它离开临界区，我们都说它是在面包店。当它在代码中的任何其他位置时，我们就说它在在面包店。
我们首先证明该算法是无死锁的。如果不是这样，它最终会达到这样一种状态:每一道工序要么永远在非关键部分，要么永远在面包房里。最终,选择［我= 0我，因此，面包店内的每一道工序都将在结算单上永远等待l3.但这是不可能的，因为等待的过程我的最小值(数量［我]，我)最终会进入临界段。因此，该算法是无死锁的。
烘焙算法确保进程一次执行一个关键代码段。
为了证明该算法是无饥饿的，它可以通过假设一个过程来得到一个矛盾我永远留在面包房里面，在临界区外面。通过死锁自由，其他进程必须不断地进入和离开临界区，因为它们不能在那里停止。
然而，一旦一个过程j是否在面包店外，再进入面包店它必须执行声明米并设置数量［j大于数量［我］．在这一点上，过程j必须永远留在面包房里，因为它会永远循环，如果它到达l3,k＝我。最终,数量［我将小于数量［j]每道工序j在面包店，所以我将进入临界区。这就是证明饥饿是自由的矛盾。
本质上，同样的证明表明，我们从烘焙算法推导出的其他互斥算法也满足饥饿自由。关于饥饿自由，我们再多说一点。我们现在解释为什么面包房算法满足互斥。为了简洁，我们缩写为(数量［我]，我)(数量［j]，j),我j。
这里有一个简单的证明我而且j不能同时出现在关键部位。为我要进入临界段，它必须找到数量［j= 0或我j在执行l3k＝j。同样的,对j要进入临界段，它必须找到数量［我= 0或j我在执行l3k＝我。因为进程号在执行时是非零的l3，这意味着for我而且j都在关键区域，我j而且j我肯定是真的，但这是不可能的。
这个论点是有缺陷的，因为它假设两者都是我而且j当其他进程执行时，是在面包房里面吗l3为合适的值k。假设过程我读数量［j),而j在门口(执行米)，但还没有定型数量［j］．这是可能的j读过数量［我= 0 inl3、进入临界段，并为我然后选择数量［我),使我j进入临界区。
论证中的缺陷可以通过陈述加以纠正l2.自选择［j= 1时j是在门口，过程我执行l3后l2发现,j不在门口;同样的,j执行l3发现我不是在门口。如果，在这两种情况下，两个过程都在烘焙时l2被执行，那么这个朴素的论点是正确的。如果其中一个j它不是在面包店里面，一定是在面包店外面。自我当时在面包店里，它现在的价值是数量［我),过程j必须有选择数量［j的当前值数量［我),使我j真实的。因此,j不能离开l3循环k＝我进入临界区我还在面包店里。因此,我而且j不能两个都在临界区。
观察到的选择变量只用于确保，当进程我执行l3k＝j，有那么一瞬间我已经在面包店里了j不在门口。这在以后会很重要。
面包店算法最令人惊讶的特性是，它不需要读取或写入内存寄存器作为一个原子操作。仔细研究互斥的证明就会发现这是必须的数量［我),选择［我都是后来所谓的安全寄存器，13只确保读操作(不重叠写操作)获得当前寄存器值。如果读操作与写操作重叠，则可以获得寄存器可能包含的任何值。
用原子操作来描述安全寄存器是最方便的。我们表示写一个值v将寄存器作为两个动作:第一个动作将其值设置为一个特殊的常量¿，第二个动作将其值设置为v。我们将读取表示为单个原子动作，如果寄存器的值不等于¿，则该操作将获得该寄存器的值。读的数量［我=¿时可返回任意自然数，并可读取选择［我=¿时可以返回0或1。
原算法的推广
烘焙算法发表时，两个推广是显而易见的。首先，在声明中米，则不需要设置数量［我]到1 +最大(……)。它可以设置为比最大值大的任何数。它也可以设置为最大值，如果使(数量［j]，j)(数量［我]，我)为所有j，但我们就不做泛化了。我们重写语句米使用:>表示“被赋值大于。”
第二个明显的概括是这个陈述l2,l3为不同的值k不需要按指定的顺序执行为声明。由于互斥性的证明考虑的是每一对进程本身，唯一的要求是，对于任何值k、语句l2必须执行之前l3.对于不同的值k，这些语句可以由不同的子流程并发执行。而且，也没有理由执行它们k＝我因为他们的如果测试总是等于假。
这两种概括在其他地方也出现过。5，10还有另一种不太明显的推广似乎是新的:赋值为0数量［我在进程离开临界区后，不需要在进程进入非临界区之前完成。事实上，如果进程离开非临界区，再次进入临界区，那么这种分配甚至不需要完成。只要任务在之前完成或取消(留下与其相等的注册表)数量［我]在语句中被赋新值米，它只是在其他进程看来就像进程一样我仍然在临界区，或者在临界区之后立即执行赋值语句。因此，仍然满足互斥。为了保持饥饿的自由，如果我永远留在非临界区。在伪代码中似乎没有简单的方法来描述这些设置要求数量［我]到0。我们只需添加神秘的关键字异步并参考这个讨论的解释。
提出了一种广义算法图2．进程显式声明;外过程语句表示有从1到1编号的进程N并显示了进程号的代码我。变量用它们的初始值声明。内过程语句声明该过程我有N- 1子流程j从1到数字N，没有编号我，并给出子进程的代码j。该语句通过派生子进程来执行，并在所有子进程都终止时继续执行下一个语句(关键部分)。有害的,转到S已经被消除了。外环被描述为而声明。的循环l2,l3 .已被描述与等待语句，每个语句都重复求其谓词的值，并在为真时终止。语句中的:>米和异步上述声明已作了解释。
图2。对原有烘焙算法的推广。
解构烘焙算法
我们假设数量［我),选择［我是安全的寄存器，只由我并被很多读者阅读。通过为每个读卡器在单独的寄存器中保存寄存器值的副本，这种寄存器很容易实现，安全寄存器只有一个读卡器。
我们通过实现安全寄存器来解构广义烘焙算法选择［我),数量［我]与单阅读器寄存器localCh［j] [我),localNum［j] [我),为每个j≠我。注意这个有违直觉的下标顺序localCh［j] [我),localNum［j] [我的副本选择［我),数量［我通过过程读取j。
解构算法的伪代码在图3．的读取选择［j),数量［j通过过程我在广义算法中，用读取数代替localCh［我］ ［j),localNum［我] [j］．的变量数量［我]现在只被进程读取我，我们已经排除了选择［我因为过程我不读。特别表示法在语句中使用米表明数量［我]被设置为大于all的值localNum［j] [我］．
图3。解构烘焙算法。
我们已经显式地指出了表示写入值的两个原子操作v到安全登记处localNum［j] [我，首先将其值设置为¿，然后设置为v。我们没有费心为写入操作做这些localCh［j] [我］．的localCh［j] [我),localNum［j] [我写操作由进程的子进程执行我，除了N对所有寄存器分别写1个¿localNum［j] [我)由赋值语句表示
主要过程我。(这将为我们的下一个烘焙算法版本提供更多方便。)设置数量［我]到0后我退出临界区，所有寄存器localNum［j] [我]被主进程设置为¿，每一个都被单独的进程设置为0。我们要求设置localNum［j] [我到0时已经完成或中止localNum［j] [我]设置为数量［我]按subprocess (我，j)．同样，伪代码中没有显式地显示这一点。
通过对原算法的证明进行简单的修改，可以得到解构算法的正确性证明。对于原始算法，我们定义了process我在门口执行语句米，最后将值赋给数量［我］．自数量［我]已被登记册所取代localNum［j] [我),过程我现在每个进程都有一个单独的入口j。我们说我就在门口吗j从何时开始执行语句米直到它的子流程j分配数量［我)localNum［j] [我］．我们说我是在面包店里面吗j从它离开门口开始j直到它退出临界区。的定义我面包店外面和以前一样。
为了将原始烘焙算法的正确性证明转化为解构算法的正确性证明，我们替换了我或j是在门口或在面包店里面的陈述它是在那里，与其他过程。改进后的证明证明了语句的作用l2是保证一定的时间间隔我走进面包房j和执行l3j、过程j不是在门口吗我。
分布式烘焙算法
我们现在使用分布式算法实现了解构烘焙算法。每个主要流程我在一个单独的节点上执行，我们称之为node我在通过消息传递进行通信的进程网络中。的变量localNum［j] [我，这就是过程j的复制数量［我，保存在节点上j。它是由过程设定的我价值v通过发送信息v来j。的设置localNum［j] [我在解构的烘焙算法中，¿是通过发送该信息的动作来实现的localNum［j] [我]设置为v通过过程j当它接收到消息时。因此，我们通过有过程来实现解构的算法j的前一个值localNum［j] [我]念一念时localNum［j] [我害怕]=。由于解构后的算法允许这样的读取获得任何值，所以这是一个正确的实现。
现在，我们假设这个过程我能写出值吗localCh［j] [我在原子上受到一个神奇的远距离作用。我们稍后会移除这个魔法。
我们假设消息从进程发送我任何其他过程j按发送的顺序接收。我们表示传输中的消息我来j通过先进先出(FIFO)队列问［我] [j］．我们将∅设为空队列，并对队列定义以下操作问：
- 附加（问，瓦尔)添加元素瓦尔直到最后Q。
- 头（问)是开始时的值Q。
- 斩首（问)删除开头的元素Q。
- 头（问)和斩首(问)是未定义的问=∅。
完整的算法已经出炉图4．阴影突出使用localCh他的魔法属性需要处理。还有主要的过程我，有多个并行执行的进程(我，j在节点我,对于每一个j≠我。过程(我，j)接收所发送的讯息并作出反应我通过j。
图4。分布式烘焙算法，具有魔力。
的主要过程我直接从解构算法中获得分布式算法的部分，方法是替换¿对每个算法的分配localNum［j] [我，并将消息发送给j，除了两个变化。首先是这个声明米和下面发送消息到其他进程(表示为追加数量［我]发送到所有消息队列问［我] [j)都被做成了单个原子动作。之所以可以这样做，是因为可以查看每个消息队列的结束问［我] [j，消息被追加到上面，成为进程的一部分我本地状态。一个民间定理4也就是说，对于多进程算法的推理，我们可以将任意数量只访问进程局部状态的操作组合成单个原子操作。这个民间定理在很多结果中都被形式化了从立顿开始，15也许最直接适用的就是兰波特。14在我们的算法中，让这个操作看起来是原子的，只需要阻止节点上的其他进程我在执行操作时对任何传入消息执行操作。
解构算法的另一个重要变化是异步声明已经消失了。的设置localNum［j] [我]是由接收发送的消息执行的我来j。FIFO消息传递确保在其后续设置为非零值之前将其设置为0。而且,由于localNum［j] [我]现在按进程(j，我)接收到消息后，在子进程中对其进行赋值j的我被移除。
解构后算法的正确性还取决于对localNum［j] [我]在处理之前执行我集localCh［j] [我)为0。自从分配给localNum［j] [我]现在在节点上执行j，这两个操作的顺序不再由代码隐含。要维护这种顺序，请使用子流程j的我必须学会这个过程(j，我)设置localNum［j] [我)数量［我才会凝固localCh［j] [我)为0。这是通过拥有(j，我)发送消息给我有一些价值消那不是一个自然数。过程(j，我)设置的值localNum［j] [我]，并发送消消息我作为单个原子动作。当过程(我，j在节点我接收消消息,它集ackRcvd［我] [j到1通知子进程j的过程我这一消已经到来。的设置localNum［j] [我)数量［我]在解构算法中被语句代替l0等待ackRcvd［我] [j等于1。
主进程的其余代码我与解构算法的对应过程相同，除了之后我离开临界区，即所有寄存器的异步设置localNum［j] [我到0将被替换为向所有进程发送消息0j,ackRcvd［我] [j]将全部重置为0j。
异步执行的进程(我，j)接收由发送的消息j通过问［j] [我］．对于一个消消息,它集ackRcvd［我] [j) 1;值为的消息数量［j它集localNum［我] [j，如果该值非零，则发送一个消来j。
剩下的一个问题是寄存器不可思议的原子读写localCh［我] [j］．该寄存器的值只在语句中使用l2.的目的l2是保证，在执行之前l3、曾经有一段时间T当我是在面包房吗j而且j不是在门口吗我。我们现在展示这个表述l2是不必要的，因为执行l0确保了这样一个时间的存在T。
语句的执行米通过j和发送数量［j在邮件中我是单个原子操作的一部分，并且j就进面包店吧我当在节点上接收到消息时我。因此,j就在门口吗我当消息中包含一个非零整数时问［j] [我］．我们称这个消息为a门口消息。过程我就进面包店吧j当它的消息包含数量［我]在节点上接收j，追加到的动作问［j] [我]消那l0号等待到达。如果没有门口信息问［j] [我]此时，则立即执行该动作后即为时间T我们需要证明谁的存在，因为它发生在收到之前消那l0在等待。如果有一个门口信息问［j] [我]，然后是所需的时间T是在节点接收到消息之后吗我。由于FIFO消息的传递，那时候也是在收到之前消那l0在等待。在这两种情况下，都是执行l0表示有时间T后我就这样走进了面包店j当j不是在门口吗我。因此,声明l2是多余的。
因为l2是唯一一个localCh［我] [j]是读出来的，我们可以消除localCh以及所有设置它的表述。删除中所有灰色的语句图4给了我们分布式烘焙算法，没有魔法。
第一篇致力于分布式互斥的论文显然是Ricart和Agrawala的。19他们的算法可以看作是我们算法的优化和简化。延迟发送消消息的一种方式，使进程可以在接收到临界区时进入临界区消从每一个其他进程，所以它不必跟踪其他进程的数字。因此，在退出临界区时发送的数字0消息可以被消除，从而产生一个消息更少的算法。虽然Ricart-Agrawala算法比我们的算法更好，但它并不直接在我们行进的路径上。
分布式状态机
在分布式状态机中，12在网络中不同的节点上有一组进程，每个进程都想执行状态机命令。进程必须对所有命令的执行顺序达成一致。为了执行命令，进程必须知道前面命令的整个顺序。
分布式互斥算法可以通过让进程在临界区执行单个命令来实现分布式状态机。进程进入临界区的顺序决定了命令的顺序。很容易设计这样一种协议:在临界区中有一个进程将其当前命令发送给所有其他进程，这些进程将其命令排序在所有前面的命令之后。从这一思想出发，结合分布式烘焙算法，得到分布式状态机算法12通过消除临界区。
烘焙算法是基于这样的思想:如果两个进程试图同时进入临界区，那么该进程我的较小值(数量［我]，我)进入。现在，无论两个进程何时进入临界区，我们都使之为真。定义焙烤算法的一个版本数量-ordered，如果它满足这个条件我进入临界区数量［我] =n我和过程j随后进入临界段数量［j] =nj,然后(n我，我)(n我，j)．我们现在让分发的面包店号码订购。我们可以这样做，因为我们将烘焙算法一般化数量［我的最大值的任意数数量［j，而不仅仅是读到第二大的数字。
我们在分布式烘焙算法中加入了一个变量maxNum,在那里maxNum［我] [j是最大的值localNum［我] [j等同，为j≠我。我们让maxNum［我] [我是最大的值数量［我]等于。然后我们对算法做了两个修改。首先，我们替换语句米在声明中图5．
图5。表述M的一个新版本。
第二，过程中(我,我),如果localNum［我] [j，则赋给一个非零值maxNum［我] [j]被赋予相同的值。消息的FIFO排序确保了的新值maxNum［我] [j]将大于其之前的值。很明显,localNum［我] [j]总是等于maxNum［我] [j)或0。的价值数量［我因此，语句允许这样选择米分布式算法的，所以这是该算法的正确实现。我们现在展示了它是按数字顺序排列的。
假设我进入临界区数量［我] =n我而且j随后进入临界段数量［j] =nj．很明显…n我，我)(nj，j)如果我＝j，所以我们可以假设我≠j。分解算法的互斥性证明表明:(i) (n我，我)(nj，j)或(ii)j选择nj读取值后localNum［我] [j]之后写的我将其设置为n我．在我们改进的分布式算法中，j读取maxNum［j] [我不localNum［我] [j)设置数量［j),而maxNum［j] [我]从未减少。因此,(n我，我)(n我，j)在case (ii)中也为真，因此算法是按数字顺序排列的。
由于算法是按数字顺序排列的，因此我们不需要临界区来实现分布式状态机。我们可以按值(数量［我]，我)就会有时间我进入临界区执行命令。过程我是否可以在包含值的消息中发送正在执行的命令数量［我]发送给其他进程。事实上，我们不需要数量［我]。当我们发送信息时，数量［我的值与maxNum［我] [我］．我们可以排除主要过程中的一切我除了原子语句包含语句米，现在可以写成图6,在那里Cmd是过程我当前命令。
图6。语句M的更新版本。
还有一个问题。过程我保存包含它发送和接收的命令的消息，收集一组三元组(v，j，Cmd)表示该过程j发布了一个命令Cmd与数量［j[比喻有价值的v。它知道这些命令是由(v，j)．但是，要在(v，j，Cmd)，它必须知道它已经收到了所有的命令(w，k，Dmd)和(w，k)(v，j)．过程我知道这一点，对于每个过程k，它已收到所有命令(w，k，Dmd),w≤maxNum［我］ ［k］．然而,假设我没有收到任何命令吗k。怎么能我确保k没有在消息中发送命令我还没有收到吗?答案是使用分布式烘焙算法消消息。这是如何。
为了方便，我们让过程我保持maxNum［我] [我]总是等于值的最大值maxNum［我] [j)(包括j＝我)．它是通过增加来实现的maxNum［我] [我，如果需要，当接收值为的消息时maxNum［我] [j从另一个过程j。收到消息后(v，Cmd)过程j、过程我集maxNum［我] [j)v(可能增加maxNum［我] [我)，并返回到j消息(maxNum［我] [我]，消)．当收到消息时，j集maxNum［j] [我因此,(增加maxNum［j] [j如果有必要的话)。当我已收到所有消它发出的命令的消息maxNum［我] [我) =v，它的所有值maxNum［我] [j]将≥v,所以过程我知道它已经收到了当前命令之前的所有命令。因此，它可以以适当的顺序执行所有这些命令，然后执行当前的命令。
这几乎与分布式状态机算法相同，12在哪里maxNum［我] [我被称为process。我的时钟。(这里给出的算法草图还不够详细，没有提到其他寄存器maxNum［我] [j]。)唯一的区别是，当过程我接收来自j使用新值v的maxNum［我] [j，算法要求maxNum［我] [我设置为>v,而≥v就足够了。的值，算法保持正确maxNum［我] [我]会在任何时候以任何数量增加。因此,注册maxNum［我] [我也可能是用于其他目的的逻辑时钟。
我们已经描述了分布式状态机算法的所有部分，但还没有将它们组合成伪代码。“精确的算法很简单，我们就懒得描述了。”12
古代史和近代史
除了是这篇文章的作者，我还是我们旅程的开始和结束算法的作者。烘焙算法是仅使用对共享内存的读写操作实现互斥的数百种算法之一。22其中一些改进了烘焙算法，最显著的改进是选定数字的边界。6，21但所有的进步似乎都给我们的道路增加了障碍，除了一个:摩西和帕廷17通过允许工艺对烘焙算法进行优化我停止等待进程j在声明中l3，如果读取两个不同的值数量［j］．但是，它与我们的路径无关，因为它优化了分布式烘焙算法中无法出现的情况。
基于读写操作的互斥算法已经几十年没有实际应用了，因为现代计算机提供了特殊的指令来更有效地实现互斥。现在，它们主要作为并发编程练习来研究。烘焙算法之所以有趣，是因为它是第一个不假设低级互斥的算法，低级互斥是由共享内存的原子读写隐含的。分布式状态机算法很有趣，因为它保留了因果关系。但它也不如它解决的问题重要。
我在状态机论文中最重要的贡献是观察到计算机网络中任何想要的合作形式都可以通过实现分布式状态机来获得。很明显，下一步是使实现容错。解决这个问题的工作范围太广，不便在此讨论。容错状态机算法已经成为实现可靠分布式系统的标准构建块。20.
烘焙算法的创建和状态机算法之间没有直接联系。面包店算法的灵感来自我长大的附近的一家面包店。一台机器向顾客分发数字，这些数字决定了顾客得到服务的顺序。状态机算法的灵感来自于Paul Johnson和Robert Thomas的一个算法。7他们使用关系和进程标识符来打破僵局，但我不知道这是否受到了烘焙算法的启发。
我们遵循的两个算法之间的路径不是我最初选择的。这段旅程开始于我为我写的笔记寻找分布式算法的一个例子。Stephan Merz提出了我用来说明状态机算法的互斥算法。我发现它太复杂了，所以我简化了它。(我不记得Ricart-Agrawala算法，直到后来才被裁判提醒)。在删除了那个特定状态机不需要的东西之后，我找到了分布式烘焙算法。这显然与最初的烘焙算法有关，但目前还不清楚具体是怎么回事。
我想让分布式算法成为烘焙算法的一个实现。我首先概括了让每个流程的子流程与其他流程独立交互的概念;这就是我多年来一直在描述的烘焙算法。延迟设置数量［我]到0是必需的，因为完成它的分布式算法的消息可能会被任意延迟。我花了一段时间才意识到我应该解构多阅读器寄存器数量［我]转化为多个单读器寄存器，并说明了原始烘焙算法和分布式算法都实现了解构算法。
从分布式烘焙算法返回到分布式状态机算法的路径简单。它可能已经帮助了我之前使用的想法，修改面包房算法，使价值数量［我继续增加。矛盾的是，这样做是为了防止这些值变得太大。10
用两类性质来表示并行算法的正确性:安全属性，如互斥，断言算法可以做什么，以及活性属性，如饥饿自由，断言算法必须做什么。1安全性能取决于算法可以执行的动作;活性属性也取决于算法必须执行哪些动作的假设，通常是隐含的。
我在这里使用的这种非正式的行为推理是出了名的不可靠。我相信，对安全特性最好的严格证明通常是基于不变量——在每一种可能执行的每一种状态都成立的谓词。2面包店算法满足互斥的不变性证明经常被用来说明形式主义或工具。5，11本文的扩展版本中提供了分解后的烘焙算法的非正式证明草图，可以在Web上找到。8可以使用时间逻辑来编写优雅的、严格的进度属性证明。18
严格的证明比非正式的证明要长，可能会吓到不习惯它们的读者。除非我相信我想证明的是真的，否则我几乎不会写。对于我们算法的正确性，这种信念是基于我所展示的非正式证明中所包含的推理——与我发现烘焙和分布式状态机算法时所使用的推理相同。
我对这两种算法有足够的了解，对烘焙算法的非分布式版本以及从分布式烘焙算法推导出的状态机算法的正确性有足够的信心。模型检查使我确信分布式烘焙算法的正确性，并确认了我的非正式不变性证明给我的信任，即解构后的算法满足互斥。
最近，Stephan Merz为我的非正式不变性证明写了一个正式的机器检查版本。他还写了一个机器检查证明，分布式烘焙算法的动作在适当的数据细化下实现了解构烘焙算法的动作。这两个证明证明了解构算法满足互斥。校样可以在网上找到。16
数字观看作者对这部作品的独家讨论通信视频。//www.eqigeno.com/videos/deconstructing-the-bakery
参考文献
1.Alpern, B.和Schneider F.定义活力。信息处理信件21， 4(1985年10月)，181-185。
2.证明并行程序的断言。计算机与系统科学， 1(1975年2月)，110-135。
3.并行编程控制中一个问题的解决。Commun。ACM 8， 9(1965年9月)，569
4.关于民间定理。Commun。ACM 23， 7(1980年7月)，379-389。
5.兰波特烘焙算法的力学验证。计算机程序设计学， 9(2013)， 1622-1638。
6.Jayanti, P.， Tan, K.， Friedland, G.和Katz, A. Bounding Lamport的烘焙算法。在L. Pacholski和P. Ruzicka的编辑中，SOFSEM 2001: 28th信息学理论与实践的当前趋势会议2234，计算机科学课堂讲稿，施普林格(2001)，261-270。
7.Johnson, P.和Thomas, R.重复数据库的维护。征求意见rfc# 677，第31507号NIC，阿帕网网络工作组，(1975年1月)。
8.《解构面包房构建分布式状态机》的在线补充材料，http://lamport.azurewebsites.net/pubs/bakery/deconstruction.html．
9.Dijkstra并行编程问题的一个新解。Commun。ACM 17， 8(1974年8月)，453-455。
10.同时阅读和写作。Commun。ACM 20， 11(1977年11月)，806-811。
11.证明多进程程序的正确性。软件工程学报， 2(1977年3月)，125-143。
12.时间、时钟和分布式系统中事件的排序。Commun。ACM 21， 7(1978年7月)，558-565。
13.关于进程间通信。分布式计算1(1986), 77 - 101。
14.分布式算法中原子性的L. A定理。分布式计算4， 2(1990)， 59-68。
15.约简:证明并行程序性质的一种方法。Commun。ACM 18， 12(1975年12月)，717-721。
16.Merz, S. Online TLA+规范和证明“解构面包圈构建分布式状态机”。https://members.loria.fr/SMerz/papers/distributed-bakery.html．
17.Moses, Y.和Patkin, K.相互排斥是优先考虑的问题。计算机理论(2018), 46-60。
18.Pnueli, a，程序的时间逻辑。在十八届立法会会议记录th计算机科学基础年会， IEEE(1977年11月)，46-57。
19.Ricart, G.和Agrawala, A.计算机网络中互斥的一个最优算法。Commun。ACM 24， 1(1981)， 9-17。
20.使用状态机方法实现容错服务:教程。ACM计算调查22， 4(1990年12月)，299-319。
21.黑白烘焙算法和相关的有界空间、自适应、局部自旋和FIFO算法。R. Guerraoui，(编辑)，分布式计算学报，18th实习生。文件3274，计算机科学课堂讲稿，施普林格(2004年10月4日)，56-70。
本作品授权于数字图书馆是由计算机协会出版的。版权所有©2022 ACM股份有限公司
没有发现记录