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. (Joint work with Gethin Norman and Roberto Segala.)

More information can be found at www.cs.bham.ac.uk/~dxp/prism/consensus/.

Monday, April 23 at 4pm in DH 3092

A reception will be held BEFORE the talk at 3:30 in DH 3092.