Computer Studies Bldg. 209
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