证明概率正确性陈述：Rabin算法的互斥情况
Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion
摘要：
大多数随机分布算法的正确性都是用这样一种形式的陈述来表达的：“执行的某些谓词具有很高的概率，而不管动作的调度顺序如何。在本文中，我们提出了一个一般的方法来证明这种随机算法的正确性声明。具体来说，我们将展示如何证明这样的声明的一系列改进，终止在一个独立的时间表的声明。为了证明这种类型的分析所涉及的问题的微妙之处，我们专注于拉宾的互斥随机分布算法[拉宾82]。令人惊讶的是，事实证明，该算法不保持在一定的时间表下的问题的要求之一。特别是，我们给出了一个时间表下，一组进程可以遭受锁定任意长的时间。
英文摘要：
The correctness of most randomized distributed algorithms is expressed by a statement of the form ``some predicate of the executions holds with high probability, regardless of the order in which actions are scheduled''. In this paper, we present a general methodology to prove correctness statements of such randomized algorithms. Specifically, we show how to prove such statements by a series of refinements, which terminate in a statement independent of the schedule. To demonstrate the subtlety of the issues involved in this type of analysis, we focus on Rabin's randomized distributed algorithm for mutual exclusion [Rabin 82]. Surprisingly, it turns out that the algorithm does not maintain one of the requirements of the problem under a certain schedule. In particular, we give a schedule under which a set of processes can suffer lockout for arbitrary long periods.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
