# Liveness and Latency of Byzantine State-Machine Replication

Manuel Bravo  IMDEA Software InstituteSpain ,  Gregory Chockler  University of
SurreyUK and  Alexey Gotsman  IMDEA Software InstituteSpain

###### 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.

##  1\. Introduction

Byzantine state-machine replication (SMR) (smr, ) ensures the consistency of
replicated state even when some of the replicas are malicious. It lies at the
heart of the modern blockchain technology and is closely related to the
classical Byzantine consensus problem. Unfortunately, no deterministic
protocol can guarantee both safety and liveness of Byzantine SMR when the
network is asynchronous (flp, ). A common way to circumvent this while
maintaining determinism is to guarantee safety under all circumstances and
liveness only under synchrony. This is formalized by the partial synchrony
model (dls, ; CT96, ), which stipulates that after some unknown Global
Stabilization Time (GST) the system becomes synchronous, with message delays
bounded by an unknown constant $\delta$ and process clocks tracking real time.
Before ${\sf GST}$, however, messages can be lost or delayed, and clocks at
different processes can drift apart.

Historically, researchers have paid more attention to safety of Byzantine SMR
protocols than their liveness. For example, while the seminal PBFT protocol
came with a detailed safety proof (castro-thesis, , §A), the nontrivial
mechanisms ensuring its liveness were only given a brief informal
justification (castro-tocs, , §4.5.1), which did not cover their most critical
properties. However, ensuring liveness under partial synchrony is far from
trivial, as illustrated by the many liveness bugs found in existing protocols
(wild, ; casper-bug, ; alysson-reads, ; tendermint-opodis, ; zyzzyva-bug, ).
In particular, classical failure and leader detectors (CT96, ; petr-survey, )
are of little help: while they have been widely used under benign failures
(R00, ; MR99, ; GR04, ), their implementations under Byzantine failures are
either impractical (kihlstrom, ) or detect only restricted failure types
(MR97, ; muteness, ; modular-smr, ; HK09, ). As an alternative, a textbook by
Cachin et al. (cachin-book, ) proposed a leader detector-like abstraction that
accepts hints from the application to identify potentially faulty processes.
However, as we explain in §8 and §F, this abstraction is impossible to
implement, and in fact, the consensus algorithm constructed using it in
(cachin-book, ) also suffers from a liveness bug.

Recent work on ensuring liveness has departed from failure detectors and
instead revisited the approach of the original DLS paper (dls, ). This
exploits the common structure of Byzantine consensus and SMR protocols under
partial synchrony: such protocols usually divide their execution into views,
each with a designated leader process that coordinates the protocol execution.
If the leader is faulty, the processes switch to another view with a different
leader. To ensure liveness, an SMR protocol needs to spend sufficient time in
views that are entered by all correct processes and where the leader correctly
follows the protocol. The challenge of achieving such view synchronization is
that, before ${\sf GST}$, clocks can diverge and messages that could be used
to synchronize processes can get lost or delayed; even after ${\sf GST}$,
Byzantine processes may try to disrupt attempts to bring everybody into the
same view. View synchronizers (NK20, ; bftlive, ; hotstuff, ; lumiere, )
encapsulate mechanisms for dealing with this challenge, allowing them to be
reused across protocols.

View synchronizers have been mostly explored in the context of (single-shot)
Byzantine consensus. In this case a synchronizer can just switch processes
through an infinite series of views with fixed or growing duration, so that
eventually there is a view with a correct leader that is long enough to reach
a decision (NK20, ; bftlive, ). However, using such a synchronizer for SMR
results in suboptimal solutions. For example, one approach is to use the
classical SMR construction where each command is decided using a separate
black-box consensus instance (smr, ), implemented using a view synchronizer.
However, this would force the processes in every instance to iterate over the
same sequence of potentially bad views until the one with a correct leader and
sufficiently long duration could be reached. As we discuss in §8, other
approaches for implementing SMR based on this type of synchronizers also
suffer from drawbacks.

To minimize the overheads of view synchronization, instead of automatically
switching processes through views based on a fixed schedule, implementations
such as PBFT allow processes to stay in the same view for as long as they are
happy with its performance. The processes can then reuse a single view to
decide multiple commands, usually with the same leader. To be useful for such
SMR protocols, a synchronizer needs to allow the processes to control when
they want to switch views via a special ${\tt advance}$ call. We call such a
primitive an SMR synchronizer, to distinguish it from the less flexible
consensus synchronizer introduced above. This kind of synchronizers was first
introduced in (NK20, ; lumiere, ), but only used as an intermediate module to
implement a consensus synchronizer.

In this paper we show that SMR synchronizers can be directly exploited to
construct efficient and provably live SMR protocols and develop a general
blueprint that enables such constructions. In more detail:

  * •

We propose a formal specification of an SMR synchronizer (§3), which is
simpler and more general than prior proposals (lumiere, ; NK20, ). It is also
strictly stronger than the consensus synchronizer of (bftlive, ), which can be
obtained from the SMR synchronizer at no extra cost. Informally, our
specification guarantees that (a) the system will move to a new view if enough
correct processes call ${\tt advance}$, and (b) all correct processes will
enter the new view, provided that for long enough, no correct process that
enters this view asks to leave it. These properties enable correct processes
to iterate through views in search of a well-behaved leader, and to
synchronize in a view they are happy with.

  * •

We give an SMR synchronizer implementation and prove that it satisfies our
specification (§3.1). Unlike prior implementations (NK20, ), ours tolerates
message loss before ${\sf GST}$ while using only bounded space; in practice,
this feature is essential to defend against denial-of-service attacks. We also
provide a precise latency analysis of our synchronizer, quantifying how
quickly all correct processes enter the next view after enough of them call
${\tt advance}$.

  * •

We demonstrate the usability of our synchronizer specification by applying it
to construct and prove the correctness of several SMR protocols. First, we
prove the liveness of a variant of PBFT using an SMR synchronizer (§4-5): to
the best of our knowledge, this is the first rigorous proof of liveness for
PBFT’s algorithmic core. The proof establishes a strong liveness guarantee
that implies censorship-resistance: every command submitted by a correct
process will be executed. The use of the synchronizer specification in the
proof allows us to avoid dealing with view synchronization mechanics and
instead focus on protocol-specific reasoning. This reasoning is done using a
reusable methodology based on showing that the use of timers in the SMR
protocol and the synchronizer together establish properties similar to those
of failure detectors. The methodology also handles the realistic ways in which
protocols such as PBFT adapt their timeouts to the unknown message delay
$\delta$. We demonstrate the generality of our methodology by also applying it
to a version of PBFT with periodic leader changes (aardvark, ; spinning, ;
mirbft, ) and a HotStuff-like protocol (hotstuff, ) (§7).

  * •

We exploit the latency bounds for our synchronizer to establish both bad-case
and good-case bounds for variants of PBFT implemented on top of it (§6). Our
bad-case bound assumes that the protocol starts before ${\sf GST}$; it shows
that after ${\sf GST}$ all correct processes synchronize in the same view
within a bounded time. This time is proportional to a conservatively chosen
constant $\Delta$ that bounds post-${\sf GST}$ message delays in all
executions (sync-hotstuff, ; pass-shi, ; HK89, ). Our good-case bound
quantifies decision latency when the protocol starts after ${\sf GST}$ and
matches the lower bound of (ittai-good-case, ).

##  2\. System Model

We consider a system of $n=3f+1$ processes, out of which at most $f$ can be
Byzantine, i.e., can behave arbitrarily. In the latter case the process is
faulty; otherwise it is correct. We denote the set of all correct processes by
$\mathcal{C}$. We call a set $Q$ of $2f+1$ processes a quorum and write ${\sf
quorum}(Q)$. We assume standard cryptographic primitives (cachin-book, ,
§2.3): processes can communicate via authenticated point-to-point links, sign
messages using digital signatures, and use a collision-resistant hash function
${\sf hash}()$. We denote by $\langle m\rangle_{i}$ a message $m$ signed by
process $p_{i}$.

We consider a partial synchrony model (dls, ; CT96, ): for each execution of
the protocol, there exist a time ${\sf GST}$ and a duration $\delta$ such that
after ${\sf GST}$ message delays between correct processes are bounded by
$\delta$; before ${\sf GST}$ messages can get arbitrarily delayed or lost. As
in (CT96, ), we assume that the values of ${\sf GST}$ and $\delta$ are unknown
to the protocol. This reflects the requirements of practical systems, whose
designers cannot accurately predict when network problems leading to
asynchrony will stop and what the latency will be during the following
synchronous period. We also assume that processes have hardware clocks that
can drift unboundedly from real time before ${\sf GST}$, but do not drift
thereafter.

##  3\. SMR Synchronizer Specification and Implementation

We consider a synchronizer interface defined in (lumiere, ; NK20, ), which
here we call an SMR synchronizer. Let ${\sf View}=\\{1,2,\ldots\\}$ be the set
of views, ranged over by $v$; we use $0$ to denote an invalid initial view.
The synchronizer produces notifications ${\tt
new\texttt{\textunderscore}view}(v)$ at a process, telling it to enter view
$v$. To trigger these, the synchronizer allows a process to call a function
${\tt advance}()$, which signals that the process wishes to advance to a
higher view. For simplicity, we assume that a correct process does not call
${\tt advance}$ twice without an intervening ${\tt
new\texttt{\textunderscore}view}$ notification.

Our first contribution is the SMR synchronizer specification in Figure 1,
which is simpler and more general than prior proposals (lumiere, ; NK20, )
(see §8 for a discussion). The specification relies on the following notation.
Given a view $v$ entered by a correct process $p_{i}$, we denote by $E_{i}(v)$
the time when this happens; we let $E_{\rm first}(v)$ and $E_{\rm last}(v)$
denote respectively the earliest and the latest time when some correct process
enters $v$. We denote by $A_{i}(v)$ the time when a correct process $p_{i}$
calls ${\tt advance}$ while in $v$, and let $A_{\rm first}(v)$ and $A_{\rm
last}(v)$ denote respectively the earliest and the latest time when this
happens. Given a partial function $f$, we write $f(x)\mathpunct{\downarrow}$
if $f(x)$ is defined, and $f(x)\mathpunct{\uparrow}$ if $f(x)$ is undefined.
Thus, $E_{\rm first}(v)\mathpunct{\downarrow}$ means that some correct process
enters $v$, and $E_{\rm first}(v)\mathpunct{\uparrow}$ that no correct process
enters $v$.

The Monotonicity property in Figure 1 ensures that views can only increase at
a given process. Validity ensures that a process may only enter a view $v+1$
if some correct process has called ${\tt advance}$ in $v$. This prevents
faulty processes from disrupting the system by forcing view changes. As a
corollary of Validity we can prove that, if a view $v^{\prime}$ is entered by
some correct process, then so are all the views $v$ preceding $v^{\prime}$.

###### Proposition 3.1.

$\forall v,v^{\prime}.\,0<v<v^{\prime}\wedge{E_{\rm
first}(v^{\prime})\mathpunct{\downarrow}}{\implies}{E_{\rm
first}(v)\mathpunct{\downarrow}}\wedge E_{\rm first}(v)<E_{\rm
first}(v^{\prime})$.

Proof. Fix $v^{\prime}\geq 2$ and assume that a correct process enters
$v^{\prime}$, so that $E_{\rm first}(v^{\prime})\mathpunct{\downarrow}$. We
prove by induction on $k$ that $\forall k=0..(v^{\prime}-1).\,{E_{\rm
first}(v^{\prime}-k)\mathpunct{\downarrow}}\wedge E_{\rm
first}(v^{\prime}-k)\leq E_{\rm first}(v^{\prime})$. The base case of $k=0$ is
trivial. For the inductive step, assume that the required holds for some $k$.
Then by Validity there exists a time $t<E_{\rm first}(v^{\prime}-k)$ at which
some correct process $p_{j}$ attempts to advance from $v^{\prime}-k-1$. But
then $p_{j}$’s view at $t$ is $v^{\prime}-k-1$. Hence, $p_{j}$ enters
$v^{\prime}-k-1$ before $t$, so that $E_{\rm first}(v^{\prime}-k-1)<t<E_{\rm
first}(v^{\prime}-k)\leq E_{\rm first}(v^{\prime})$, as required.
$\sqcap$$\sqcup$

Bounded Entry ensures that if some process enters view $v$, then all correct
processes will do so within at most $d$ units of time of each other
($d=2\delta$ for our implementation). This only holds if within $d$ no process
attempts to advance to a higher view, as this may make some processes skip $v$
and enter a higher view directly. Bounded Entry also holds only starting from
some view $\mathcal{V}$, since a synchronizer may not be able to guarantee it
for views entered before ${\sf GST}$.

  1. 1.

Monotonicity. A process enters increasing views: $\forall
i,v,v^{\prime}.\,{E_{i}(v)\mathpunct{\downarrow}}\,\wedge\,{E_{i}(v^{\prime})\mathpunct{\downarrow}}\,{\implies}\,(v<v^{\prime}\,{\iff}\,E_{i}(v)<E_{i}(v^{\prime}))$

  2. 2.

Validity. A process may only enter a view $v+1$ if some correct process has
attempted to advance from $v$:
$\forall i,v.\,{E_{i}(v+1)\mathpunct{\downarrow}}\,{\implies}\,{A_{\rm
first}(v)\mathpunct{\downarrow}}\,\wedge\,A_{\rm first}(v)<E_{i}(v+1)$

  3. 3.

Bounded Entry. For some $\mathcal{V}$ and $d$, if a process enters a view
$v\geq\mathcal{V}$ and no process attempts to advance to a higher view within
time $d$, then all correct processes will enter $v$ within $d$:
$\exists\mathcal{V},d.\,\forall v\geq\mathcal{V}.\,{E_{\rm
first}(v)\mathpunct{\downarrow}}\,\wedge\,\neg(A_{\rm first}(v)<E_{\rm
first}(v)+d)\,{\implies}(\forall
p_{i}\in\mathcal{C}.\,{E_{i}(v)\mathpunct{\downarrow}})\,\wedge\,(E_{\rm
last}(v)\leq E_{\rm first}(v)+d)$

  4. 4.

Startup. Some correct process will enter view $1$ if $f+1$ processes call
${\tt advance}$:
$(\exists P\subseteq\mathcal{C}.\,|P|=f+1\,\wedge\,(\forall p_{i}\in
P.\,{A_{i}(0)\mathpunct{\downarrow}}))\,{\implies}\,{E_{\rm
first}(1)\mathpunct{\downarrow}}$

  5. 5.

Progress. If a correct process enters a view $v$ and, for some set $P$ of
$f+1$ correct processes, any process in $P$ that enters $v$ eventually calls
${\tt advance}$, then some correct process will enter view $v+1$:
$\forall v.\,{E_{\rm first}(v)\mathpunct{\downarrow}}\,\wedge\,(\exists
P\subseteq\mathcal{C}.\,|P|=f+1\,\wedge\,(\forall p_{i}\in
P.\,{E_{i}(v)\mathpunct{\downarrow}}\,{\implies}\,{A_{i}(v)\mathpunct{\downarrow}}))\,{\implies}\,{E_{\rm
first}(v+1)\mathpunct{\downarrow}}$

Figure 1. SMR synchronizer specification.

1

2when the process starts or timer expires

3 advance();

4

5

6upon ${\tt new\texttt{\textunderscore}view}(v)$

7 ${\tt stop\texttt{\textunderscore}timer}({\sf timer})$;

8 ${\tt start\texttt{\textunderscore}timer}({\sf timer},\tau)$;

9

Figure 2. A simple client of
an SMR synchronizer.

Startup ensures that some correct process enters view $1$ if $f+1$ processes
call ${\tt advance}$. Given a view $v$ entered by a correct process, Progress
determines conditions under which some correct process will enter the next
view $v+1$. This will happen if for some set $P$ of $f+1$ correct processes,
any process in $P$ entering $v$ eventually calls ${\tt advance}$. Note that
even a single ${\tt advance}$ call at a correct process may lead to a view
switch (reflecting the fact that in implementations faulty processes may help
this correct process). Startup and Progress ensure that the synchronizer must
switch if at least $f+1$ correct processes ask for this. We now illustrate a
typical pattern of their use, which we later apply to PBFT (§5). To this end,
we consider a simple client in Figure 2, where in each view a process sets a
timer for a fixed duration $\tau$ and calls ${\tt advance}$ when the timer
expires. Using Startup and Progress we prove that this client keeps switching
views forever as follows.

###### Proposition 3.2.

In any execution of the client in Figure 2: $\forall v.\,\exists
v^{\prime}.\,v^{\prime}>v\wedge{E_{\rm
first}(v^{\prime})\mathpunct{\downarrow}}$.

Proof. Since all correct processes initially call ${\tt advance}$, by Startup
some correct process eventually enters view $1$. Assume now that the
proposition is false, so that there is a maximal view $v$ entered by any
correct process. Let $P$ be any set of $f+1$ correct processes and consider an
arbitrary process $p_{i}\in P$ that enters $v$. When this happens, $p_{i}$
sets the ${\sf timer}$ for the duration $\tau$. The process then either calls
${\tt advance}$ when ${\sf timer}$ expires, or enters a new view $v^{\prime}$
before this. In the latter case $v^{\prime}>v$ by Monotonicity, which is
impossible. Hence, $p_{i}$ eventually calls ${\tt advance}$ while in $v$.
Since $p_{i}$ was chosen arbitrarily, $\forall p_{i}\in
P.\,{E_{i}(v)\mathpunct{\downarrow}}{\implies}{A_{i}(v)\mathpunct{\downarrow}}$.
Then by Progress we get $E_{\rm first}(v+1)\mathpunct{\downarrow}$, yielding a
contradiction.  $\sqcap$$\sqcup$

Similarly to Figure 2, we can use an SMR synchronizer satisfying the
properties in Figure 1 to implement a consensus synchronizer (bftlive, ; NK20,
) without extra overhead. This lacks an ${\tt advance}$ call and provides only
the ${\tt new\texttt{\textunderscore}view}$ notification, which it keeps
invoking at increasing intervals so that eventually the there is a view long
enough for the consensus protocol running on top to decide. We obtain a
consensus synchronizer if in Figure 2 we propagate the ${\tt
new\texttt{\textunderscore}view}$ notification to the consensus protocol and
set the ${\sf timer}$ to an unboundedly increasing function of views instead
of a constant $\tau$. In §A we show that the resulting consensus synchronizer
satisfies the specification proposed in (bftlive, ).

###  3.1. A Bounded-Space SMR Synchronizer

We now present a bounded-space algorithm that implements the specification in
Figure 1 under partial synchrony for $d=2\delta$. Our implementation reuses
algorithmic techniques from a consensus synchronizer of Bravo et al. (bftlive,
). However, it supports a more general abstraction, and thus requires a more
intricate correctness proof and latency analysis (§3.2).

1 2function __ advance()  3 send ${\tt WISH}(\max({\sf view}+1,{\sf view}^{+}))$ to all;  4 ${\sf advanced}\leftarrow\text{\sc true}$;  5 6 7 8periodically 9 if  _${\sf advanced}$_ then 10 send ${\tt WISH}(\max({\sf view}+1,{\sf view}^{+}))$ to all;  11 12 else if  _${\sf view}^{+} >0$_ then 13 send ${\tt WISH}({\sf view}^{+})$ to all;  14 15 16 |  17 18when received ${\tt WISH}(v)$ from $p_{j}$ 19 $\textit{prev{\textunderscore}v},\textit{prev{\textunderscore}v}^{+}\leftarrow{\sf view},{\sf view}^{+}$;  20 if  _$v >{\sf max\texttt{\textunderscore}views}[j]$_ then ${\sf max\texttt{\textunderscore}views}[j]\leftarrow v$;  21 ${\sf view}\ \ \leftarrow\max\\{v\mid\exists k.\,{\sf max\texttt{\textunderscore}views}[k]=v\wedge{}$ $|\\{j\mid{\sf max\texttt{\textunderscore}views}[j]\geq v\\}|\geq 2f+1\\}$;  22 ${\sf view}^{+}\leftarrow\max\\{v\mid\exists k.\,{\sf max\texttt{\textunderscore}views}[k]=v\wedge{}$ $|\\{j\mid{\sf max\texttt{\textunderscore}views}[j]\geq v\\}|\geq f+1\\}$;  23 if  _${\sf view}^{+}={\sf view}\wedge{\sf view} >\textit{prev{\textunderscore}v}$_ then 24 trigger ${\tt new\texttt{\textunderscore}view}({\sf view})$; ${\sf advanced}\leftarrow\text{\sc false}$;  25 26 if  _${\sf view}^{+} >\textit{prev{\textunderscore}v}^{+}$_ then send ${\tt WISH}({\sf view}^{+})$ to all;  27 28
---|---
Figure 3. A bounded-space SMR synchronizer. The periodic handler fires every
$\rho$ units of time. All counters are initially $0$.

When a process calls ${\tt advance}$ (line 3), the synchronizer does not
immediately move to the next view $v^{\prime}$, but disseminates a ${\tt
WISH}(v^{\prime})$ message announcing its intention. A process enters a new
view once it accumulates a sufficient number of ${\tt WISH}$ messages
supporting this. A naive synchronizer design could follow Bracha broadcast
(random-bracha, ): enter a view $v^{\prime}$ upon receiving $2f+1$ ${\tt
WISH}(v^{\prime})$ messages, and echo ${\tt WISH}(v^{\prime})$ upon receiving
$f+1$ copies thereof; the latter is needed to combat equivocation by Byzantine
processes. However, in this case the process would have to track all newly
proposed views for which $<2f+1$ ${\tt WISH}$es have been received. Since
messages sent before ${\sf GST}$ can be lost or delayed, this would require
unbounded space. To reduce the space complexity, in our algorithm a process
only remembers the highest view received from each process, kept in an array
${\sf max\texttt{\textunderscore}views}:\\{1,\ldots,n\\}\rightarrow{\sf
View}\cup\\{0\\}$ (line 3). This array is then used to compute variables ${\sf
view}$ and ${\sf view}^{+}$, which respectively hold the $(2f\,{+}\,1)$st
highest and the $(f\,{+}\,1)$st highest views in ${\sf
max\texttt{\textunderscore}views}$ (lines 3-3). These variables never decrease
and always satisfy ${\sf view}\leq{\sf view}^{+}$.

The process enters the view stored in the ${\sf view}$ variable when this
variable increases (lines 3-3). A process thus enters a view $v$ only if it
receives $2f+1$ ${\tt WISH}$es for views $\geq v$, and a process may be forced
to switch views even if it did not call ${\tt advance}$; the latter helps
lagging processes to catch up. The variable ${\sf view}^{+}$ increases when
the process receives $f+1$ ${\tt WISH}$es for views $\geq{\sf view}^{+}$, and
thus some correct process wishes to enter a new view $\geq{\sf view}^{+}$. In
this case the process echoes ${\sf view}^{+}$ (line 3), to help processes
switch views and satisfy Bounded Entry and Progress.

The guard ${\sf view}^{+}={\sf view}$ in line 3 ensures that a process does
not enter a “stale” view such that another correct process already wishes to
enter a higher one. Similarly, when the process calls ${\tt advance}$, it
sends a ${\tt WISH}$ for the maximum of ${\sf view}+1$ and ${\sf view}^{+}$
(line 3). Thus, if ${\sf view}={\sf view}^{+}$, so that the values of the two
variables have not changed since the process entered the current view, then
the process sends a ${\tt WISH}$ for the next view (${\sf view}+1$).
Otherwise, ${\sf view}<{\sf view}^{+}$, and the process sends a ${\tt WISH}$
for the higher view ${\sf view}^{+}$. Finally, to deal with message loss
before ${\sf GST}$, a process retransmits the highest ${\tt WISH}$ it sent
every $\rho$ units of time, according to its local clock (line 3). Depending
on whether the process has called ${\tt advance}$ in the current view (tracked
by the advanced flag), the ${\tt WISH}$ is computed as in lines 3 or 3.

Our SMR synchronizer requires only $O(n)$ variables for storing views.
Proposition 3.1 also ensures that views entered by correct processes do not
skip values. Thus, although the individual view values stored by the
synchronizer are unbounded, Proposition 3.1 limits the power of the adversary
to exhaust their allocated space, similarly to (BazziD04, ).

###  3.2. SMR Synchronizer Correctness and Latency Bounds

The following theorem (proved in §B) states the correctness of our
synchronizer as well as and its performance properties. In §6 we apply the
latter to bound the latency of Byzantine SMR protocols. Given a view $v$ that
was entered by a correct process $p_{i}$, we let $T_{i}(v)$ denote the time at
which $p_{i}$ either attempts to advance from $v$ or enters a view $>v$; we
let $T_{\rm last}(v)$ denote the latest time when a correct process does so.
We assume that every correct process eventually attempts to advance from view
$0$ unless it enters a view $>0$, i.e., $\forall
p_{i}\in\mathcal{C}.\,T_{i}(0)\mathpunct{\downarrow}$.

###### Theorem 3.3.

Consider an execution with an eventual message delay $\delta$. In this
execution, the algorithm in Figure 3 satisfies the properties in Figure 1 for
$d=2\delta$ and $\mathcal{V}=\max\\{v\mid({E_{\rm
first}(v)\mathpunct{\downarrow}}\,\wedge\,E_{\rm first}(v)<{\sf GST}+\rho)\vee
v=0\\}+1$ if $A_{\rm first}(0)<{\sf GST}$, and $\mathcal{V}=1$, otherwise.
Furthermore, the algorithm also satisfies the following:

  1. A.

$\forall v.\,{E_{\rm first}(v)\mathpunct{\downarrow}}\,\wedge\,A_{\rm
first}(0)<{\sf GST}\,{\implies}\,E_{\rm last}(v)\leq\max(E_{\rm first}(v),{\sf
GST}+\rho)+2\delta$.

  2. B.

$\forall v.\,{E_{\rm first}(v+1)\mathpunct{\downarrow}}\,{\implies}\,E_{\rm
last}(v+1)\leq\begin{cases}\max(T_{\rm last}(v),{\sf
GST}+\rho)+\delta,&\text{if }A_{\rm first}(0)<{\sf GST};\\\\[-1.0pt] T_{\rm
last}(v)+\delta,&\text{otherwise.}\end{cases}$

The theorem gives a witness for $\mathcal{V}$ in Bounded Entry: it is the next
view after the highest one entered by a correct process at or before ${\sf
GST}+\rho$ (or $1$ if no view was entered). Property A bounds the latest time
any correct process can enter a view that has been previously entered by a
correct process. It is similar to Bounded Entry, but also handles views
$<\mathcal{V}$. Property B refines Progress: while the latter guarantees that
the synchronizer will enter $v+1$ if enough processes ask for this, the former
bounds the time by which this will happen. We explain the use of these
properties in §6.

##  4\. PBFT Using an SMR Synchronizer

We now demonstrate how an SMR synchronizer can be used to implement Byzantine
SMR. More formally, we implement Byzantine atomic broadcast (cachin-book, ),
from which SMR can be implemented in the standard way (smr, ). This allows
processes to broadcast values, and we assume an application-specific predicate
to indicate whether a value is valid (cachin-crypto01, ; vaba, ) (e.g., a
block in a blockchain is invalid if it lacks correct signatures). We assume
that all values broadcast by correct processes in a single execution are valid
and unique. Then Byzantine atomic broadcast is defined by the following
properties:

  * •

Integrity. Every process delivers a value at most once.

  * •

External Validity. A correct process delivers only values satisfying ${\sf
valid}()$.

  * •

Ordering. If a correct process $p$ delivers $x_{1}$ before $x_{2}$, then
another correct process $q$ cannot deliver $x_{2}$ before $x_{1}$.

  * •

Liveness. If a correct process broadcasts or delivers $x$, then eventually all
correct processes will deliver $x$. (Note that this implies censorship-
resistance: the service cannot selectively omit values submitted by correct
processes.)

#### The PBFT-light protocol.

We implement Byzantine atomic broadcast in a PBFT-light protocol (Figures
4-6), which faithfully captures the algorithmic core of the seminal Practical
Byzantine Fault Tolerance protocol (PBFT) (pbft, ). Whereas PBFT integrated
view synchronization functionality with the core SMR protocol, PBFT-light
delegates this to an SMR synchronizer, and in §5 we rigorously prove its
liveness when using any synchronizer satisfying our specification. When using
the synchronizer in Figure 3, the protocol also incurs only bounded space
overhead (see §C.4 for details).

We base PBFT-light on the PBFT protocol with signatures and, for simplicity,
omit the mechanisms for managing checkpoints and watermarks; these can be
easily added without affecting liveness. The protocol works in a succession of
views produced by the synchronizer. A process stores its current view in ${\sf
curr\texttt{\textunderscore}view}$. Each view $v$ has a fixed leader ${\sf
leader}(v)=p_{((v-1)\ \mathrel{\rm mod}\ n)+1}$ that is responsible for
totally ordering values submitted for broadcast; the other processes are
followers, which vote on proposals made by the leader. Processes store the
sequence of (unique) values proposed by the leader in a ${\sf log}$ array; at
the leader, a ${\sf next}$ counter points to the first free slot in the array.
Processes monitor the leader’s behavior and ask the synchronizer to advance to
another view if they suspect that the leader is faulty. A ${\sf status}$
variable records whether the process is operating as normal in the current
view (normal) or is changing the view.

1 2function ${\tt start}()$ 3 if  _${\sf curr\texttt{\textunderscore}view}=0$_ then advance();  4 5 6 7when a timer expires 8 ${\tt stop\texttt{\textunderscore}all\texttt{\textunderscore}timers}()$;  9 ${\tt advance}()$;  10 ${\sf status}\leftarrow\textsc{advanced}$;  11 ${\sf dur\texttt{\textunderscore}delivery}\leftarrow{\sf dur\texttt{\textunderscore}delivery}+\tau$;  12 ${\sf dur\texttt{\textunderscore}recovery}\leftarrow{\sf dur\texttt{\textunderscore}recovery}+\tau$;  13 14 15 16function ${\tt broadcast}(x)$ 17 pre: ${\sf valid}(x)$;  18 send $\langle{\tt BROADCAST}(x)\rangle_{i}$ to all periodically until $x$ is delivered 19 20 21when received ${\tt BROADCAST}(x)$ 22 pre: ${\sf valid}(x)\wedge{\sf status}=\textsc{normal}\wedge{}$ $\phantom{\text{{\bf pre:} }}{\sf timer\texttt{\textunderscore}delivery}[x]$ not active  $\phantom{\text{{\bf pre:} }}(\forall k.\,k\leq{\sf last\texttt{\textunderscore}delivered}{\implies}{}$ $\phantom{\text{{\bf pre:} }(}{\sf commit\texttt{\textunderscore}log}[k]\not=x)$;  23 ${\tt start\texttt{\textunderscore}timer}({\sf timer\texttt{\textunderscore}delivery}[x],$ ${\sf dur\texttt{\textunderscore}delivery})$;  24 send $\langle{\tt FORWARD}(x)\rangle_{i}$ to ${\sf leader}({\sf curr\texttt{\textunderscore}view})$;  25 26 27 28when received ${\tt FORWARD}(x)$ 29 pre: ${\sf valid}(x)\wedge p_{i}={\sf leader}({\sf curr\texttt{\textunderscore}view})\wedge{}$ $\phantom{\text{{\bf pre:} }}{\sf status}=\textsc{normal}\wedge\forall k.\,{\sf log}[k]\not=x$;  30 send $\langle{\tt PREPREPARE}({\sf curr\texttt{\textunderscore}view},$ ${\sf next},x)\rangle_{i}$ to all;  31 ${\sf next}\leftarrow{\sf next}+1$;  32 33 |  34 when received $\langle{\tt PREPREPARE}(v,k,x)\rangle_{j}$ 35 pre: $p_{j}={\sf leader}(v)\wedge{\sf curr\texttt{\textunderscore}view}=v\wedge{\sf status}=\textsc{normal}\wedge{}$ $\phantom{\text{{\bf pre:} }}{\sf phase}[k]=\textsc{start}\wedge{\sf valid}(x)\wedge(\forall k^{\prime}.\,{\sf log}[k^{\prime}]\not=x)$ 36 $({\sf log},{\sf phase})[k]\leftarrow(x,\textsc{preprepared})$;  37 send $\langle{\tt PREPARE}(v,k,{\sf hash}(x))\rangle_{i}$ to all;  38 39 40 41when received $\\{\langle{\tt PREPARE}(v,k,h)\rangle_{j}\mid p_{j}\in Q\\}\,{=}\,C$ for a quorum $Q$ 42 pre: ${\sf curr\texttt{\textunderscore}view}=v\wedge{\sf phase}[k]=\textsc{preprepared}\wedge{}$ $\phantom{\text{{\bf pre:} }}{}{\sf status}=\textsc{normal}\wedge{\sf hash}({\sf log}[k])=h$;  43 $({\sf prep\texttt{\textunderscore}log},{\sf prep\texttt{\textunderscore}view},{\sf cert},{\sf phase})[k]\leftarrow{}$ $\quad({\sf log}[k],{\sf curr\texttt{\textunderscore}view},C,\textsc{prepared})$;  44 send $\langle{\tt COMMIT}(v,k,h)\rangle_{i}$ to all;  45 46 47 48when received $\\{\langle{\tt COMMIT}(v,k,h)\rangle_{j}\mid p_{j}\in Q\\}=C$ for a quorum $Q$ 49 pre: ${\sf curr\texttt{\textunderscore}view}=v\wedge{\sf phase}[k]=\textsc{prepared}\wedge{}$ $\phantom{\text{{\bf pre:} }}{\sf status}=\textsc{normal}\wedge{\sf hash}({\sf prep\texttt{\textunderscore}log}[k])=h$;  50 $({\sf commit\texttt{\textunderscore}log},{\sf phase})[k]\leftarrow({\sf log}[k],\textsc{committed})$;  51 broadcast $\langle{\tt DECISION}({\sf commit\texttt{\textunderscore}log}[k],k,C)$;  52 53 54 55when ${\sf commit\texttt{\textunderscore}log}[{\sf last\texttt{\textunderscore}delivered}+1]\not=\bot$ 56 ${\sf last\texttt{\textunderscore}delivered}\leftarrow{\sf last\texttt{\textunderscore}delivered}+1$;  57 if  _${\sf commit\texttt{\textunderscore}log}[{\sf last\texttt{\textunderscore}delivered}]\not={\tt nop}$_ then 58 ${\tt deliver}({\sf commit\texttt{\textunderscore}log}[{\sf last\texttt{\textunderscore}delivered}])$ 59 ${\tt stop\texttt{\textunderscore}timer}({\sf timer\texttt{\textunderscore}delivery}[{\sf commit\texttt{\textunderscore}log}[{\sf last\texttt{\textunderscore}delivered}]])$;  60 if  _${\sf last\texttt{\textunderscore}delivered}={\sf init\texttt{\textunderscore}log\texttt{\textunderscore}length}\wedge{\sf status}={\textsc{normal}}$_ then 61 ${\tt stop\texttt{\textunderscore}timer}({\sf timer\texttt{\textunderscore}recovery})$;  62 63 64 65when received ${\tt DECISION}(x,k,C)$ 66 pre: ${\sf commit\texttt{\textunderscore}log}[k]\not=\bot\wedge\exists v.\,{\sf committed}(C,v,k,{\sf hash}(x))$;  67 ${\sf commit\texttt{\textunderscore}log}[k]\leftarrow x$;  68 69
---|---
Figure 4. Normal operation of PBFT-light at a process $p_{i}$.

#### Normal protocol operation.

A process broadcasts a valid value $x$ using a ${\tt broadcast}$ function
(line 4), which keeps sending the value to all processes in a ${\tt
BROADCAST}$ message until the process delivers the value. The periodic
retransmission ensures that the value will reach the processes despite message
loss before ${\sf GST}$. When a process receives a ${\tt BROADCAST}$ message
with a new value (line 4), it forwards the value to the leader in a ${\tt
FORWARD}$ message. This ensures that the value reaches the leader even when
broadcast by a faulty process, which may withhold the ${\tt BROADCAST}$
message from the leader. (We explain the timer set in line 4 later.) When the
leader receives a new value $x$ in a ${\tt FORWARD}$ message (line 4), it
sends a ${\tt PREPREPARE}$ message to all processes (including itself) that
includes $x$ and its position in the log, generated from the ${\sf next}$
counter. Processes vote on the leader’s proposal in two phases. Each process
keeps track of the status of values going through the vote in an array ${\sf
phase}$, whose entries initially store start.

When a process receives a proposal $x$ for a position $k$ from the leader of
its view $v$ (line 4), it first checks that ${\sf phase}[k]$ is start, so that
it has not yet accepted a proposal for the position $k$ in the current view.
It also checks that the value is valid and distinct from all values it knows
about. The process then stores $x$ in ${\sf log}[k]$ and advances ${\sf
phase}[k]$ to preprepared. Since a faulty leader may send different proposals
for the same position to different processes, the process next communicates
with others to check that they received the same proposal. To this end, it
disseminates a ${\tt PREPARE}$ message with the position and the hash of the
value $x$ it received. The process handles $x$ further once it gathers a set
$C$ of ${\tt PREPARE}$ messages from a quorum matching the value (line 4),
which we call a prepared certificate and check using the ${\sf prepared}$
predicate in Figure 6. In this case the process stores the value in ${\sf
prep\texttt{\textunderscore}log}[k]$, the certificate in ${\sf cert}[k]$, and
the view in which it was formed in ${\sf
prep\texttt{\textunderscore}view}[k]$. At this point we say that the process
prepared the proposal, which is recorded by setting its ${\sf phase}$ to
prepared. It is easy to show that processes cannot prepare different values at
the same position and view, since each correct process can send only one
corresponding ${\tt PREPARE}$ message.

Having prepared a value, the process disseminates a ${\tt COMMIT}$ message
with the hash of the value. Once the process gathers a quorum of matching
${\tt COMMIT}$ messages (line 4), it stores the value in a ${\sf
commit\texttt{\textunderscore}log}$ array and advances its ${\sf phase}$ to
committed; we then say that the value is committed. The protocol ensures that
correct processes cannot commit different values at the same position, even in
different views. We call a quorum of matching ${\tt COMMIT}$ messages a commit
certificate and check it using the ${\sf committed}$ predicate in Figure 6. A
process delivers committed values in the ${\sf
commit\texttt{\textunderscore}log}$ order, with ${\sf
last\texttt{\textunderscore}delivered}$ tracking the position of the last
delivered value.

To satisfy the Liveness property of atomic broadcast, similarly to (alysson-
reads, ), PBFT-light allows a process to find out about committed values from
other processes directly. When a correct process commits a value (line 4), it
disseminates a ${\tt DECISION}$ message with the value, its position $k$ in
the log and the commit certificate (line 4). A process receiving such a
message with a valid certificate saves the value in ${\sf
commit\texttt{\textunderscore}log}[k]$, which allows it to be delivered (line
4). The ${\tt DECISION}$ messages are disseminated via a form of reliable
broadcast ensuring that, if a correct process delivers the value, then so do
all other correct processes. To implement this, each process could
periodically resend the ${\tt DECISION}$ messages it has (omitted from the
pseudocode). A more practical implementation would only resend information
that other processes are missing. As proved in (dls, ), such periodic resends
are unavoidable in the presence of message loss.

#### View initialization.

When the synchronizer tells a process to move to a new view $v$ (line 5), the
process sets ${\sf curr\texttt{\textunderscore}view}$ to $v$, which ensures
that it will no longer accept messages from prior views. It also sets ${\sf
status}$ to initializing, which means that the process is not yet ready to
order values in the new view. It then sends a ${\tt
NEW\texttt{\textunderscore}LEADER}$ message to the leader of $v$ with the
information about the values it has prepared so far and the corresponding
certificates.111In PBFT this information is sent in VIEW-CHANGE messages,
which also play a role similar to ${\tt WISH}$ messages in our synchronizer
(Figure 3). In PBFT-light we opted to eschew VIEW-CHANGE messages to maintain
a clear separation between view synchronization internals and the SMR
protocol.

53 upon ${\tt new\texttt{\textunderscore}view}(v)$ 54 ${\tt stop\texttt{\textunderscore}all\texttt{\textunderscore}timers}()$;  55 ${\sf curr\texttt{\textunderscore}view}\leftarrow v$;  56 ${\sf status}\leftarrow\textsc{initializing}$;  57 send $\langle{\tt NEW\texttt{\textunderscore}LEADER}({\sf curr\texttt{\textunderscore}view},{\sf prep\texttt{\textunderscore}view},$ ${\sf prep\texttt{\textunderscore}log},{\sf cert})\rangle_{i}$ to ${\sf leader}({\sf curr\texttt{\textunderscore}view})$;  58 ${\tt start\texttt{\textunderscore}timer}({\sf timer\texttt{\textunderscore}recovery},$ ${\sf dur\texttt{\textunderscore}recovery})$;  59 60 61 62when received $\\{\langle{\tt NEW\texttt{\textunderscore}LEADER}(v,\mathit{prep\texttt{\textunderscore}view}_{j},$ $\mathit{prep\texttt{\textunderscore}log}_{j},\mathit{cert}_{j})\rangle_{j}\mid$ $p_{j}\in Q\\}=M$ for a quorum $Q$ 63 pre: $p_{i}={\sf leader}(v)\wedge{\sf curr\texttt{\textunderscore}view}=v\wedge{}$ $\phantom{\text{{\bf pre:} }}{\sf status}=\textsc{initializing}\wedge{}$ $\phantom{\text{{\bf pre:} }}\forall m\in M.\,{\sf ValidNewLeader}(m)$;  64 forall  _$k$_ do 65 if  _$\exists p_{j^{\prime}}\in Q.\,\mathit{prep\texttt{\textunderscore}view}_{j^{\prime}}[k]\not=0\wedge{}$ $\forall p_{j}\in Q.\,\mathit{prep\texttt{\textunderscore}view}_{j}[k]\leq\mathit{prep\texttt{\textunderscore}view}_{j^{\prime}}[k]$_ then $\mathit{log}^{\prime}[k]\leftarrow\mathit{prep\texttt{\textunderscore}log}_{j^{\prime}}[k]$;  66 67 ${\sf next}\leftarrow\max\\{k\mid\mathit{log}^{\prime}[k]\neq\bot\\}$;  68 69 |  70 forall  _$k=1..({\sf next}-1)$_ do 71 if  _$\mathit{log}^{\prime}[k]=\bot\vee\exists k^{\prime}.\,k^{\prime}\not=k\wedge\mathit{log}^{\prime}[k^{\prime}]=\mathit{log}^{\prime}[k]\wedge{}$ $\exists p_{j^{\prime}}\in Q.\,\forall p_{j}\in Q.\,\mathit{prep\texttt{\textunderscore}view}_{j^{\prime}}[k^{\prime}]>\mathit{prep\texttt{\textunderscore}view}_{j}[k]$_ then $\mathit{log}^{\prime}[k]\leftarrow{\tt nop}$;  72 73 send $\langle{\tt NEW\texttt{\textunderscore}STATE}(v,\mathit{log}^{\prime},M)\rangle_{i}$ to all;  74 75 76 77when received $\langle{\tt NEW\texttt{\textunderscore}STATE}(v,\mathit{log}^{\prime},M)\rangle_{j}=m$ 78 pre: ${\sf status}=\textsc{initializing}\wedge{\sf curr\texttt{\textunderscore}view}=v\wedge{}$ $\phantom{\text{{\bf pre:} }}{\sf ValidNewState}(m)$;  79 ${\sf log}\leftarrow\mathit{log}^{\prime}$;  80 forall  _$\\{k\mid{\sf log}[k]\not=\bot\\}$_ do 81 ${\sf phase}[k]\leftarrow\textsc{preprepared}$;  82 send $\langle{\tt PREPARE}(v,k,{\sf hash}({\sf log}[k]))\rangle_{i}$ to all;  83 84 ${\sf status}\leftarrow\textsc{normal}$;  85 ${\sf init\texttt{\textunderscore}log\texttt{\textunderscore}length}\leftarrow\max\\{k\mid{\sf log}[k]\neq\bot\\}$;  86 if  _${\sf init\texttt{\textunderscore}log\texttt{\textunderscore}length}\leq{\sf last\texttt{\textunderscore}delivered}$_ then 87 ${\tt stop\texttt{\textunderscore}timer}({\sf timer\texttt{\textunderscore}recovery})$;  88 89 90
---|---
Figure 5. View-initialization protocol of PBFT-light at a process $p_{i}$.

$\displaystyle{\sf prepared}(C,v,k,h)\iff\exists Q.\,{\sf quorum}(Q)\wedge
C=\\{\langle{\tt PREPARE}(v,k,h)\rangle_{j}\mid p_{j}\in Q\\}$
$\displaystyle{\sf committed}(C,v,k,h)\iff\exists Q.\,{\sf quorum}(Q)\wedge
C=\\{\langle{\tt COMMIT}(v,k,h)\rangle_{j}\mid p_{j}\in Q\\}$
$\displaystyle\begin{array}[]{@{}l@{}}{\sf ValidNewLeader}(\langle{\tt
NEW\texttt{\textunderscore}LEADER}(v,\mathit{prep\texttt{\textunderscore}view},\mathit{prep\texttt{\textunderscore}log},\mathit{cert})\rangle_{\texttt{\textunderscore}})\iff{}\\\\[2.0pt]
\forall
k.\,(\mathit{prep\texttt{\textunderscore}view}[k]>0{\implies}\mathit{prep\texttt{\textunderscore}view}[k]<v\wedge{\sf
prepared}(\mathit{cert}[k],\mathit{prep\texttt{\textunderscore}view}[k],k,\mathit{prep\texttt{\textunderscore}log}[k]))\end{array}$
$\displaystyle\begin{array}[]{@{}l@{}}{\sf ValidNewState}(\langle{\tt
NEW\texttt{\textunderscore}STATE}(v,\mathit{log}^{\prime},M)\rangle_{i})\iff
p_{i}={\sf leader}(v)\wedge\exists
Q,\mathit{prep\texttt{\textunderscore}view},\mathit{prep\texttt{\textunderscore}log},\mathit{cert}.\,{\sf
quorum}(Q)\wedge{}\\\\[2.0pt] M=\\{\langle{\tt
NEW\texttt{\textunderscore}LEADER}(v,\mathit{prep\texttt{\textunderscore}view}_{j},\mathit{log}_{j},\mathit{cert}_{j})\rangle_{j}\mid
p_{j}\in Q\\}\wedge{}\\\\[2.0pt] (\forall m\in C.\,{\sf
ValidNewLeader}(m))\wedge(\mathit{log}^{\prime}\mbox{ is computed from $M$ as
per lines~{}\ref{alg:castro:select-proposal}-\ref{alg:castro:newview-
end}})\end{array}$

Figure 6. Auxiliary predicates for PBFT-light.

The new leader waits until it receives a quorum of well-formed ${\tt
NEW\texttt{\textunderscore}LEADER}$ messages, as checked by the predicate
${\sf ValidNewLeader}$ (line 5). Based on these, the leader computes the
initial log of the new view, stored in $\mathit{log}^{\prime}$. Similarly to
Paxos (paxos, ), for each index $k$ the leader puts at the $k$th position in
$\mathit{log}^{\prime}$ the value prepared in the highest view (line 5). The
resulting array may contain empty or duplicate entries. To resolve this, the
leader writes ${\tt nop}$ into empty entries and those entries for which there
is a duplicate prepared in a higher view (line 5). The latter is safe because
one can show that no value could have been committed in such entries in prior
views. Finally, the leader sends a ${\tt NEW\texttt{\textunderscore}STATE}$
message to all processes, containing the initial log and the ${\tt
NEW\texttt{\textunderscore}LEADER}$ messages from which it was computed (line
5).

A process receiving the ${\tt NEW\texttt{\textunderscore}STATE}$ message first
checks its correctness by redoing the leader’s computation, as specified by
the ${\sf ValidNewState}$ predicate (line 5). If the check passes, the process
overwrites its log with the new one and sets ${\sf status}$ to normal. It also
sends ${\tt PREPARE}$ messages for all ${\sf log}$ entries, to commit them in
the new view. A more practical version of the protocol would include a
checkpointing mechanism, so that a process restarts committing previous ${\sf
log}$ entries only from the last stable checkpoint (pbft, ); this mechanism
can be easily added to PBFT-light.

#### Triggering view changes.

We now describe when a process calls ${\tt advance}$, which is key to ensure
liveness (§5). This happens either on start-up (line 4) or when the process
suspects that the current leader is faulty. To this end, the process monitors
the leader’s behavior using timers; if one of these expires, the process calls
${\tt advance}$ and sets ${\sf status}$ to advanced (line 4). First, the
process checks that each value it receives is delivered promptly: e.g., to
guard against a faulty leader not making any proposals or censoring certain
values. For a value $x$ this is done using ${\sf
timer\texttt{\textunderscore}delivery}[x]$, set for a duration ${\sf
dur\texttt{\textunderscore}delivery}$ when the process receives ${\tt
BROADCAST}(x)$ (lines 4). The timer is stopped when the process delivers $x$
(line 4). A process also checks that the leader initializes a view quickly
enough: e.g., to guard against the leader crashing during the initialization.
Thus, when a process enters a view it starts ${\sf
timer\texttt{\textunderscore}recovery}$ for a duration ${\sf
dur\texttt{\textunderscore}recovery}$ (line 5). The process stops the timer
when it delivers all values in the initial log (lines 4 and 5).

The above checks may make a process suspect a correct leader if the timeouts
are initially set too small with respect to the message delay $\delta$,
unknown to the process. To deal with this, a process increases ${\sf
dur\texttt{\textunderscore}delivery}$ and ${\sf
dur\texttt{\textunderscore}recovery}$ each time a timer expires, which signals
that the current view is not operating normally (lines 4-4). This way of
adapting timeouts is used in the original PBFT (castro-thesis, , §2.3.5), and
as we show §7, also benefits other protocols.

##  5\. Proving the Liveness of PBFT

Assume that PBFT-light is used with a synchronizer satisfying the
specification in Figure 1; to simplify the following latency analysis, we
assume $d=2\delta$, as for the synchronizer in Figure 3. We now prove that the
protocol satisfies the Liveness property of Byzantine atomic broadcast; we
defer the proof of the other properties to §C.1. To the best of our knowledge,
this is the first rigorous proof of liveness for the algorithmic core of PBFT:
as we elaborate in §8, the liveness mechanisms of PBFT came only with a brief
informal justification, which did not cover their most critical properties
(castro-tocs, , §4.5.1). Our proof is simplified by the use of the
synchronizer specification, which allows us to avoid dealing with view
synchronization mechanics. It also provides a methodology that we reuse to
prove the liveness of other protocols (§7).

We prove the liveness of PBFT-light by showing that the protocol establishes
properties reminiscent of those of failure detectors (CT96, ). First,
similarly to their completeness property, we prove that every correct process
eventually attempts to advance from a bad view in which no progress is
possible (e.g., because the leader is faulty).

###### Lemma 5.1.

Assume that a correct process $p_{i}$ receives ${\tt BROADCAST}(x)$ for a
valid value $x$ while in a view $v$. If $p_{i}$ never delivers $x$ and never
enters a view higher than $v$, then it eventually calls ${\tt advance}$ in
$v$.

The lemma holds because in PBFT-light each process monitors the leader’s
behavior using timers, and we defer its easy proof to §C.2. Note that even
though this monitoring ensures that correct processes will eventually try to
advance from a view with a faulty leader, the SMR protocol by itself does not
ensure that the processes will actually enter a new view with a different
leader. Achieving this is the job of the synchronizer, and in the following
proof of PBFT-light we show that this happens using the Progress property in
Figure 1 together with Lemma 5.1.

The next lemma we establish is similar to the eventual accuracy property of
failure detectors. It stipulates that if the timeout values are high enough,
then eventually any correct process that enters a good view (with a correct
leader) will never attempt to advance from it. Let ${\sf
dur\texttt{\textunderscore}recovery}_{i}(v)$ and ${\sf
dur\texttt{\textunderscore}delivery}_{i}(v)$ denote respectively the value of
the ${\sf dur\texttt{\textunderscore}recovery}$ and ${\sf
dur\texttt{\textunderscore}delivery}$ variable at a correct process $p_{i}$
while in view $v$.

###### Lemma 5.2.

Consider a view $v\geq\mathcal{V}$ such that $E_{\rm first}(v)\geq{\sf GST}$
and ${\sf leader}(v)$ is correct. If ${\sf
dur\texttt{\textunderscore}recovery}_{i}(v)>6\delta$ and ${\sf
dur\texttt{\textunderscore}delivery}_{i}(v)>4\delta$ at each correct process
$p_{i}$ that enters $v$, then no correct process calls ${\tt advance}$ in $v$.

Figure 7. An illustration of the bound on ${\sf
dur\texttt{\textunderscore}recovery}$ in Lemma 5.2.

Before proving the lemma, we informally explain the rationale for the bounds
on timeouts in it, using the example of ${\sf
dur\texttt{\textunderscore}recovery}$. The timer ${\sf
timer\texttt{\textunderscore}recovery}$ is started at a process $p_{i}$ when
this process enters a view $v$ (line 5), and is stopped when the process
delivers all values inherited from previous views (lines 4 or 5). The two
events are separated by $4$ communication steps of PBFT-light, exchanging
messages of the types ${\tt NEW\texttt{\textunderscore}LEADER}$, ${\tt
NEW\texttt{\textunderscore}STATE}$, ${\tt PREPARE}$ and ${\tt COMMIT}$ (Figure
7). However, $4\delta$ would be too small a value for ${\sf
dur\texttt{\textunderscore}recovery}$. This is because the leader of $v$ sends
its ${\tt NEW\texttt{\textunderscore}STATE}$ message only after receiving a
quorum of ${\tt NEW\texttt{\textunderscore}LEADER}$ messages, and different
processes may enter $v$ and send their ${\tt
NEW\texttt{\textunderscore}LEADER}$ messages at different times (e.g., $p_{i}$
and $p_{j}$ in Figure 7). Hence, ${\sf dur\texttt{\textunderscore}recovery}$
must additionally accommodate the maximum discrepancy in the entry times,
which is $d=2\delta$ by the Bounded Entry property. Then to ensure that
$p_{i}$ stops the timer before it expires, we require ${\sf
dur\texttt{\textunderscore}recovery}_{i}(v)>6\delta$. As the above reasoning
illustrates, Lemma 5.2 is more subtle than Lemma 5.1: while the latter is
ensured just by the checks in the SMR protocol, the former relies on the
Bounded Entry property of the synchronizer.

Another subtlety about Lemma 5.2 is that the $\delta$ used in its premise is a
priori unknown. Hence, to apply the lemma in the liveness proof of PBFT-light,
we have to argue that, if correct processes keep changing views due to lack of
progress, then all of them will eventually increase their timeouts high enough
to satisfy the bounds in Lemma 5.2. This is nontrivial due to the fact that,
as in the original PBFT, in our protocol the processes update their timeouts
independently, and may thus disagree on their durations. For example, the
first correct process $p_{i}$ to detect a problem with the current view $v$
will increase its timeouts and call ${\tt advance}$ (line 4). The synchronizer
may then trigger ${\tt new\texttt{\textunderscore}view}$ notifications at
other correct processes before they detect the problem as well, so that their
timeouts will stay unchanged (line 5).222Recall that even a single ${\tt
advance}$ call at a correct process may lead to a view switch (§3). For
example, with the synchronizer in Figure 3 this may happen as follows. The
${\tt advance}$ call at a process generates ${\tt WISH}(v+1)$ (line 3) and the
Byzantine processes produce another $f$ copies of the same message. Correct
processes receiving the resulting $f+1$ copies of the message relay it via
line 3, which yields $2f+1$ copies in total. The synchronizer then triggers
${\tt new\texttt{\textunderscore}view}(v+1)$ notifications at correct
processes that receive all these copies (line 3), causing them to enter $v+1$
without increasing their timeouts. One may think that this allows executions
in which only some correct processes keep increasing their timeouts until they
are high enough, whereas others are forever stuck with timeouts that are too
low, invalidating the premise of Lemma 5.2. The following lemma rules out such
scenarios and also trivially implies Lemma 5.2. It establishes that, in a
sufficiently high view $v$ with a correct leader, if the timeouts at a correct
process $p_{i}$ that enters $v$ are high enough, then this process cannot be
the first one to initiate a view change. Hence, for the protocol to enter
another view, some other process with lower timeouts must call ${\tt advance}$
and thus increase their durations (line 4).

###### Lemma 5.3.

Let $v\geq\mathcal{V}$ be such that $E_{\rm first}(v)\geq{\sf GST}$ and ${\sf
leader}(v)$ is correct, and consider a correct process $p_{i}$ that enters
$v$. If ${\sf dur\texttt{\textunderscore}recovery}_{i}(v)>6\delta$ and ${\sf
dur\texttt{\textunderscore}delivery}_{i}(v)>4\delta$ then $p_{i}$ is not the
first correct process to call ${\tt advance}$ in $v$.

Proof. Since $E_{\rm first}(v)\geq{\sf GST}$, messages sent by correct
processes after $E_{\rm first}(v)$ get delivered to all correct processes
within $\delta$ and process clocks track real time. By contradiction, assume
that $p_{i}$ is the first correct process to call ${\tt advance}$ in $v$. This
happens because a timer expires at $p_{i}$, and we now make a case split on
which timer it is. Here we only consider ${\sf
timer\texttt{\textunderscore}recovery}$ and handle ${\sf
timer\texttt{\textunderscore}delivery}$ in §C.2. A process starts ${\sf
timer\texttt{\textunderscore}recovery}$ when it enters the view $v$ (line 5),
and hence, at $E_{\rm first}(v)$ at the earliest (Figure 7). Because $p_{i}$
is the first correct process to call ${\tt advance}$ in $v$ and ${\sf
dur\texttt{\textunderscore}recovery}_{i}(v)>6\delta$, no correct process calls
${\tt advance}$ in $v$ until after $E_{\rm first}(v)+6\delta$. Then by Bounded
Entry all correct processes enter $v$ by $E_{\rm first}(v)+2\delta$. Also, by
Validity no correct process can enter $v+1$ until after $E_{\rm
first}(v)+6\delta$, and by Proposition 3.1 the same holds for any view $>v$.
Thus, all correct processes stay in $v$ at least until $E_{\rm
first}(v)+6\delta$.

When a correct process enters $v$, it sends a ${\tt
NEW\texttt{\textunderscore}LEADER}$ message to the leader of $v$, which
happens by $E_{\rm first}(v)+2\delta$. When the leader receives such messages
from a quorum of processes, it broadcasts a ${\tt
NEW\texttt{\textunderscore}STATE}$ message. Thus, by $E_{\rm
first}(v)+4\delta$ all correct processes receive this message and set ${\sf
status}=\textsc{normal}$. If at that point ${\sf
init\texttt{\textunderscore}log\texttt{\textunderscore}length}\leq{\sf
last\texttt{\textunderscore}delivered}$ at $p_{i}$, then the process stops
${\sf timer\texttt{\textunderscore}recovery}$ (line 5), which contradicts our
assumption. Hence, ${\sf
init\texttt{\textunderscore}log\texttt{\textunderscore}length}>{\sf
last\texttt{\textunderscore}delivered}$. When a correct process receives ${\tt
NEW\texttt{\textunderscore}STATE}$, it sends ${\tt PREPARE}$ messages for all
positions $\leq{\sf
init\texttt{\textunderscore}log\texttt{\textunderscore}length}$ (line 5). It
then takes the correct processes at most $2\delta$ to exchange the sequence of
${\tt PREPARE}$ and ${\tt COMMIT}$ messages that commits the values at all
positions $\leq{\sf
init\texttt{\textunderscore}log\texttt{\textunderscore}length}$. Thus, by
$E_{\rm first}(v)+6\delta$ the process $p_{i}$ commits and delivers all these
positions, stopping ${\sf timer\texttt{\textunderscore}recovery}$ (line 4).
This again contradicts our assumption.  $\sqcap$$\sqcup$

###### Theorem 5.4.

PBFT-light satisfies the Liveness property of Byzantine atomic broadcast.

Proof. Consider a valid value $x$ broadcast by a correct process. We first
prove that $x$ is eventually delivered by some correct process. Assume the
contrary. We now prove that in this case PBFT-light must keep switching views
forever. We do this analogously to Proposition 3.2 in §3: we use Lemma 5.1 to
show that correct processes keep calling ${\tt advance}$, and the Progress
property of the synchronizer to show that some of them will keep switching
views as a result.

Claim 1. Every view is entered by some correct process.

Proof. Since all correct processes call start (line 4), by Startup a correct
process eventually enters some view. We now show that correct processes keep
entering new views forever. Assume that this is false, so that there exists a
maximal view $v$ entered by any correct process. Let $P$ be any set of $f+1$
correct processes and consider an arbitrary process $p_{i}\in P$ that enters
$v$. The process that broadcast $x$ is correct, and thus keeps broadcasting
$x$ until the value is delivered (line 4). Since $x$ is never delivered,
$p_{i}$ is guaranteed to receive $x$ while in $v$. Then by Lemma 5.1, $p_{i}$
eventually calls ${\tt advance}$ while in $v$. Since $p_{i}$ was picked
arbitrarily, we have $\forall p_{i}\in
P.\,{E_{i}(v)\mathpunct{\downarrow}}{\implies}{A_{i}(v)\mathpunct{\downarrow}}$.
Then by Progress we get $E_{\rm first}(v+1)\mathpunct{\downarrow}$, which
yields a contradiction. Thus, correct processes keep entering views forever.
The claim then follows from Proposition 3.1 ensuring that, if a view is
entered by a correct process, then so are all preceding views.
$\sqcap$$\sqcup$

Let view $v_{1}$ be the first view such that $v_{1}\geq\mathcal{V}$ and
$E_{\rm first}(v_{1})\geq{\sf GST}$; such a view exists by Claim 1. The next
claim is needed to show that all correct processes will increase their
timeouts high enough to satisfy the bounds in Lemma 5.2.

Claim 2. Every correct process calls the timer expiration handler (line 4)
infinitely often.

Proof. Assume the contrary and let $C_{\rm fin}$ and $C_{\rm inf}$ be the sets
of correct processes that call the timer expiration handler finitely and
infinitely often, respectively. Then $C_{\rm fin}\not=\emptyset$, and by Claim
1 and Validity, $C_{\rm inf}\not=\emptyset$. The values of ${\sf
dur\texttt{\textunderscore}delivery}$ and ${\sf
dur\texttt{\textunderscore}recovery}$ increase unboundedly at processes from
$C_{\rm inf}$, and do not change after some view $v_{2}$ at processes from
$C_{\rm fin}$. By Claim 1 and since leaders rotate round-robin, there is a
view $v_{3}\geq\max\\{v_{2},v_{1}\\}$ with a correct leader such that any
process $p_{i}\in C_{\rm inf}$ that enters $v_{3}$ has ${\sf
dur\texttt{\textunderscore}delivery}_{i}(v_{3})>4\delta$ and ${\sf
dur\texttt{\textunderscore}recovery}_{i}(v_{3})>6\delta$. By Claim 1 and
Validity, at least one correct process calls ${\tt advance}$ in $v_{3}$; let
$p_{l}$ be the first process to do so. Since $v_{3}\geq v_{2}$, this process
cannot be in $C_{\rm fin}$ because none of these processes can increase their
timers in $v_{3}$. Then $p_{l}\in C_{\rm inf}$, contradicting Lemma 5.3.
$\sqcap$$\sqcup$

By Claims 1 and 2, there exists a view $v_{4}\geq v_{1}$ with a correct leader
such that some correct process enters $v_{4}$, and for any correct process
$p_{i}$ that enters $v_{4}$ we have ${\sf
dur\texttt{\textunderscore}delivery}_{i}(v_{4})>4\delta$ and ${\sf
dur\texttt{\textunderscore}recovery}_{i}(v_{4})>6\delta$. By Lemma 5.2, no
correct process calls ${\tt advance}$ in $v_{4}$. Then, by Validity, no
correct process enters $v_{4}+1$, which contradicts Claim 1. This
contradiction shows that $x$ must be delivered by a correct process. Then,
since the protocol reliably broadcasts committed values (line 4), all correct
processes will also eventually deliver $x$. From here the Liveness property
follows.  $\sqcap$$\sqcup$

##  6\. Latency Bounds for PBFT

Assume that PBFT-light is used with our SMR synchronizer in Figure 3. We now
quantify its latency using the bounds for the synchronizer in Theorem 3.3,
yielding the first detailed latency analysis for a PBFT-like protocol. Due to
space constraints we defer proofs to §C.3. To state our bounds, we assume the
existence of a known upper bound $\Delta$ on the maximum value of $\delta$ in
any execution (sync-hotstuff, ; pass-shi, ; HK89, ), so that we always have
$\delta<\Delta$. In practice, $\Delta$ provides a conservative estimate of the
message delay during synchronous periods, which may be much higher than the
maximal delay $\delta$ in a particular execution. We modify the protocol in
Figure 4 so that in lines 4-4 it does not increase ${\sf
dur\texttt{\textunderscore}recovery}$ and ${\sf
dur\texttt{\textunderscore}delivery}$ above $6\Delta$ and $4\Delta$,
respectively. This corresponds to the bounds in Lemma 5.2 and preserves the
protocol liveness. Finally, we assume that periodic handlers (line 3 in Figure
3 and line 4 in Figure 4) are executed every $\rho$ units of time, and that
the latency of reliable broadcast in line 4 under synchrony is
$\leq\delta+\rho$ (this corresponds to an implementation that just
periodically retransmits ${\tt DECISION}$ messages).

We quantify the latency of PBFT-light in both bad and good cases. For the bad
case we assume that the protocol starts during the asynchronous period. Given
a value $x$ broadcast before ${\sf GST}$, we quantify how quickly after ${\sf
GST}$ all correct processes deliver $x$. For simplicity, we assume that
timeouts are high enough at ${\sf GST}$ and that ${\sf leader}(\mathcal{V})$
is correct.

###### Theorem 6.1.

Assume that before ${\sf GST}$ all correct processes start executing the
protocol and one of them broadcasts $x$. Let $\mathcal{V}$ be defined as in
Theorem 3.3 and assume that ${\sf leader}(\mathcal{V})$ is correct and at
${\sf GST}$ each correct process has ${\sf
dur\texttt{\textunderscore}recovery}>6\delta$ and ${\sf
dur\texttt{\textunderscore}delivery}>4\delta$. Then all correct processes
deliver $x$ by ${\sf
GST}+\rho+\max\\{\rho+\delta,6\Delta\\}+4\Delta+\max\\{\rho,\delta\\}+7\delta$.

Although the latency bound looks complex, its main message is simple: PBFT-
light recovers after a period of asynchrony in bounded time. This time is
dominated by multiples of $\Delta$; without the assumption that ${\sf
leader}(\mathcal{V})$ is correct it would also be multiplied by $f$ due to
going over up to $f$ views with faulty leaders. To show the bound, we take
advantage of the latency guarantees of our synchronizer (Theorem 3.3). In more
detail, the bound has to account for an unfavorable scenario where the last
view $\mathcal{V}-1$ of the asynchronous period is not operational (e.g., not
all correct processes enter it). In this case, to deliver $x$ the protocol
first needs to bring all correct processes into the same view $\mathcal{V}$.
To bound the time required for that, we first use Property A to determine the
latest time when a correct process can enter $\mathcal{V}-1$: ${\sf
GST}+\rho+2\delta$. We then add the time such a process may spend in
$\mathcal{V}-1$ before it detects that $x$ is taking too long to get delivered
and call ${\tt advance}$: $\max\\{\rho+\delta,6\Delta\\}+4\Delta$, where
$6\Delta$ and $4\Delta$ come from the maximal timeout values. The first clause
of Property B then shows that all correct processes will enter $\mathcal{V}$
within an additional $\delta$, i.e., $E_{\rm last}(\mathcal{V})\leq{\sf
GST}+\rho+\max\\{\rho+\delta,6\Delta\\}+4\Delta+3\delta$. Finally, we add the
time for $x$ to be delivered in $\mathcal{V}$:
$\max\\{\rho,\delta\\}+4\delta$.

We now consider the case when the protocol starts during the synchronous
period, i.e., after ${\sf GST}$. The following theorem quantifies how quickly
all correct processes enter the first functional view, which in this case is
view $1$. If ${\sf leader}(1)$ is correct, it also quantifies how quickly a
broadcast value $x$ is delivered by all correct processes. The bound takes
into account the following optimization: in view $1$ the processes do not need
to exchange ${\tt NEW\texttt{\textunderscore}LEADER}$ messages. Then, after
the systems starts up, the protocol delivers values within $4\delta$, which
matches an existing lower bound of $3\delta$ for the delivery time starting
from the leader (ittai-good-case, ). The proof of the theorem exploits the
second clause of Property B.

###### Theorem 6.2.

Assume that all correct processes start the protocol after ${\sf GST}$ with
${\sf dur\texttt{\textunderscore}recovery}>5\delta$ and ${\sf
dur\texttt{\textunderscore}delivery}>4\delta$. Then the $\mathcal{V}$ defined
in Theorem 3.3 is equal to $1$ and $E_{\rm last}(1)\leq T_{\rm
last}(0)+\delta$. Furthermore, if a correct process broadcasts $x$ at
$t\geq{\sf GST}$ and ${\sf leader}(1)$ is correct, then all correct processes
deliver $x$ by $\max\\{t,T_{\rm last}(0)+\delta\\}+4\delta$.

##  7\. Additional Case Studies

To demonstrate the generality of the SMR synchronizer abstraction, we have
also used it to ensure the liveness of two other protocols. First, we handle a
variant of PBFT that periodically forces a leader change, as is common in
modern Byzantine SMR (aardvark, ; spinning, ; mirbft, ). In this protocol a
process calls ${\tt advance}$ not only when it suspects the current leader to
be faulty, but also when it delivers $B$ values proposed by this leader (for a
fixed $B$). This changes the censorship-resistance mechanism, which can now
exploit the fact that the protocol will keep encountering correct leaders.
Second, we have applied the SMR synchronizer to a variant of the above
protocol that follows the approach of HotStuff (hotstuff, ). The resulting
protocol adds an extra communication step to the normal path of PBFT in
exchange for reducing the communication complexity of leader change. Due to
space constraints, we defer the details about these two protocols to §D and
§E. Their liveness proofs follow the methodology we proposed for PBFT-light,
establishing analogs of Lemmas 5.1-5.3.

For PBFT with periodic leader rotation we have also established latency bounds
when using the synchronizer in Figure 3 (see §D). The most interesting one,
stated informally below, demonstrates the benefit of PBFT’s mechanism for
adapting timeouts to an unknown $\delta$: recall that in PBFT a process only
increases its timeouts when a timer expires, which means that the current view
does not operate normally (§4). The bound assumes that the protocol executes
during a synchronous period, all views up to $v$ operate normally, and the
leader of $v$ is faulty (for simplicity, just crashed). The bound then
quantifies how quickly the protocol switches to the next view $v+1$. Since in
PBFT processes do not increase timeouts in good views, they pay a minimal
latency penalty once they encounter a bad leader – the initial value of ${\sf
dur\texttt{\textunderscore}recovery}$. This contrasts with the simplistic way
of adapting the timeouts to an unknown $\delta$ by increasing them in every
view: in this case, as the protocol keeps changing views, the timeouts would
eventually increase up to the maximum (determined by $\Delta$), and the
protocol would have to wait that much to recover from a faulty leader.

###### Theorem 7.1 (informal).

Assume that all correct processes start executing PBFT with leader rotation
after ${\sf GST}$, and consider a view $v$ such that ${\sf leader}(v)$ is
initially crashed. Suppose that in each view $v^{\prime}<v$ all correct
processes deliver $B$ values proposed by the leader of this view. Then $E_{\rm
last}(v+1)\leq E_{\rm last}(v)+R+\delta$, where $R$ is the initial value of
${\sf dur\texttt{\textunderscore}recovery}$.

##  8\. Related Work and Discussion

#### Failure detectors.

Failure detectors and leader oracles (CT96, ; petr-survey, ) have been widely
used for implementing live consensus and SMR under benign failures (MR99, ;
GR04, ; R00, ). However, their implementations under Byzantine failures are
either impractical (kihlstrom, ) or detect only restricted failure types
(MR97, ; muteness, ; modular-smr, ; HK09, ). An alternative approach was
proposed in a textbook by Cachin et al. (cachin-book, ). This relies on a
leader-based Byzantine Epoch-Change (BEC) abstraction, which accepts
“complain” hints from the application to identify situations when the trust in
the current leader needs to be revoked. However, like the classical leader
oracles, BEC requires all correct processes to eventually trust the same well-
behaved leader, which is impossible to achieve in Byzantine settings333E.g., a
set of $\leq f$ correct processes complaining about the leader will not have
sufficient voting power to convince the remaining ones to stop trusting it..
In fact, the BEC-based Byzantine consensus algorithm in §5.6.4 of (cachin-
book, ) suffers from a liveness bug, which we describe in §F. The bug has been
confirmed with one of the textbook’s authors (cristian-personal, ).

Although our ${\tt advance}$ is similar to “complain”, we use it to implement
a weaker abstraction of an SMR synchronizer. We then obtain properties similar
to accuracy and completeness of failure detectors by carefully combining SMR-
level timers with uses of ${\tt advance}$ (Lemmas 5.1-5.2). Also, while
(cachin-book, ) does not specify constraints on the use of “complain” (see §F
for details), we give a complete characterization of ${\tt advance}$ and show
its sufficiency for solving SMR.

BFT-SMaRt (bftsmart, ; bftsmart-thesis, ) built on the ideas of (cachin-book,
) to propose an abstraction of validated and provable (VP) consensus, which
allows its clients to control leader changes. Although the overall BFT-SMaRt
protocol appears to be correct, its liveness proof sketch suffers from issues
with rigor similar to those of (cachin-book, ). In particular, the conditions
on how to change the leader in VP-Consensus to ensure its liveness were
underspecified (again, see §F).

#### Emulating synchrony.

Alternative abstractions avoid dependency on the specifics of a failure model
by simulating synchrony (Gaf98, ; heardof, ; KS06, ; heardof-bft, ). The first
such abstraction is due to Awerbuch (Awe85, ) who proposed a family of
synchronizer algorithms emulating a round-based synchronous system of top of
an asynchronous network with reliable communication and processes. The first
such emulation in a failure-prone partially synchronous system was introduced
in the DLS paper (dls, ). It relied on an expensive clock synchronization
protocol, which interleaved its messages with every step of a high-level
consensus algorithm implemented on top of it. Later work has proposed more
practical solutions, which reduce the synchronization frequency by relying on
either timers (cezara, ) or synchronized hardware clocks (ADDNR19, ;
indulgent1, ; indulgent2, ) (the latter can be obtained using one of the
existing fault-tolerant clock synchronization algorithms (SWL86, ; DHSS95, )).
However, the DLS model emulates communication-closed rounds, i.e., eventually,
a process in a round $r$ receives all messages sent by correct processes in
$r$. This property is needlessly strong for Byzantine consensus or SMR, since
protocols such as PBFT can make progress in a given view if they receive
messages from any quorum.

#### Consensus synchronizers.

To address the shortcoming of DLS rounds, recent work (NK20, ; bftlive, ;
hotstuff, ) proposed a more flexible abstraction (“consensus synchronizer” in
§3) that switches processes through an infinite series of views. In contrast
to rounds, each view may subsume multiple communication steps, and its
duration can either be fixed in advance (NK20, ) or grow dynamically (bftlive,
; hotstuff, ). Although consensus synchronizers can be used for efficient
single-shot Byzantine consensus (bftlive, ), using them for SMR results in
suboptimal implementations. A classical approach is to decide on each SMR
command using a separate black-box consensus instance (smr, ). However,
implementing the latter using a consensus synchronizer would force the
processes in every instance to iterate over the same sequence of potentially
bad views until the one with a correct leader and sufficiently long duration
could be reached. Although reusing good views across instances is possible,
this would require a non-trivial reconfiguration protocol to share their
parameters (tenderbake, ).

An alternative approach was proposed in HotStuff (hotstuff, ). This SMR
protocol is driven by a pacemaker, which keeps generating views similarly to a
consensus synchronizer. Within each view HotStuff runs a voting protocol that
commits a block of client commands in a growing hash chain. Although the
voting protocol can commit a block at wire speed (“optimistic
responsiveness”), committing the next block is delayed until the pacemaker
generates a new view, which increases latency. Furthermore, the cost the
pacemaker may incur to generate a view is paid for every single block.

#### SMR synchronizers.

In contrast to the above approaches, SMR synchronizers allow the application
to initiate view changes on demand via an ${\tt advance}$ call. As we show,
this affords SMR protocols the flexibility to judiciously manage their view
synchronization schedule: in particular, it prevents the timeouts from growing
unnecessarily (Theorem 7.1, §7) and avoids the overheads of further view
synchronizations once a stable view is reached (Lemma 5.2, §5).

The first synchronizer with a ${\tt new\texttt{\textunderscore}view}$/${\tt
advance}$ interface, which here we call an SMR synchronizer, was proposed by
Naor et al. (NK20, ; lumiere, ). They used it as an intermediate module in a
communication-efficient implementation of a consensus synchronizer. The latter
is sufficient to ensure the liveness of HotStuff (hotstuff, ) via either of
the two straightforward SMR constructions we described above. The
specification of the ${\tt new\texttt{\textunderscore}view}$/${\tt advance}$
module of Naor et al. was only used as a stepping stone in the proof of their
consensus synchronizer, and as a result, is more low-level and complex than
our SMR synchronizer specification. Naor et al. did not investigate the
usability of the SMR synchronizer abstraction as a generic building block
applicable to a wide range of Byzantine SMR protocols – a gap we fill in this
paper. Finally, they only handled a simplified version of partial synchrony
where messages are never lost and $\delta$ is known a priori, whereas our SMR
synchronizer implementation handles partial synchrony in its full generality.
This implementation builds on the consensus synchronizer of Bravo et al.
(bftlive, ). However, its correctness proof and performance analysis are more
intricate, since the timing of the view switches is not fixed a priori, but
driven by external ${\tt advance}$ inputs.

The algorithms we consider are deterministic. An interesting direction for
future research is to adapt SMR synchronizers to emulate asynchronous rounds,
as required by randomized consensus algorithms (random-benor, ; random-bracha,
; random-saia, ; random-cachin, ).

#### SMR liveness proofs.

PBFT (pbft, ; castro-thesis, ; castro-tocs, ) is a seminal protocol whose
design choices have been widely adopted (zyzzyva, ; aardvark, ; spinning, ;
mirbft, ; sbft, ). To the best of our knowledge, our proof in §5 is the first
one to formally establish its liveness. An informal argument given in (castro-
tocs, , §4.5.1) mainly justifies liveness assuming all correct processes enter
a view with a correct leader and stay in that view for sufficiently long. It
does not rigorously justify why such a view will be eventually reached, and in
particular, how this is ensured by the interplay between SMR-level timeout
management and view synchronization (§5). Liveness mechanisms were also
omitted from the formal specification of PBFT by an I/O-automaton (castro-
tocs, ; castro-thesis, ).

Bravo et al. (bftlive, ) have applied consensus synchronizers to several
consensus protocols, including a single-shot version of PBFT. These protocols
and their proofs and are much more straightforward than the full SMR protocols
we consider here. In particular, since a consensus synchronizer keeps
switching processes between views regardless of whether their leaders are
correct, the proof of the single-shot PBFT in (bftlive, ) does not need to
establish analogs of completeness and accuracy (Lemmas 5.1 and 5.2) or deal
with the fact that processes may disagree on timeout durations (Lemma 5.3).

Byzantine SMR protocols often integrate the view synchronization mechanism
into the core protocol, which enables white-box optimizations (tendermint-
arxiv, ; libra, ; pbft, ; ittai-fast-path, ). Our work does not rule out this
approach, but provides a way to make it more systematic: we can first develop
efficient mechanisms for view synchronization independently from SMR protocols
and do white-box optimizations afterwards, if needed. Overall, our
synchronizer specification and the analysis of PBFT provide a blueprint for
designing provably live and efficient Byzantine SMR protocols.

## References

  * [1] DiemBFT v4: State machine replication in the Diem blockchain.
https://developers.diem.com/papers/diem-consensus-state-machine-replication-
in-the-diem-blockchain/2021-08-17.pdf.

  * [2] Incorrect by construction-CBC Casper isn’t live.  https://derekhsorensen.com/docs/CBC_Casper_Flaw.pdf.
  * [3] I. Abraham, S. Devadas, D. Dolev, K. Nayak, and L. Ren.  Synchronous Byzantine agreement with expected ${O}(1)$ rounds, expected ${O}(n^{2})$ communication, and optimal resilience.  In Conference on Financial Cryptography and Data Security (FC), 2019\.
  * [4] I. Abraham, G. Gueta, D. Malkhi, L. Alvisi, R. Kotla, and J. Martin.  Revisiting fast practical Byzantine fault tolerance.  arXiv, abs/1712.01367, 2017.
  * [5] I. Abraham, D. Malkhi, K. Nayak, L. Ren, and M. Yin.  Sync HotStuff: Simple and practical synchronous state machine replication.  In Symposium on Security and Privacy (SP), 2020.
  * [6] I. Abraham, D. Malkhi, and A. Spiegelman.  Asymptotically optimal validated asynchronous Byzantine agreement.  In Symposium on Principles of Distributed Computing (PODC), 2019\.
  * [7] I. Abraham, K. Nayak, L. Ren, and Z. Xiang.  Brief note: Fast authenticated Byzantine consensus.  CoRR, abs/2102.07932, 2021.
  * [8] I. Abraham, K. Nayak, L. Ren, and Z. Xiang.  Good-case latency of Byzantine broadcast: a complete categorization.  In Symposium on Principles of Distributed Computing (PODC), 2021\.
  * [9] L. Aştefănoaei, P. Chambart, A. Del Pozzo, T. Rieutord, S. Tucci-Piergiovanni, and E. Zălinescu.  Tenderbake - a solution to dynamic repeated consensus for blockchains.  In Symposium on Foundations and Applications of Blockchain (FAB), 2021.
  * [10] D. Alistarh, S. Gilbert, R. Guerraoui, and C. Travers.  Generating fast indulgent algorithms.  In International Conference on Distributed Computing and Networking (ICDCN), 2011.
  * [11] Y. Amoussou-Guenou, A. D. Pozzo, M. Potop-Butucaru, and S. Tucci-Piergiovanni.  Correctness of Tendermint-core blockchains.  In Conference on Principles of Distributed Systems (OPODIS), 2018\.
  * [12] B. Awerbuch.  Complexity of network synchronization.  J. ACM, 32(4):804–823, 1985.
  * [13] R. A. Bazzi and Y. Ding.  Non-skipping timestamps for Byzantine data storage systems.  In Symposium on Distributed Computing (DISC), 2004.
  * [14] M. Ben-Or.  Another advantage of free choice (extended abstract): Completely asynchronous agreement protocols.  In Symposium on Principles of Distributed Computing (PODC), 1983\.
  * [15] C. Berger, H. P. Reiser, and A. Bessani.  Making reads in BFT state machine replication fast, linearizable, and live.  In Symposium on Reliable Distributed Systems (SRDS), 2021.
  * [16] A. N. Bessani, J. Sousa, and E. A. P. Alchieri.  State machine replication for the masses with BFT-SMART.  In Conference on Dependable Systems and Networks (DSN), 2014.
  * [17] M. Biely, J. Widder, B. Charron-Bost, A. Gaillard, M. Hutle, and A. Schiper.  Tolerating corrupted communication.  In Symposium on Principles of Distributed Computing (PODC), 2007\.
  * [18] G. Bracha.  Asynchronous Byzantine agreement protocols.  Inf. Comput., 75(2):130–143, 1987.
  * [19] M. Bravo, G. Chockler, and A. Gotsman.  Making Byzantine consensus live.  In Symposium on Distributed Computing (DISC), 2020.
  * [20] E. Buchman, J. Kwon, and Z. Milosevic.  The latest gossip on BFT consensus.  arXiv, abs/1807.04938, 2018.
  * [21] C. Cachin.  Personal communication.  2022\.
  * [22] C. Cachin, R. Guerraoui, and L. E. T. Rodrigues.  Introduction to Reliable and Secure Distributed Programming (2 ed.).  Springer, 2011.
  * [23] C. Cachin, K. Kursawe, F. Petzold, and V. Shoup.  Secure and efficient asynchronous broadcast protocols.  In International Cryptology Conference (CRYPTO), 2001.
  * [24] C. Cachin, K. Kursawe, and V. Shoup.  Random oracles in Constantinople: Practical asynchronous Byzantine agreement using cryptography.  J. Cryptol., 18(3):219–246, 2005.
  * [25] C. Cachin and M. Vukolić.  Blockchain consensus protocols in the wild (keynote talk).  In Symposium on Distributed Computing (DISC), 2017.
  * [26] M. Castro.  Practical Byzantine Fault Tolerance.  PhD thesis, Massachusetts Institute of Technology, 2001.
  * [27] M. Castro and B. Liskov.  Practical Byzantine fault tolerance.  In Symposium on Operating Systems Design and Implementation (OSDI), 1999.
  * [28] M. Castro and B. Liskov.  Practical Byzantine fault tolerance and proactive recovery.  ACM Transactions on Computer Systems, 20(4):398–461, 2002.
  * [29] T. D. Chandra and S. Toueg.  Unreliable failure detectors for reliable distributed systems.  J. ACM, 43(2):225–267, 1996.
  * [30] B. Charron-Bost and A. Schiper.  The Heard-Of model: computing in distributed systems with benign faults.  Distributed Comput., 22(1):49–71, 2009.
  * [31] A. Clement, E. Wong, L. Alvisi, M. Dahlin, and M. Marchetti.  Making Byzantine fault tolerant systems tolerate Byzantine faults.  In Symposium on Networked Systems Design and Implementation (NSDI), 2009.
  * [32] D. Dolev, J. Y. Halpern, B. Simons, and R. Strong.  Dynamic fault-tolerant clock synchronization.  J. ACM, 42(1):143–185, 1995.
  * [33] A. Doudou, B. Garbinato, and R. Guerraoui.  Abstractions for devising Byzantine-resilient state machine replication.  In Symposium on Reliable Distributed Systems (SRDS), 2000.
  * [34] A. Doudou, B. Garbinato, R. Guerraoui, and A. Schiper.  Muteness failure detectors: Specification and implementation.  In European Dependable Computing Conference (EDCC), 1999.
  * [35] C. Dragoi, J. Widder, and D. Zufferey.  Programming at the edge of synchrony.  Proc. ACM Program. Lang., 4(OOPSLA), 2020.
  * [36] C. Dwork, N. A. Lynch, and L. J. Stockmeyer.  Consensus in the presence of partial synchrony.  J. ACM, 35(2):288–323, 1988.
  * [37] M. J. Fischer, N. A. Lynch, and M. Paterson.  Impossibility of distributed consensus with one faulty process.  J. ACM, 32(2):374–382, 1985.
  * [38] F. C. Freiling, R. Guerraoui, and P. Kuznetsov.  The failure detector abstraction.  ACM Comput. Surv., 43(2):9:1–9:40, 2011.
  * [39] E. Gafni.  Round-by-round fault detectors: Unifying synchrony and asynchrony.  In Symposium on Principles of Distributed Computing (PODC), 1998\.
  * [40] S. Gilbert, R. Guerraoui, and D. R. Kowalski.  On the message complexity of indulgent consensus.  In Symposium on Distributed Computing (DISC), 2007.
  * [41] G. Golan-Gueta, I. Abraham, S. Grossman, D. Malkhi, B. Pinkas, M. K. Reiter, D. Seredinschi, O. Tamir, and A. Tomescu.  SBFT: A scalable and decentralized trust infrastructure.  In Conference on Dependable Systems and Networks (DSN), 2019.
  * [42] R. Guerraoui.  Indulgent algorithms (preliminary version).  In Symposium on Principles of Distributed Computing (PODC), 2000\.
  * [43] R. Guerraoui and M. Raynal.  The information structure of indulgent consensus.  IEEE Transactions on Computers, 53(4):453–466, 2004.
  * [44] A. Haeberlen and P. Kuznetsov.  The fault detection problem.  In Conference on Principles of Distributed Systems (OPODIS), 2009\.
  * [45] A. Herzberg and S. Kutten.  Fast isolation of arbitrary forwarding faults.  In Symposium on Principles of Distributed Computing (PODC), 1989\.
  * [46] I. Keidar and A. Shraer.  Timeliness, failure-detectors, and consensus performance.  In Symposium on Principles of Distributed Computing (PODC), 2006\.
  * [47] K. P. Kihlstrom, L. E. Moser, and P. M. Melliar-Smith.  Byzantine fault detectors for solving consensus.  The Computer Journal, 46(1):16–35, 2003.
  * [48] V. King and J. Saia.  Byzantine agreement in expected polynomial time.  J. ACM, 63(2):13:1–13:21, 2016.
  * [49] R. Kotla, L. Alvisi, M. Dahlin, A. Clement, and E. Wong.  Zyzzyva: Speculative Byzantine fault tolerance.  ACM Trans. Comput. Syst., 27(4):7:1–7:39, 2010.
  * [50] L. Lamport.  The part-time parliament.  ACM Trans. Comput. Syst., 16(2):133–169, 1998.
  * [51] D. Malkhi and M. Reiter.  Unreliable intrusion detection in distributed computations.  In Workshop on Computer Security Foundations (CSFW), 1997.
  * [52] A. Mostéfaoui and M. Raynal.  Solving consensus using Chandra-Toueg’s unreliable failure detectors: A general quorum-based approach.  In Symposium on Distributed Computing (DISC), 1999.
  * [53] O. Naor, M. Baudet, D. Malkhi, and A. Spiegelman.  Cogsworth: Byzantine view synchronization.  In Cryptoeconomics Systems Conference (CES), 2020.
  * [54] O. Naor and I. Keidar.  Expected linear round synchronization: The missing link for linear Byzantine SMR.  In Symposium on Distributed Computing (DISC), 2020.
  * [55] R. Pass and E. Shi.  Hybrid consensus: Efficient consensus in the permissionless model.  In Symposium on Distributed Computing (DISC), 2017.
  * [56] F. B. Schneider.  Implementing fault-tolerant services using the state machine approach: A tutorial.  ACM Comput. Surv., 22(4):299–319, 1990.
  * [57] B. Simons, J. Welch, and N. Lynch.  An overview of clock synchronization.  In Fault-Tolerant Distributed Computing, 1986.
  * [58] J. Sousa.  Byzantine State Machine Replication for the Masses.  PhD thesis, University of Lisbon, 2017.
  * [59] C. Stathakopoulou, T. David, and M. Vukolić.  Mir-BFT: High-throughput BFT for blockchains.  CoRR, abs/1906.05552, 2019.
  * [60] G. S. Veronese, M. Correia, A. N. Bessani, and L. C. Lung.  Spin one’s wheels? Byzantine fault tolerance with a spinning primary.  In Symposium on Reliable Distributed Systems (SRDS), 2009.
  * [61] M. Yin, D. Malkhi, M. K. Reiter, G. Golan-Gueta, and I. Abraham.  HotStuff: BFT consensus with linearity and responsiveness.  In Symposium on Principles of Distributed Computing (PODC), 2019\.

##  Appendix A Constructing a Consensus Synchronizer from an SMR Synchronizer

1

2function start()

3 advance();

4

5

6upon ${\tt new\texttt{\textunderscore}view}(v)$

7 ${\tt stop\texttt{\textunderscore}timer}({\sf
timer\texttt{\textunderscore}view})$;

8 ${\tt start\texttt{\textunderscore}timer}({\sf
timer\texttt{\textunderscore}view},F(v))$;

9 trigger ${\tt
new\texttt{\textunderscore}consensus\texttt{\textunderscore}view}(v)$;

10

11

12

13when timer_view expires

14 advance();

15

Figure 8. A consensus synchronizer from an SMR synchronizer.

  1. I.

$\forall
i,v,v^{\prime}.\,{\mathbb{E}_{i}(v)\mathpunct{\downarrow}}\wedge{\mathbb{E}_{i}(v^{\prime})\mathpunct{\downarrow}}{\implies}(v<v^{\prime}{\iff}\mathbb{E}_{i}(v)<\mathbb{E}_{i}(v^{\prime}))$

  2. II.

$\mathbb{E}_{\rm first}(\mathcal{V})\geq{\sf GST}$

  3. III.

$\forall i.\,\forall
v\geq\mathcal{V}.\,p_{i}\in\mathcal{C}{\implies}{\mathbb{E}_{i}(v)\mathpunct{\downarrow}}$

  4. IV.

$\forall v\geq\mathcal{V}.\,\mathbb{E}_{\rm last}(v)\leq\mathbb{E}_{\rm
first}(v)+d$

  5. V.

$\forall v\geq\mathcal{V}.\,\mathbb{E}_{\rm first}(v+1)>\mathbb{E}_{\rm
first}(v)+F(v)$

Figure 9. Consensus synchronizer specification [19], holding for some
$\mathcal{V}\in{\sf View}$.

A consensus synchronizer produces a stream of notifications ${\tt
new\texttt{\textunderscore}consensus\texttt{\textunderscore}view}(v)$ at each
correct process, telling it to enter a view $v$. A process can ensure that the
synchronizer has started operating by calling a special ${\tt start}()$
function. We assume that each correct process eventually calls ${\tt
start}()$, unless it gets a ${\tt
new\texttt{\textunderscore}consensus\texttt{\textunderscore}view}$
notification first. For a consensus protocol to terminate, its processes need
to stay in the same view for long enough to complete the message exchange
leading to a decision. Since the message delay $\delta$ after ${\sf GST}$ is
unknown to the protocol, we need to increase the view duration until it is
long enough for the protocol to terminate. To this end, the synchronizer is
parameterized by a function defining this duration – $F:{\sf
View}\cup\\{0\\}\to{\sf Time}$, which is monotone, satisfies $F(0)=0$, and
increases unboundedly:

(1) $\forall\theta.\,\exists v.\,\forall v^{\prime}.\,v^{\prime}\geq v\implies
F(v^{\prime})>\theta.$

Figure 8 shows how we can construct a consensus synchronizer from an SMR
synchronizer. Upon a ${\tt start}()$ call, the consensus synchronizer just
tells the underlying SMR synchronizer to advance (line 8). When the SMR
synchronizer tells the process to enter a view $v$ (line 8), the consensus
synchronizer produces the corresponding ${\tt
new\texttt{\textunderscore}consensus\texttt{\textunderscore}view}(v)$
notification. It also sets a timer ${\sf timer\texttt{\textunderscore}view}$
for the duration $F(v)$. When the timer expires (line 8), the consensus
synchronizer tells the SMR synchronizer to advance.

Figure 9 presents the specification of a consensus synchronizer proposed in
[19]. This relies on the following notation, analogous to the one used for SMR
synchronizers. Given a view $v$ for which a correct process $p_{i}$ received a
${\tt new\texttt{\textunderscore}consensus\texttt{\textunderscore}view}(v)$
notification, we denote by $\mathbb{E}_{i}(v)$ the time when this happens; we
let $\mathbb{E}_{\rm first}(v)$ and $\mathbb{E}_{\rm last}(v)$ denote
respectively the earliest and the latest time when some correct process
receives a ${\tt
new\texttt{\textunderscore}consensus\texttt{\textunderscore}view}(v)$
notification. Like an SMR synchronizer, a consensus synchronizer must
guarantee that views only increase at a given process (Property I). A
consensus synchronizer ensures view synchronization only starting from some
view $\mathcal{V}$, entered after ${\sf GST}$ (Property II). Starting from
$\mathcal{V}$, correct processes do not skip any views (Property III), enter
each view $v\geq\mathcal{V}$ within at most $d$ of each other (Property IV)
and stay there for a determined amount of time: until $F(v)$ after the first
process enters $v$ (Property V). We next prove the following theorem, showing
that the consensus synchronizer in Figure 8 satisfies these properties.

###### Theorem A.1.

The consensus synchronizer in Figure 8 satisfies Properties I-V in Figure 9,
provided the SMR synchronizer it uses satisfies the properties in Figure 1.

The implementation in Figure 8 ensures the following proposition, which we
tacitly use in our proof.

###### Proposition A.2.

$\forall i,v.\,\mathbb{E}_{i}(v)=E_{i}(v)$.

###### Proposition A.3.

$\forall v.\,\exists v^{\prime}.\,v^{\prime}>v\wedge{\mathbb{E}_{\rm
first}(v^{\prime})\mathpunct{\downarrow}}$.

Proof. Analogous to Proposition 3.2.  $\sqcap$$\sqcup$

###### Lemma A.4.

If a correct process enters a view $v>0$ and $E_{\rm first}(v)\geq{\sf GST}$,
then for all $v^{\prime}>v$, no correct process attempts to advance from
$v^{\prime}-1$ before $E_{\rm first}(v)+F(v)$.

Proof. Suppose by contradiction that there exists a time $t^{\prime}<E_{\rm
first}(v)+F(v)$ and a correct process $p_{i}$ such that $p_{i}$ attempts to
advance from $v^{\prime}-1>v-1$ at $t^{\prime}$. Since $v^{\prime}\geq v+1>1$,
at $t^{\prime}$ the process $p_{i}$ executes the handler at line 8 and the
last view it entered is $v^{\prime}-1$. Since $p_{i}.{\sf
timer\texttt{\textunderscore}view}$ is not enabled at $t^{\prime}$, $p_{i}$
must have entered $v^{\prime}-1$ at least $F(v)$ before $t^{\prime}$ according
to its local clock. Since $v^{\prime}-1\geq v$, by Proposition 3.1, we have
$E_{\rm first}(v^{\prime}-1)\geq E_{\rm first}(v)\geq{\sf GST}$. Therefore,
given that the clocks of all correct processes progress at the same rate as
real time after ${\sf GST}$, we get

$E_{\rm first}(v)\leq E_{\rm first}(v^{\prime}-1)\leq
t^{\prime}-F(v^{\prime}-1).$

Hence,

$t^{\prime}\geq E_{\rm first}(v)+F(v^{\prime}-1).$

Since $F$ is non-decreasing and $v^{\prime}-1\geq v$, we have
$F(v^{\prime}-1)\geq F(v)$, so that

$t^{\prime}\geq E_{\rm first}(v)+F(v),$

which contradicts our assumption that $t^{\prime}<E_{\rm first}(v)+F(v)$. This
contradiction shows the required.  $\sqcap$$\sqcup$

#### Proof of Theorem A.1.

Property I follows from Monotonicity of the SMR synchronizer. Let
$\mathcal{V}$ be the view from Bounded Entry and let $\mathcal{V}^{\prime}$ be
the minimal view such that $\mathcal{V}^{\prime}\geq\mathcal{V}$, $E_{\rm
first}(\mathcal{V}^{\prime})\geq{\sf GST}$ and $F(\mathcal{V}^{\prime})\geq
2\delta$. Such a view exists by (1) and Proposition A.3. Then Property II
holds for $\mathcal{V}=\mathcal{V}^{\prime}$. By Propositions 3.1 and A.3, a
correct process enters every view $v\geq\mathcal{V}^{\prime}$. By Proposition
3.1, $v\geq\mathcal{V}^{\prime}$ implies

(2) $E_{\rm first}(v)\geq E_{\rm first}(\mathcal{V}^{\prime})\geq{\sf GST}.$

Since $F$ is a non-decreasing function, $F(v)\geq 2\delta$. Thus, by Lemma A.4
and Bounded Entry, all correct processes enter $v$, and $E_{\rm last}(v)\leq
E_{\rm first}(v)+2\delta$, which validates Properties III and IV for
$\mathcal{V}=\mathcal{V}^{\prime}$. To prove Property V, fix a view
$v\geq\mathcal{V}^{\prime}$. Since a correct process enters view $v+1$, by
Validity, there exist a time $t<E_{\rm first}(v+1)$ at which some correct
process attempts to advance from $v$. By (2), $E_{\rm first}(v)\geq{\sf GST}$.
Then by Lemma A.4 we get $t\geq E_{\rm first}(v)+F(v)$, so that $E_{\rm
first}(v+1)>t\geq E_{\rm first}(v)+F(v)$, as required.  $\sqcap$$\sqcup$

##  Appendix B Correctness and Performance of the Synchronizer Algorithm

###  B.1. Proof of the Synchronizer Correctness

The local view of a process $p_{i}$ at time $t$, denoted ${\sf LV}_{i}(t)$, is
the latest view entered by $p_{i}$ at or before $t$, or $0$ if $p_{i}$ has not
entered any views by then.

###### Lemma B.1.

For all $t$ and $v\geq 0$, if a correct process sends ${\tt WISH}(v+1)$ at
$t$, then there exists a time $t^{\prime}\leq t$ such that some correct
process attempts to advance from $v$ at $t^{\prime}$.

Proof. We first prove the following auxiliary proposition:

(3) $\forall p_{i}.\,\forall v.\,p_{i}\text{~{}is~{}correct}\wedge
p_{i}\text{~{}sends~{}}{\tt WISH}(v+1)\text{~{}at~{}}t\implies\\\ \exists
t^{\prime}\leq t.\,\exists v^{\prime}\geq v.\,\exists
p_{j}.\,p_{j}\text{~{}is~{}correct}\wedge
p_{j}\text{~{}attempts~{}to~{}advance~{}from~{}}v^{\prime}\text{~{}at~{}}t^{\prime}.$

By contradiction, assume that a correct process $p_{i}$ sends ${\tt
WISH}(v+1)$ at $t$, but for all $t^{\prime}\leq t$ and all $v^{\prime}\geq v$,
no correct process attempts to advance from $v^{\prime}$ at $t^{\prime}$.
Consider the earliest time $t_{k}$ when some correct process $p_{k}$ sends a
${\tt WISH}(v_{k})$ with $v_{k}\geq v+1$, so that $t_{k}\leq t$.

Since $p_{k}$ sends ${\tt WISH}(v_{k})$ at $t_{k}$, either $v_{k}=p_{k}.{\sf
view}^{+}(t_{k})$ or $p_{k}.{\sf view}(t_{k})=p_{k}.{\sf
view}^{+}(t_{k})=v_{k}-1$, and in the latter case $p_{k}$ executes either line
3 or line 3. If $p_{k}.{\sf view}^{+}(t_{k})=v_{k}\geq v+1$, then $p_{k}.{\sf
max\texttt{\textunderscore}views}(t_{k})$ includes $f+1$ entries $\geq
v_{k}\geq v+1$, and therefore, there exists a correct process $p_{l}$ that
sent ${\tt WISH}(v^{\prime})$ with $v^{\prime}\geq v+1$ at $t_{l}<t_{k}$,
contradicting the assumption that $t_{k}$ is the earliest time when this can
happen. Suppose that $p_{k}.{\sf view}(t_{k})=p_{k}.{\sf
view}^{+}(t_{k})=v_{k}-1$ and at $t_{k}$, $p_{k}$ executes either line 3 or
line 3. Then ${\sf LV}_{k}(t_{k})=v_{k}-1$. If $p_{k}$ executes line 3 at
$t_{k}$, then since ${\sf LV}_{k}(t_{k})=v_{k}-1$, $p_{k}$ attempts to advance
from $v_{k}-1\geq v$ at $t_{k}\leq t$, contradicting our assumption that no
such attempt can occur. Suppose now that $p_{k}$ executes the code in line 3
at $t_{k}$. If $v_{k}>1$, then since $p_{k}.{\sf view}(t_{k})=p_{k}.{\sf
view}^{+}(t_{k})=v_{k}-1$, we know that $E_{k}(v_{k}-1)$ is defined and
satisfies $E_{k}(v_{k}-1)<t_{k}$. Let $t^{\prime}_{k}=E_{k}(v_{k}-1)$ if
$v_{k}>1$, and $t^{\prime}_{k}=0$ otherwise. Then $p_{k}.{\sf
view}(t^{\prime}_{k})=p_{k}.{\sf view}^{+}(t^{\prime}_{k})=v_{k}-1$ and
$p_{k}.{\sf advanced}(t^{\prime}_{k})=\text{\sc false}$. Since $p_{k}.{\sf
advanced}(t_{k})=\text{\sc true}$, there exists a time $t^{\prime\prime}_{k}$
such that $t^{\prime}_{k}<t^{\prime\prime}_{k}\leq t_{k}$ and $p_{k}$ calls
${\tt advance}()$ at $t^{\prime\prime}_{k}$. Since both $p_{k}.{\sf view}$ and
$p_{k}.{\sf view}^{+}$ are non-decreasing, and both are equal to $v_{k}-1$ at
$t^{\prime\prime}_{k}$ as well as $t_{k}$, $p_{k}.{\sf
view}(t^{\prime\prime}_{k})=p_{k}.{\sf
view}^{+}(t^{\prime\prime}_{k})=v_{k}-1$. Thus, ${\sf
LV}_{k}(t^{\prime\prime}_{k})=v_{k}-1$, which implies that at
$t^{\prime\prime}_{k}<t_{k}\leq t$, $p_{k}$ attempts to advance from
$v_{k}-1\geq v$, contradicting our assumption that no such attempt can happen.
Thus, (3) holds.

We now prove the lemma. Let $t$ and $v$ be such that some correct process
sends ${\tt WISH}(v+1)$ at $t$. By (3), there exists a correct process that
attempts to advance from a view $\geq v$ at or before $t$. Let $t^{\prime}$ be
the earliest time when some correct process attempts to advance from a view
$\geq v$, and let $p_{j}$ be this process and $v^{\prime}\geq v$ be the view
from which $p_{j}$ attempts to advance at $t^{\prime}$. Thus, at $t^{\prime}$,
$p_{j}$ executes the code in line 3 and ${\sf
LV}_{j}(t^{\prime})=v^{\prime}\geq v$. Hence, there exists an earlier time at
which $p_{j}.{\sf view}^{+}=p_{j}.{\sf view}=v^{\prime}$. Since $p_{j}.{\sf
view}^{+}$ is non-decreasing, $p_{j}.{\sf view}^{+}(t^{\prime})\geq
v^{\prime}$. If $p_{j}.{\sf view}^{+}(t^{\prime})>v^{\prime}$, then given that
$v^{\prime}\geq v$, $p_{j}.{\sf view}^{+}(t^{\prime})\geq v+1$. Thus, there
exists a correct process $p_{k}$ and time $t^{\prime\prime}<t^{\prime}$ such
that $p_{k}$ sent ${\tt WISH}(v^{\prime\prime})$ with $v^{\prime\prime}\geq
v+1$ to $p_{j}$ at $t^{\prime\prime}$. By (3), there exists a time $\leq
t^{\prime\prime}<t^{\prime}$ at which some correct process attempts to advance
from a view $\geq v^{\prime\prime}-1\geq v$, which is impossible. Thus,
$p_{j}.{\sf view}^{+}(t^{\prime})=v^{\prime}$. Since ${\sf
LV}_{j}(t^{\prime})=v^{\prime}$, we have $p_{j}.{\sf
view}(t^{\prime})=p_{j}.{\sf view}^{+}(t^{\prime})=v^{\prime}\geq v$. By the
definitions of ${\sf view}$ and ${\sf view}^{+}$, $v^{\prime}$ is both the
lowest view among the highest $2f+1$ views in $p_{j}.{\sf
max\texttt{\textunderscore}views}(t^{\prime})$, and the lowest view among the
highest $f+1$ views in $p_{j}.{\sf
max\texttt{\textunderscore}views}(t^{\prime})$. Hence, $p_{j}.{\sf
max\texttt{\textunderscore}views}(t^{\prime})$ includes $f+1$ entries equal to
$v^{\prime}$, and therefore, there exists a correct process $p_{k}$ such that

(4) $p_{j}.{\sf view}(t^{\prime})=p_{j}.{\sf view}^{+}(t^{\prime})=p_{j}.{\sf
max\texttt{\textunderscore}views}[k](t^{\prime})=v^{\prime}\geq v-1.$

Also, for all correct processes $p_{l}$, $p_{j}.{\sf
max\texttt{\textunderscore}views}[l](t^{\prime})<v+1$: otherwise, some correct
process sent ${\tt WISH}(v^{\prime\prime})$ with $v^{\prime\prime}\geq v+1$ at
$t^{\prime\prime}<t^{\prime}$, and therefore, by (3), some correct process
attempted to advance from a view $\geq v$ earlier than $t^{\prime}$, which is
impossible. Thus,

$p_{j}.{\sf view}(t^{\prime})=p_{j}.{\sf view}^{+}(t^{\prime})=p_{j}.{\sf
max\texttt{\textunderscore}views}[k](t^{\prime})<v+1.$

Together with (4), this implies

$p_{j}.{\sf view}(t^{\prime})=p_{j}.{\sf view}^{+}(t^{\prime})=v.$

Hence, ${\sf LV}_{j}(t^{\prime})=v$, and therefore, $p_{j}$ attempts to
advance from $v$ at $t^{\prime}$. Thus, $v^{\prime}=v$ and $t^{\prime}\leq t$,
as required.  $\sqcap$$\sqcup$

###### Lemma B.2.

Validity holds: $\forall
i,v.\,{E_{i}(v+1)\mathpunct{\downarrow}}{\implies}{A_{\rm
first}(v)\mathpunct{\downarrow}}\wedge A_{\rm first}(v)<E_{i}(v+1)$.

Proof. Since $p_{i}$ enters a view $v+1$, we have $p_{i}.{\sf
view}(E_{i}(v+1))=p_{i}.{\sf view}^{+}(E_{i}(v+1))=v+1$. By the definitions of
${\sf view}$ and ${\sf view}^{+}$, $v+1$ is both the lowest view among the
highest $2f+1$ views in $p_{i}.{\sf
max\texttt{\textunderscore}views}(E_{i}(v+1))$, and the lowest view among the
highest $f+1$ views in $p_{i}.{\sf
max\texttt{\textunderscore}views}(E_{i}(v+1))$. Hence, $p_{i}.{\sf
max\texttt{\textunderscore}views}(E_{i}(v+1))$ includes $f+1$ entries equal to
$v+1$. Then there exists a time $t^{\prime}<E_{i}(v+1)$ at which some correct
process sends ${\tt WISH}(v+1)$. Hence, by Lemma B.1, there exists a time
$t\leq t^{\prime}<E_{i}(v+1)$ at which some correct process attempts to
advance from $v$.  $\sqcap$$\sqcup$

###### Lemma B.3.

For all times $t$ and views $v>0$, if a correct process sends ${\tt WISH}(v)$
at $t$, then there exists a time $t^{\prime}\leq t$ such that some correct
process attempts to advance from view $0$ at $t^{\prime}$.

Proof. Consider the earliest time $t_{k}\leq t$ at which some correct process
$p_{k}$ sends ${\tt WISH}(v_{k})$ for some view $v_{k}$. By Lemma B.1, there
exists a time $t_{j}\leq t_{k}$ at which some correct process attempts to
advance from $v_{k}-1\geq 0$, and therefore, sends ${\tt WISH}(v_{k})$ at
$t_{j}$. Since $t_{k}$ is the earliest time when this could happen, we have
$t_{j}=t_{k}$. Also, if $v_{k}-1>0$, then $E_{k}(v_{k}-1)$ is defined, and
hence, by Lemma B.2, some correct process attempts to advance from $v_{k}-2$
by sending ${\tt WISH}(v_{k}-1)$ earlier than $t_{j}=t_{k}$, which cannot
happen. Thus, $v_{k}=1$ and at $t_{k}$, $p_{k}$ attempts to advance from $0$,
as required.  $\sqcap$$\sqcup$

###### Proposition B.4.

Let $p_{i}$ be a correct process. Then:

  1. (1)

$\forall v.\forall t.\,p_{i}\text{~{}sends~{}}{\tt
WISH}(v)\text{~{}at~{}}t{\implies}v\in\\{p_{i}.{\sf view}^{+}(t),p_{i}.{\sf
view}^{+}(t)+1\\}$.

  2. (2)

$\forall v.\forall t.\,p_{i}\text{~{}sends~{}}{\tt
WISH}(v)\text{~{}at~{}}t\wedge v=p_{i}.{\sf view}^{+}(t)+1{\implies}p_{i}.{\sf
view}^{+}(t)=p_{i}.{\sf view}(t)\wedge p_{i}.{\sf advanced}(t)=\text{\sc
true}$.

###### Lemma B.5.

For all views $v,v^{\prime}>0$, if a correct process sends ${\tt WISH}(v)$
before sending ${\tt WISH}(v^{\prime})$, then $v\leq v^{\prime}$.

Proof. Let $s$ and $s^{\prime}$ such that $s<s^{\prime}$ be the times at which
a correct process $p_{i}$ sends ${\tt WISH}(v)$ and ${\tt WISH}(v^{\prime})$
messages, respectively. We show that $v^{\prime}\geq v$. By Proposition
B.4(1), $v\in\\{p_{i}.{\sf view}^{+}(s),p_{i}.{\sf view}^{+}(s)+1\\}$ and
$v^{\prime}\in\\{p_{i}.{\sf view}^{+}(s^{\prime}),p_{i}.{\sf
view}^{+}(s^{\prime})+1\\}$. Hence, if $v=p_{i}.{\sf view}^{+}(s)$ or
$v^{\prime}=p_{i}.{\sf view}^{+}(s^{\prime})+1$, then we get $v\leq
v^{\prime}$ from the fact that $p_{i}.{\sf view}^{+}$ is non-decreasing. It
thus remains to consider the case when $v=p_{i}.{\sf view}^{+}(s)+1$ and
$v^{\prime}=p_{i}.{\sf view}^{+}(s^{\prime})$. In this case by Proposition
B.4(2), $p_{i}.{\sf view}^{+}(s)=p_{i}.{\sf view}(s)$ and $p_{i}.{\sf
advanced}(s)=\text{\sc true}$. We now consider several cases depending on the
line at which ${\tt WISH}(v^{\prime})$ is sent.

  * •

${\tt WISH}(v^{\prime})$ is sent at lines 3 or 3. Then $v^{\prime}=p_{i}.{\sf
view}^{+}(s^{\prime})=\max(p_{i}.{\sf view}(s^{\prime})+1,p_{i}.{\sf
view}^{+}(s^{\prime}))$. Since $p_{i}.{\sf view}$ is non-decreasing, we get
$p_{i}.{\sf view}^{+}(s^{\prime})\geq p_{i}.{\sf
view}(s^{\prime})+1>p_{i}.{\sf view}(s^{\prime})\geq p_{i}.{\sf
view}(s)=p_{i}.{\sf view}^{+}(s)$. Hence, $p_{i}.{\sf
view}^{+}(s^{\prime})>p_{i}.{\sf view}^{+}(s)$, and therefore,
$v^{\prime}=p_{i}.{\sf view}^{+}(s^{\prime})\geq p_{i}.{\sf view}^{+}(s)+1=v$,
as required.

  * •

${\tt WISH}(v^{\prime})$ is sent at line 3. Then $p_{i}.{\sf
advanced}(s^{\prime})=\text{\sc false}$. Since $p_{i}.{\sf
advanced}(s)=\text{\sc true}$, there exists a time $s^{\prime\prime}$ such
that $s<s^{\prime\prime}<s^{\prime}$ and $p_{i}$ enters a view at
$s^{\prime\prime}$. By the view entry condition $p_{i}.{\sf
view}(s^{\prime\prime})>p_{i}.\textit{prev{\textunderscore}v}(s^{\prime\prime})$.
Since $p_{i}.{\sf view}$ is non-decreasing, we get $p_{i}.{\sf
view}^{+}(s^{\prime})\geq p_{i}.{\sf view}(s^{\prime})\geq p_{i}.{\sf
view}(s^{\prime\prime})>p_{i}.{\sf view}(s)=p_{i}.{\sf view}^{+}(s)$. Thus,
$p_{i}.{\sf view}^{+}(s^{\prime})>p_{i}.{\sf view}^{+}(s)$ and therefore,
$v^{\prime}=p_{i}.{\sf view}^{+}(s^{\prime})\geq p_{i}.{\sf view}^{+}(s)+1=v$,
as required.

  * •

${\tt WISH}(v^{\prime})$ is sent at line 3. Then $p_{i}.{\sf
view}^{+}(s^{\prime})>p_{i}.\textit{prev{\textunderscore}v}^{+}(s^{\prime})\geq
p_{i}.{\sf view}^{+}(s)$, and therefore, $v^{\prime}=p_{i}.{\sf
view}^{+}(s^{\prime})\geq p_{i}.{\sf view}^{+}(s)+1=v$, as required.

$\sqcap$$\sqcup$

In order to cope with message loss before ${\sf GST}$, every correct process
retransmits the highest ${\tt WISH}$ it sent every $\rho$ units of time,
according to its local clock (lines 3-3). Eventually, one of these
retransmissions will occur after ${\sf GST}$, and therefore, there exists a
time by which all correct processes are guaranteed to send their highest ${\tt
WISH}$es at least once after ${\sf GST}$. The earliest such time,
$\overline{{\sf GST}}$, is defined as follows:

$\overline{{\sf GST}}=\begin{cases}{\sf GST}+\rho,&\text{if }A_{\rm
first}(0)<{\sf GST};\\\ A_{\rm first}(0),&\text{otherwise}.\end{cases}$

From this definition it follows that

(5) $\overline{{\sf GST}}\geq{\sf GST}.$

Lemma B.6 below formalizes the key property of $\overline{{\sf GST}}$.

###### Lemma B.6.

For all correct processes $p_{i}$, times $t\geq\overline{{\sf GST}}$, and
views $v$, if $p_{i}$ sends ${\tt WISH}(v)$ at a time $\leq t$, then there
exists a view $v^{\prime}\geq v$ and a time $t^{\prime}$ such that ${\sf
GST}\leq t^{\prime}\leq t$ and $p_{i}$ sends ${\tt WISH}(v^{\prime})$ at
$t^{\prime}$.

Proof. Let $s\leq t$ be the time at which $p_{i}$ sends ${\tt WISH}(v)$. We
consider two cases. Suppose first that $A_{\rm first}(0)\geq{\sf GST}$. By
Lemma B.3, $s\geq A_{\rm first}(0)$, and therefore, ${\sf GST}\leq s\leq t$.
Thus, choosing $t^{\prime}=s$ and $v^{\prime}=v$ validates the lemma. Suppose
next that $A_{\rm first}(0)<{\sf GST}$. Then by the definition of
$\overline{{\sf GST}}$, $t\geq{\sf GST}+\rho$. If $s\geq{\sf GST}$, then ${\sf
GST}\leq s\leq t$, and therefore, choosing $t^{\prime}=s$ and $v^{\prime}=v$
validates the lemma. Assume now that $s<{\sf GST}$. Since after ${\sf GST}$
the $p_{i}$’s local clock advances at the same rate as real time, there exists
a time $s^{\prime}$ satisfying ${\sf GST}\leq s^{\prime}\leq t$ such that
$p_{i}$ executes the periodic retransmission code in lines 3-3 at
$s^{\prime}$. We now show that

(6) $p_{i}.{\sf advanced}(s^{\prime})\vee p_{i}.{\sf view}^{+}(s^{\prime})>0.$

Since $p_{i}$ already sent a ${\tt WISH}$ message at $s<{\sf GST}\leq
s^{\prime}$, by the structure of the code,

$p_{i}.{\sf advanced}(s)\vee p_{i}.{\sf view}^{+}(s)>0.$

If $p_{i}.{\sf view}^{+}(s)>0$, then since $p_{i}.{\sf view}^{+}$ is non-
decreasing, $p_{i}.{\sf view}^{+}(s^{\prime})>0$, and therefore, (6) holds.
Assume now that $p_{i}.{\sf advanced}(s)$. If $p_{i}.{\sf
advanced}(s^{\prime})$, then (6) holds too. We therefore consider the case
when $\neg p_{i}.{\sf advanced}(s^{\prime})$. Then there exists a time $s\leq
s^{\prime\prime}\leq s^{\prime}$ at which $p_{i}$ enters the view $p_{i}.{\sf
view}(s^{\prime\prime})>0$. Hence, $p_{i}.{\sf view}^{+}(s^{\prime})\geq
p_{i}.{\sf view}^{+}(s^{\prime\prime})\geq p_{i}.{\sf
view}(s^{\prime\prime})>0$, validating (6). Thus, (6) holds in all cases.
Therefore, at $s^{\prime}$ the process $p_{i}$ sends ${\tt WISH}(v^{\prime})$
for some view $v^{\prime}$. By Lemma B.5, $v^{\prime}\geq v$, and above we
established ${\sf GST}\leq s^{\prime}\leq t$, as required.  $\sqcap$$\sqcup$

###### Lemma B.7.

Consider a view $v>0$ and assume that $v$ is entered by a correct process. If
$E_{\rm first}(v)\geq\overline{{\sf GST}}$, and no correct process attempts to
advance from $v$ before $E_{\rm first}(v)+2\delta$, then all correct processes
enter $v$ and $E_{\rm last}(v)\leq E_{\rm first}(v)+2\delta$.

Proof. If some correct process attempts to advance from a view $v^{\prime}>v$
before $E_{\rm first}(v)+2\delta$, then by Proposition 3.1, some correct
process must also enter the view $v+1$. By Lemma B.2, this implies that some
correct process attempts to advance from $v$ before $E_{\rm
first}(v)+2\delta$, contradicting the lemma’s premise. Thus, no correct
process attempts to advance from any view $v^{\prime}\geq v$ before $E_{\rm
first}(v)+2\delta$, and therefore, by Lemma B.1, no correct process can send
${\tt WISH}(v^{\prime})$ with $v^{\prime}>v$ earlier than $E_{\rm
first}(v)+2\delta$. Once any such ${\tt WISH}(v^{\prime})$ is sent, it will
take a non-zero time until it is received by any correct process. Thus, we
have:

  1. (*)

no correct process receives ${\tt WISH}(v^{\prime})$ with $v^{\prime}>v$ from
a correct process until after $E_{\rm first}(v)+2\delta$.

Let $p_{i}$ be a correct process that enters $v$ at $E_{\rm first}(v)$. By the
view entry condition, $p_{i}.{\sf view}(E_{\rm first}(v))=v$, and therefore
$p_{i}.{\sf max\texttt{\textunderscore}views}(E_{\rm first}(v))$ includes
$2f+1$ entries $\geq v$. At least $f+1$ of these entries belong to correct
processes, and by (*), none of them can be $>v$. Hence, there exists a set $C$
of $f+1$ correct processes, each of which sends ${\tt WISH}(v)$ to all
processes before $E_{\rm first}(v)$.

Since $E_{\rm first}(v)\geq\overline{{\sf GST}}$, by Lemma B.6, every
$p_{j}\in C$ also sends ${\tt WISH}(v^{\prime})$ with $v^{\prime}\geq v$ at
some time $s_{j}$ such that ${\sf GST}\leq s_{j}\leq E_{\rm first}(v)$. Then
by (*) we have $v^{\prime}=v$. It follows that each $p_{j}\in C$ is guaranteed
to send ${\tt WISH}(v)$ to all correct processes between ${\sf GST}$ and
$E_{\rm first}(v)$. Since all messages sent by correct processes after ${\sf
GST}$ are guaranteed to be received by all correct processes within $\delta$
of their transmission, by $E_{\rm first}(v)+\delta$ all correct processes will
receive ${\tt WISH}(v)$ from at least $f+1$ correct processes.

Consider an arbitrary correct process $p_{j}$ and let $t_{j}\leq E_{\rm
first}(v)+\delta$ be the earliest time by which $p_{j}$ receives ${\tt
WISH}(v)$ from $f+1$ correct processes. By (*), no correct process sends ${\tt
WISH}(v^{\prime})$ with $v^{\prime}>v$ before $t_{j}<E_{\rm
first}(v)+2\delta$. Thus, $p_{j}.{\sf
max\texttt{\textunderscore}views}(t_{j})$ includes at least $f+1$ entries
equal to $v$ and at most $f$ entries $>v$, so that $p_{j}.{\sf
view}^{+}(t_{j})=v$. Then $p_{j}$ sends ${\tt WISH}(v)$ to all processes no
later than $t_{j}\leq E_{\rm first}(v)+\delta$. Since $E_{\rm
first}(v)\geq\overline{{\sf GST}}$, by Lemma B.6, $p_{j}$ also sends ${\tt
WISH}(v^{\prime})$ with $v^{\prime}\geq v$ in-between ${\sf GST}$ and $E_{\rm
first}(v)+\delta$. By (*), $v^{\prime}=v$, and therefore, $p_{j}$ must have
sent ${\tt WISH}(v)$ to all processes sometime between ${\sf GST}$ and $E_{\rm
first}(v)+\delta$. Hence, all correct processes are guaranteed to send ${\tt
WISH}(v)$ to all correct processes between ${\sf GST}$ and $E_{\rm
first}(v)+\delta$.

Consider an arbitrary correct process $p_{k}$ and let $t_{k}\leq E_{\rm
first}(v)+2\delta$ be the earliest time by which $p_{k}$ receives ${\tt
WISH}(v)$ from all correct processes. Then by (*), all entries of correct
processes in $p_{k}.{\sf max\texttt{\textunderscore}views}(t_{k})$ are equal
to $v$. Since there are at least $2f+1$ correct processes: _(i)_ at least
$2f+1$ entries in $p_{k}.{\sf max\texttt{\textunderscore}views}(t_{k})$ are
equal to $v$, and _(ii)_ one of the $f+1$ highest entries in $p_{k}.{\sf
max\texttt{\textunderscore}views}(t_{k})$ is equal to $v$. From _(i)_ ,
$p_{k}.{\sf view}^{+}(t_{k})\geq p_{k}.{\sf view}(t_{k})\geq v$, and from
_(ii)_ , $p_{k}.{\sf view}(t_{k})\leq p_{k}.{\sf view}^{+}(t_{k})\leq v$.
Therefore, $p_{k}.{\sf view}(t_{k})=p_{k}.{\sf view}^{+}(t_{k})=v$, so that
$p_{k}$ enters $v$ no later than $t_{k}\leq E_{\rm first}(v)+2\delta$. We have
thus shown that by $E_{\rm first}(v)+2\delta$, all correct processes enter
$v$, as required.  $\sqcap$$\sqcup$

###### Lemma B.8.

Startup holds: suppose there exists a set $P$ of $f+1$ correct processes such
that $\forall p_{i}\in P.\,{A_{i}(0)\mathpunct{\downarrow}}$; then eventually
some correct process enters view $1$.

Proof. Assume by contradiction that there exists a set $P$ of $f+1$ correct
processes such that $\forall p_{i}\in P.\,{A_{i}(0)\mathpunct{\downarrow}}$,
and no correct process enters the view $1$. By Proposition 3.1, the latter
implies

(7) $\forall v^{\prime}>0.\,\forall p_{i}\in\mathcal{C}.\,E_{\rm
first}(v^{\prime})\mathpunct{\uparrow}.$

Then by Lemma B.1 we have

(8) $\forall t.\,\forall v^{\prime}>1.\,\forall
p_{i}.\,\neg(p_{i}\text{~{}sends~{}}{\tt
WISH}(v^{\prime})\text{~{}at~{}}t\wedge p_{i}\text{~{}is~{}correct}).$

Let $T_{1}=\max(\overline{{\sf GST}},A_{\rm last}(0))$. Since there exists a
set $P$ of $f+1$ correct processes that attempt to advance from view $0$, each
$p_{i}\in P$ sends ${\tt WISH}(v_{i})$ with $v_{i}>0$ before $T_{1}$. Since
$T_{1}\geq\overline{{\sf GST}}$, by Lemma B.6, there exists a view
$v_{i}^{\prime}\geq 1$ and a time $s_{i}$ such that ${\sf GST}\leq s_{i}\leq
T_{1}$ and $p_{i}$ sends ${\tt WISH}(v_{i}^{\prime})$ at $s_{i}$. By (8),
$v_{i}^{\prime}=1$. Since the links are reliable after ${\sf GST}$, the ${\tt
WISH}(1)$ sent by $p_{i}$ at $s_{i}$ will be received by all correct
processes.

Thus, there exists a time $T_{2}\geq T_{1}\geq\overline{{\sf GST}}$ by which
all correct processes have received ${\tt WISH}(1)$ from all processes in $P$.
Fix an arbitrary correct process $p_{j}$. Since all process in $P$ are
correct, all entries in $p_{j}.{\sf max\texttt{\textunderscore}views}(T_{2})$
associated with the processes in $P$ are equal to $1$. Since $|P|=f+1$,
$p_{j}.{\sf max\texttt{\textunderscore}views}(T_{2})$ includes at least $f+1$
entries $\geq 1$, and therefore, $p_{j}.{\sf view}^{+}(T_{2})\geq 1$. Hence,
$p_{j}$ sends ${\tt WISH}(v_{j})$ with $v_{j}\geq 1$ no later than $T_{2}$.
Since $T_{2}\geq\overline{{\sf GST}}$, by Lemma B.6 there exists a view
$v^{\prime}_{j}\geq 1$ and a time $s_{j}$ such that ${\sf GST}\leq s_{j}\leq
T_{2}$ and $p_{j}$ sends ${\tt WISH}(v^{\prime}_{j})$ at $s_{j}$. By (8),
$v^{\prime}_{j}=1$. Since the links are reliable after ${\sf GST}$, the ${\tt
WISH}(1)$ sent by $p_{j}$ will be received by all correct processes.

Thus, there exists a time $T_{3}\geq T_{2}\geq\overline{{\sf GST}}$ by which
all correct processes have received ${\tt WISH}(1)$ from all correct
processes. Fix an arbitrary correct process $p_{k}$. By (8), all entries of
correct processes in $p_{k}.{\sf max\texttt{\textunderscore}views}(T_{3})$ are
equal to $1$. Since there are at least $2f+1$ correct processes: _(i)_ at
least $2f+1$ entries in $p_{k}.{\sf max\texttt{\textunderscore}views}(T_{3})$
are equal to $1$, and _(ii)_ one of the $f+1$ highest entries in $p_{k}.{\sf
max\texttt{\textunderscore}views}(T_{2})$ is equal to $1$. From _(i)_ ,
$p_{k}.{\sf view}^{+}(T_{2})\geq p_{k}.{\sf view}(T_{2})\geq 1$, and from
_(ii)_ , $p_{k}.{\sf view}(T_{2})\leq p_{k}.{\sf view}^{+}(T_{2})\leq 1$.
Hence, $p_{k}.{\sf view}(T_{2})=p_{k}.{\sf view}^{+}(T_{2})=1$, and therefore,
$p_{k}$ enters view $1$ by $T_{2}$, contradicting (7).  $\sqcap$$\sqcup$

###### Lemma B.9.

Progress holds: consider a view $v>0$ that is entered by a correct process,
and suppose there exists a set $P$ of $f+1$ correct processes such that

(9) $\forall p_{i}\in
P.\,{E_{i}(v)\mathpunct{\downarrow}}\implies{A_{i}(v)\mathpunct{\downarrow}};$

then eventually some correct process enters $v+1$.

Proof. Assume by contradiction that the required does not hold. Then, there
exists a view $v>0$ such that some correct process enters $v$, (9) holds, and
no correct process enters the view $v+1$. By Proposition 3.1, the latter
implies that

(10) $\forall v^{\prime}>v.\,\forall p_{i}\in\mathcal{C}.\,E_{\rm
first}(v^{\prime})\mathpunct{\uparrow}.$

Thus, by Lemma B.1, we have

(11) $\forall t.\,\forall v^{\prime}>v+1.\,\forall
p_{i}.\,\neg(p_{i}\text{~{}sends~{}}{\tt
WISH}(v^{\prime})\text{~{}at~{}}t\wedge p_{i}\text{~{}is~{}correct}).$

Let $T_{1}=\max(\overline{{\sf GST}},E_{\rm first}(v))$. Since some correct
process entered $v$ by $T_{1}$, there exists a set $C$ consisting of $f+1$
correct processes all of which sent ${\tt WISH}(v^{\prime})$ with
$v^{\prime}\geq v$ before $T_{1}$. Consider $p_{i}\in C$ and let $t_{i}\leq
T_{1}$ be a time such that at $t_{i}$ the process $p_{i}$ sends ${\tt
WISH}(v_{i})$ with $v_{i}\geq v$. Since $T_{1}\geq\overline{{\sf GST}}$, by
Lemma B.6, there exists a view $v_{i}^{\prime}\geq v_{i}$ and a time $s_{i}$
such that ${\sf GST}\leq s_{i}\leq T_{1}$ and $p_{i}$ sends ${\tt
WISH}(v_{i}^{\prime})$ at $s_{i}$. By (11), we have
$v_{i}^{\prime}\in\\{v,v+1\\}$. Since the links are reliable after ${\sf
GST}$, the ${\tt WISH}(v_{i}^{\prime})$ sent by $p_{i}$ at $s_{i}$ will be
received by all correct processes.

Thus, there exists a time $T_{2}\geq T_{1}\geq\overline{{\sf GST}}$ by which
all correct processes have received ${\tt WISH}(v^{\prime})$ with
$v^{\prime}\in\\{v,v+1\\}$ from all processes in $C$. Consider an arbitrary
correct process $p_{j}$. By (11), the entry of every process in $C$ in
$p_{j}.{\sf max\texttt{\textunderscore}views}(T_{2})$ is equal to either $v$
or $v+1$. Since $|C|\geq f+1$ and all processes in $C$ are correct,
$p_{j}.{\sf max\texttt{\textunderscore}views}(T_{2})$ includes at least $f+1$
entries $\geq v$. Thus, $p_{j}.{\sf view}^{+}(T_{2})\geq v$, and therefore,
$p_{j}$ sends ${\tt WISH}(v_{j})$ with $v_{j}\geq v$ no later than at $T_{2}$.
By (11), $v_{j}\in\\{v,v+1\\}$. Since $T_{2}\geq\overline{{\sf GST}}$, by
Lemma B.6, there exists a view $v_{j}^{\prime}\geq v$ and a time $s_{j}$ such
that ${\sf GST}\leq s_{j}\leq t_{j}$ and $p_{j}$ sends ${\tt
WISH}(v_{j}^{\prime})$ at $s_{j}$. By (11), $v_{j}^{\prime}\in\\{v,v+1\\}$.
Since the links are reliable after ${\sf GST}$, the ${\tt
WISH}(v_{j}^{\prime})$ sent by $p_{j}$ at $s_{j}$ will be received by all
correct processes.

Thus, there exists a time $T_{3}\geq T_{2}\geq\overline{{\sf GST}}$ by which
all correct processes have received ${\tt WISH}(v^{\prime})$ such that
$v^{\prime}\in\\{v,v+1\\}$ from all correct processes. Consider an arbitrary
correct process $p_{k}$, and suppose that $p_{k}$ is a member of the set $P$
stipulated by the lemma’s premise. Then at $T_{3}$, all entries of correct
processes in $p_{k}.{\sf max\texttt{\textunderscore}views}$ are $\geq v$. By
(11), each of these entries is equal to either $v$ or $v+1$. Since at least
$2f+1$ processes are correct: _(i)_ at least $2f+1$ entries in $p_{k}.{\sf
max\texttt{\textunderscore}views}(T_{3})$ are $\geq v$, and _(ii)_ one of the
$f+1$ highest entries in $p_{k}.{\sf max\texttt{\textunderscore}views}(T_{3})$
is $\leq v+1$. From _(i)_ , $p_{k}.{\sf view}^{+}(T_{3})\geq p_{k}.{\sf
view}(T_{3})\geq v$, and from _(ii)_ , $p_{k}.{\sf view}(T_{3})\leq p_{k}.{\sf
view}^{+}(T_{3})\leq v+1$. Hence, $p_{k}.{\sf view}(T_{3}),p_{k}.{\sf
view}^{+}(T_{3})\in\\{v,v+1\\}$. Since no correct process enters $v+1$,
$p_{k}.{\sf view}(T_{3})$ and $p_{k}.{\sf view}^{+}(T_{3})$ cannot be both
simultaneously equal to $v+1$. Thus, $p_{k}.{\sf view}(T_{3})=v$, and either
$p_{k}.{\sf view}^{+}(T_{3})=v$ or $p_{k}.{\sf view}^{+}(T_{3})=v+1$. If
$p_{k}.{\sf view}^{+}(T_{3})=v+1$, then $p_{k}$ has sent ${\tt WISH}(v_{k})$
with $v_{k}=v+1$ when $p_{k}.{\sf view}^{+}$ has first become equal to $v+1$
sometime before $T_{3}$. On the other hand, if $p_{k}.{\sf
view}(T_{3})=p_{k}.{\sf view}^{+}(T_{3})=v$, then $p_{k}$ has entered $v$ at
some time $t\leq T_{3}$. Since $p_{k}\in P$, by (9), there exists a time
$t^{\prime}\geq t$ such that $p_{k}$ attempts to advance from $v$ at
$t^{\prime}$, and therefore, sends ${\tt WISH}(v_{k})$ with $v_{k}\geq v+1$ at
$t^{\prime}$. By (11), $v_{k}\leq v+1$, and therefore, $v_{k}=v+1$. Thus,
there exists a time $t_{k}\geq T_{3}$ by which $p_{k}$ sends ${\tt WISH}(v+1)$
to all processes. Since $t_{k}\geq T_{3}\geq\overline{{\sf GST}}$, by Lemma
B.6, there exists a view $v^{\prime}_{k}\geq v+1$ and a time $s_{k}$ such that
${\sf GST}\leq s_{k}\leq t_{k}$ and $p_{k}$ sends ${\tt WISH}(v^{\prime}_{k})$
at $s_{k}$. By (11), $v^{\prime}_{k}=v+1$. Since the links are reliable after
${\sf GST}$, the ${\tt WISH}(v+1)$ sent by $p_{k}$ will be received by all
correct processes.

Thus, there exists a time $T_{4}\geq T_{3}\geq\overline{{\sf GST}}$ by which
all correct processes have received ${\tt WISH}(v+1)$ from all processes in
$P$. Fix an arbitrary correct process $p_{l}$. Since all process in $P$ are
correct, by (11), all entries in $p_{l}.{\sf
max\texttt{\textunderscore}views}(T_{4})$ associated with the processes in $P$
are equal to $v+1$. Since $|P|=f+1$, $p_{l}.{\sf
max\texttt{\textunderscore}views}(T_{4})$ includes at least $f+1$ entries
equal to $v+1$, and therefore, $p_{l}.{\sf view}^{+}(T_{4})\geq v+1$. Hence,
$p_{l}$ sends ${\tt WISH}(v_{l})$ with $v_{l}\geq v+1$ no later than $T_{4}$.
Since $T_{4}\geq\overline{{\sf GST}}$, by Lemma B.6 there exists a view
$v^{\prime}_{l}\geq v+1$ and a time $s_{l}$ such that ${\sf GST}\leq s_{l}\leq
T_{4}$ and $p_{l}$ sends ${\tt WISH}(v^{\prime}_{l})$ at $s_{l}$. By (11),
$v_{l}^{\prime}=v+1$. Since the links are reliable after ${\sf GST}$, the
${\tt WISH}(v+1)$ sent by $p_{l}$ will be received by all correct processes.

Thus, there exists a time $T_{5}\geq T_{4}\geq\overline{{\sf GST}}$ by which
all correct processes have received ${\tt WISH}(v+1)$ from all correct
processes. Fix an arbitrary correct process $p_{m}$. By (11), all entries of
correct processes in $p_{m}.{\sf max\texttt{\textunderscore}views}(T_{5})$ are
equal to $v+1$. Since there are at least $2f+1$ correct processes: _(i)_ at
least $2f+1$ entries in $p_{m}.{\sf max\texttt{\textunderscore}views}(T_{5})$
are equal to $v+1$, and _(ii)_ one of the $f+1$ highest entries in $p_{m}.{\sf
max\texttt{\textunderscore}views}(T_{5})$ is equal to $v+1$. From _(i)_ ,
$p_{m}.{\sf view}^{+}(T_{5})\geq p_{m}.{\sf view}(T_{5})\geq v+1$, and from
_(ii)_ , $p_{m}.{\sf view}(T_{5})\leq p_{l}.{\sf view}^{+}(T_{5})\leq v+1$.
Hence, $p_{m}.{\sf view}(T_{5})=p_{m}.{\sf view}^{+}(T_{5})=v+1$, and
therefore, $p_{m}$ enters $v+1$ by $T_{5}$, contradicting (10).
$\sqcap$$\sqcup$

###### Theorem B.10.

Consider an execution with an eventual message delay $\delta$. Then in this
execution the algorithm in Figure 3 satisfies the properties in Figure 1 for
$d=2\delta$.

Proof. Monotonicity is satisfied trivially, and Validity, Startup, and
Progress are given by Lemmas B.2, B.8, and B.9, respectively. To prove Bounded
Entry, let

(12) $\mathcal{V}=\max\\{v\mid{E_{\rm first}(v)\mathpunct{\downarrow}}\wedge
E_{\rm first}(v)<\overline{{\sf GST}}\\}+1.$

Then $\forall v\geq\mathcal{V}.\,{E_{\rm
first}(v)\mathpunct{\downarrow}}{\implies}E_{\rm first}(v)\geq\overline{{\sf
GST}}$. Thus, by Lemma B.7, Bounded Entry holds for $d=2\delta$, as required.
$\sqcap$$\sqcup$

###  B.2. Proof of the Synchronizer Performance Properties

The following lemma bounds the latency of entering $v$ as a function of the
time by which all correct processes have sent such ${\tt WISH}$es.

###### Lemma B.11.

For all views $v>0$ and times $s$, if all correct processes $p_{i}$ send ${\tt
WISH}(v_{i})$ with $v_{i}\geq v$ no later than at $s$, and some correct
process enters $v$, then $E_{\rm last}(v)\leq\max(s,\overline{{\sf
GST}})+\delta$.

Proof. Fix an arbitrary correct process $p_{i}$ that sends ${\tt WISH}(v_{i})$
with $v_{i}\geq v$ to all processes at time $t_{i}\leq
s\leq\max(s,\overline{{\sf GST}})$. Since $\max(s,\overline{{\sf
GST}})\geq\overline{{\sf GST}}$, by Lemma B.6 there exists a time
$t_{i}^{\prime}$ such that ${\sf GST}\leq
t_{i}^{\prime}\leq\max(s,\overline{{\sf GST}})$ and at $t_{i}^{\prime}$,
$p_{i}$ sends ${\tt WISH}(v_{i}^{\prime})$ with $v_{i}^{\prime}\geq v_{i}\geq
v$ to all processes. Since $t_{i}^{\prime}\geq{\sf GST}$, all correct
processes receive ${\tt WISH}(v_{i}^{\prime})$ from $p_{i}$ no later than at
$t_{i}^{\prime}+\delta\leq\max(s,\overline{{\sf GST}})+\delta$.

Consider an arbitrary correct process $p_{j}$ and let
$t_{j}\leq\max(s,\overline{{\sf GST}})+\delta$ be the earliest time by which
$p_{j}$ receives ${\tt WISH}(v_{i}^{\prime})$ with with $v_{i}^{\prime}\geq v$
from each correct processes $p_{i}$. Thus, at $t_{j}$, the entries of all
correct processes in $p_{j}.{\sf max\texttt{\textunderscore}views}$ are
occupied by views $\geq v$. Since at least $2f+1$ entries in $p_{j}.{\sf