**Author:** M. Kwiatkowska,
G. Norman,
R. Segala
**Appears:** *Proceedings of the 13th
International Conference on Computer Aided Verification (CAV)
2001*, Paris, France, LNCS 2102, pages 194-206, July 2001

**Abstract:** We consider the randomized consensus protocol of
Aspnes and Herlihy for achieving agreement among N asynchronous
processes that communicate via read/write shared registers. The
algorithm guarantees termination in the presence of stopping failures
within polynomial expected time. Processes proceed through possibly
unboundedly many rounds; at each round, they read the status of all
other processes and attempt to agree. Each attempt involves a
distributed random walk: when processes disagree, a shared
coin-flipping protocol is used to decide their next preferred
value. Achieveng polynomial expected time depends on the probability
that all processes draw the same value being above an appropriate
bound. For the non-probabilistic part of the algorithm, we use the
proof assistant Cadence SMV to prove the validity and agreement for
all N and for all rounds. The coin-flipping protocol is verified using
the probabilistic model checker PRISM. For a finite number of
processes (up to 10) we automatically calculate the minimum
probability of the processes drawing the same value. The correctness
of the full protocol follows from the separately proved
properties. This is the first time a complex randomized distributed
algorithm has been mechanically verified.

**Download:**

Download the
paper from the publisher.

Download an author-created copy
of the paper
(© Springer-Verlag).