arXiv · math/9409219
Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion
Abstract
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.
Explore related subjects
Keep this discovery
Isaac Saias. 1994-09-19. Proving probabilistic correctness statements: the case of Rabin's algorithm for mutual exclusion. https://arxiv.org/abs/math/9409219
Cite the original work for its findings. Save a collection to share your selection of sources.