The correctness proof of Ben-Or's randomized consensus algorithm
The correctness proof of Ben-Or's randomized consensus algorithm
复制标题
DOI：
10.1007/s00446-012-0162-z
复制
发表时间：
2012-10-01
影响因子：
1.3
通讯作者：
Toueg, Sam
中科院分区：
文献类型：
--
作者：
Aguilera, Marcos K.;Toueg, Sam
在1983年发表的一篇开创性论文中，Ben-Or提出了第一个解决异步消息传递系统中共识的随机算法，其中进程可能会因崩溃而失败。虽然后来提出了更有效的随机算法，但Ben-Or算法仍然是最简单和最优雅的算法。由于这个原因，它经常在分布式计算课程中教授，并出现在几本教科书中。即使Ben-Or的算法是众所周知的，它是非常简单的，令人惊讶的证明算法的正确性还没有出现：以前发表的证明做了一些简化的说明--具体地说，它们或者假设f < n/3，（n是进程的总数，f是可能崩溃的进程的最大数量）或者对手很弱，也就是说，它不能看到进程状态或消息的内容。在本文中，我们提出了一个正确的证明Ben-Or的随机共识算法的情况下，f < n/2进程崩溃和对手是强的（即，它可以看到处理状态和消息内容，并相应地调度处理步骤和消息接收）。据我们所知，这是这个经典算法的第一个完整证明。我们还证明了一个违反直觉的问题，可能会发生，如果一个人使用众所周知的抽象的“全球硬币”模块化和加速随机共识算法，如本-奥尔的算法。具体来说，我们表明，与普遍的看法相反，使用全球硬币有时可能是有害的，而不是有益的：而不是加速Ben-Or的算法，在这个算法中使用全球硬币实际上可能会防止终止。
In a ground-breaking paper that appeared in 1983, Ben-Or presented the first randomized algorithm to solve consensus in an asynchronous message-passing system where processes can fail by crashing. Although more efficient randomized algorithms were subsequently proposed, Ben-Or's algorithm is still the simplest and most elegant one. For this reason, it is often taught in distributed computing courses and it appears in several textbooks. Even though Ben-Or's algorithm is widely known and it is very simple, surprisingly a proof of correctness of the algorithm has not yet appeared: previously published proofs make some simplifying assumptions-specifically, they either assume that f < n/3 (n is the total number of processes and f is maximum number of processes that may crash) or that the adversary is weak, that is, it cannot see the process states or the content of the messages. In this paper, we present a correctness proof for Ben-Or's randomized consensus algorithm for the case that f < n/2 process crashes and the adversary is strong (i.e., it can see the process states and message contents, and schedule the process steps and message receipts accordingly). To the best of our knowledge, this is the first full proof of this classical algorithm. We also demonstrate a counterintuitive problem that may occur if one uses the well-known abstraction of a "global coin" to modularize and speed up randomized consensus algorithms, such as Ben-Or's algorithm. Specifically, we show that contrary to common belief, the use of a global coin can sometimes be deleterious rather than beneficial: instead of speeding up Ben-Or's algorithm, the use of a global coin in this algorithm may actually prevent termination.