Abstract: Reliable distributed systems require replication and
consensus among distributed processes to tolerate process and
communication failures. Understanding and assuring the correctness of
algorithms for replication and consensus have been a significant
challenge.
This work studies the precise specification and runtime checking of
two important consensus algorithms, the revisited classical
Viewstamped Replication and the more recently proposed Derecho.
Precise specifications must fill in missing details and resolve
ambiguities in many places in the published descriptions of these
algorithms. We make important improvements to previous specifications
of these algorithms, especially by careful manual analysis and
increasingly systematic runtime checking. We obtain simpler
specifications, and we discover and fix numerous safety and liveness
bugs and inefficiencies in the previous specifications and several in
pseudocode. These improvements were made possible using DistAlgo, a
language that allows distributed algorithms to be clearly expressed
and directly executed.

Contact events [at] cs.stonybrook.edu for Zoom info.