Abstract
Partially synchronous Byzantine consensus protocols typically structure their
execution into a sequence of views, each with a designated leader process. The
key to guaranteeing liveness in these protocols is to ensure that all correct
processes eventually overlap in a view with a correct leader for long enough to
reach a decision. We propose a simple view synchronizer abstraction that
encapsulates the corresponding functionality for Byzantine consensus protocols,
thus simplifying their design. We present a formal specification of a view
synchronizer and its implementation under partial synchrony, which runs in
bounded space despite tolerating message loss during asynchronous periods. We
show that our synchronizer specification is strong enough to guarantee liveness
for single-shot versions of several well-known Byzantine consensus protocols,
including HotStuff, Tendermint, PBFT and SBFT. We furthermore give precise
latency bounds for these protocols when using our synchronizer. By factoring
out the functionality of view synchronization we are able to specify and
analyze the protocols in a uniform framework, which allows comparing them and
highlights trade-offs.