Abstract
Byzantine state-machine replication (SMR) ensures the consistency of
replicated state in the presence of malicious replicas and lies at the heart of
the modern blockchain technology. Byzantine SMR protocols often guarantee
safety under all circumstances and liveness only under synchrony. However,
guaranteeing liveness even under this assumption is nontrivial. So far we have
lacked systematic ways of incorporating liveness mechanisms into Byzantine SMR
protocols, which often led to subtle bugs. To close this gap, we introduce a
modular framework to facilitate the design of provably live and efficient
Byzantine SMR protocols. Our framework relies on a view abstraction generated
by a special SMR synchronizer primitive to drive the agreement on command
ordering. We present a simple formal specification of an SMR synchronizer and
its bounded-space implementation under partial synchrony. We also apply our
specification to prove liveness and analyze the latency of three Byzantine SMR
protocols via a uniform methodology. In particular, one of these results yields
what we believe is the first rigorous liveness proof for the algorithmic core
of the seminal PBFT protocol.