We consider the randomized consensus protocol due to 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
expected polynomial time. The processes proceed through possibly
unboundedly many rounds; at each round, they read the status of the
other processes and attempt to agree. The agreement attempt involves
a distributed random walk (a Markov decision process, i.e. a
combination of nondeterministic and probabilistic choices): when the
processes disagree, they use a shared coin-flipping protocol to
decide their next preferred value. Achieving polynomial expected time
depends in an essential way on ensuring that the probability that all
non-failed processes draw the same value is above an appropriate
bound. For the non-probabilistic part of the algorithm, we use the
proof assistant Cadence SMV to verify validity, agreement and
progress for all N and for all rounds. The shared coin-flipping
protocol is modelled and verified using the probabilistic model
checker PRISM. For a finite number of processes (up to 10) we
automatically calculate the exact (minimum) probability of the
processes drawing the same value, as opposed to a lower bound
established analytically using random walk theory. The
correctness of the full protocol (for the finite configurations
mentioned above) follows from the separately proved properties. This
is the first time a complex randomized distributed algorithm has
been mechanically verified.
