Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM

Marta Kwiatkowska, Gethin Norman and Roberto Segala

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


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.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Start Conference Manager
Conference Systems