Monday, December 07, 2009
11:00 AM
Computer Studies Bldg. 209
Robbert Van Renesse
Cornell University
Refining the way to Consensus
Consensus protocols, typically a dozen or so lines of high-level pseudo-code, are notoriously difficult to comprehend. For this reason, they are usually accompanied by correctness proofs, but few people are prepared to slog through those details. And although the proofs should constitute a way to understand the protocols, they are rarely illuminating and do not distinguish between important insights and the myriad of low-level technical details that also need to be right. So people are more likely to do operational reasoning, where they look at various hand-simulated sample executions and attempt to understand how and why the protocols work based on those. Moreover, little effort is made to relate the different protocols even though all seem to be constructed from a relatively small number of underlying mechanisms, such as rounds of messaging and quorum intersection. We present a different approach to understanding consensus protocols. Specifically, we present a sequence of specifications of consensus with gradually increasing lower-level detail. Each such refinement step involves an important insight about how and why consensus protocols work.

Bio: Robbert Van Renesse is a Principal Research Scientist at the Department of Computer Science. He received his Ph.D. from the Vrije Universiteit in Amsterdam in 1989 where he developed the Amoeba Distributed Operating System. Subsequently he worked on the Plan 9 operating system at AT&T Bell Laboratories. Since joining Cornell in 1991 he has worked on fault-tolerant distributed systems. Robbert van Renesse is a co-founder of D.A.G. Labs, which was acquired by FAST Search & Transfer, which was acquired by Microsoft, and a co-founder of Reliable Network Solutions, Inc.

Refreshments provided at 10:45