Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion
<|reference_start|>Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion: 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.<|reference_end|>
@article{saias1994proving,
    title={Proving probabilistic correctness statements: the case of Rabin's
  algorithm for mutual exclusion},
    author={Isaac Saias},
    journal={arXiv preprint arXiv:math/9409219},
    year={1994},
    number={LACES 68Q-94-14},
    archivePrefix={arXiv},
    eprint={math/9409219},
    primaryClass={math.CO cs.CC}
}