Making Byzantine consensus live

Abstract

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

1 Introduction

The popularity of blockchains has renewed interest in Byzantine consensus protocols, which allow a set of processes to reach an agreement on a value despite a fraction of the processes being malicious. Unlike proof-of-work or proof-of-stake protocols underlying many blockchains, classic Byzantine consensus assumes a fixed set of processes, but can in exchange provide hard guarantees on the finality of decisions. Byzantine consensus protocols are now used in blockchains with both closed membership [7, 31] and open one [14, 15, 30], in the latter case by running Byzantine consensus inside a committee elected among blockchain participants. These use cases have motivated a wave of new algorithms [14, 31, 45] that improve on classical solutions, such as DLS [27] and PBFT [19].

Designing Byzantine consensus protocols is challenging, as witnessed by a number of bugs found in recent protocols [2, 5, 17, 35]. Historically, researchers have paid more attention to safety of these protocols rather than liveness: e.g., while PBFT came with a safety proof [18], the nontrivial mechanism used to guarantee its liveness has never had one. However, achieving liveness of Byzantine consensus is no less challenging than its safety. The seminal FLP result shows that guaranteeing both properties is impossible when the network is asynchronous [28]. Hence, consensus protocols aim to guarantee safety under all circumstances and liveness only when the network is synchronous. The expected network behavior is formalized by the partial synchrony model [27]. In one of its more general formulations [21], the model guarantees 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 $\mathsf{GST}$, however, messages can be lost or arbitrarily delayed, and clocks at different processes can drift apart without bound. This behavior reflects real-world phenomena: in practice, the space for buffering unacknowledged messages in the communication layer is bounded, and messages will be dropped if this space overflows; also, clocks are synchronized by exchanging messages (e.g., using NTP), so network asynchrony will make clocks diverge.

Byzantine consensus protocols usually achieve liveness under partial synchrony by dividing execution into views (aka rounds), each with a designated leader process responsible for driving the protocol towards a decision. If a view does not reach a decision (e.g., because its leader is faulty), processes switch to the next one. To ensure liveness, the protocol needs to guarantee that all correct processes will eventually enter the same view with a correct leader and stay there long enough to complete the communication required for a decision. Achieving such view synchronization is nontrivial, because before $\mathsf{GST}$, clocks that could measure the duration of a view can diverge, and messages that could be used to bring processes into the same view can get lost or delayed. Thus, by $\mathsf{GST}$ processes may end up in wildly different views, and the protocol has to bring them back together, despite any disruption caused by Byzantine processes. Some of the Byzantine consensus protocols integrate the functionality required for view synchronization with the core consensus protocol, which complicates their design [14, 19]. In contrast, both the seminal DLS work on consensus under partial synchrony [27] and some of the more recent work [1, 41, 45] suggest separating the complex functionality required for view synchronization into a distinct component—view synchronizer, or simply synchronizer. This approach allows designing Byzantine protocols modularly, with mechanisms for ensuring liveness reused among different protocols.

However, to date there has been no rigorous analysis showing which properties of a synchronizer would be sufficient for modern Byzantine consensus protocols. Furthermore, the existing implementations of synchronizer-like abstractions are either expensive or do not handle partial synchrony in its full generality. In particular, DLS [27] implements view synchronization by constructing clocks from program counters of processes. Since these counters drift apart on every step, processes need to frequently synchronize their local clocks. This results in prohibitive communication overheads and makes this solution impractical. Abraham et al. [1] address this inefficiency by assuming hardware clocks with a bounded drift, but only give a solution for a synchronous system. Finally, recent synchronizers by Naor et al. [41] only handle a simplified variant of partial synchrony which disallows clock drift and message loss before $\mathsf{GST}$.

In this paper we make several contributions that address the above limitations:

• We propose a simple and precise specification of a synchronizer abstraction sufficient for single-shot consensus (Sect. 3). The specification ensures that from some point on after $\mathsf{GST}$, all correct processes go through the same sequence of views, overlapping for some time in each one of them. It precisely characterizes the duration of the overlap and gives bounds on how quickly correct processes switch between views.

• We propose a synchronizer implementation, called FastSync, and rigorously prove that it satisfies our specification. FastSync handles the general version of the partial synchrony model [27], allowing for an unknown $\delta$ and—before $\mathsf{GST}$—unbounded clock drift and message loss (Sect. 3.1). Despite the latter, the synchronizer runs in bounded space—a key feature under Byzantine failures, because the absence of a bound on the required memory opens the system to denial-of-service attacks. Our synchronizer also does not use digital signatures, relying only on authenticated point-to-point links.

• We show that our synchronizer specification is strong enough to guarantee liveness under partial synchrony for single-shot versions of a number of Byzantine consensus protocols. All of these protocols can thus achieve liveness using a single synchronizer—FastSync. In the paper we consider in detail PBFT [19] (Sect. 5.1), HotStuff [45] (Sect. 5.2) and a two-phase version of the latter similar to Tendermint [14] (Sect. 5.3); in [12, §B] we also analyze SBFT [31] and Tendermint itself. The precise guarantees about the timing of view switches provided by our specification are key to handle such a wide range of protocols.

• We provide a precise latency analysis of FastSync, showing that it quickly converges to a synchronized view (Sect. 3.2). Building on this analysis, we prove worst-case latency bounds for the above consensus protocols when using FastSync. Our bounds consider both favorable and unfavorable conditions: if the protocol executes during a synchronous period, they determine how quickly all correct processes decide; and if the protocol starts during an asynchronous period, how quickly the processes decide after $\mathsf{GST}$. Our analysis stipulates an a priori known conservative message delay estimate $\Delta$, which bounds the actual post-$\mathsf{GST}$ message delay $\delta$ in every execution. This allows us, for the first time, to derive closed-form expressions for Byzantine consensus latency bounds in a partial synchrony model where $\delta$ both is unknown and only holds after $\mathsf{GST}$.

• Most of the protocols we consider were originally presented in a form optimized for solving consensus repeatedly. By specializing them to the standard single-shot consensus problem and factoring out the functionality required for view synchronization, we are able to succinctly capture their core ideas in a uniform framework. This allows us to highlight the similarities and differences among protocols in a pedagogical fashion, thus providing a tutorial on modern Byzantine consensus.

Fig. 1

Visual illustration of the synchronizer properties

2 System model

We assume 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 call a set Q of $2f+1$ processes a quorum and write $\mathsf{quorum}(Q)$ in this case. Processes communicate using authenticated point-to-point links and, when needed, can sign messages using digital signatures. We denote by $\langle m \rangle _i$ a message m signed by process $p_i$. We sometimes use a cryptographic hash function $\mathsf{hash}()$, which must be collision-resistant: the probability of an adversary producing inputs m and $m'$ such that $\mathsf{hash}(m) = \mathsf{hash}(m')$ is negligible.

We consider a generalized partial synchrony model [21, 27], which guarantees that, for each execution of the protocol, there exist a time $\mathsf{GST}$ and a duration $\delta$ such that after $\mathsf{GST}$ message delays between correct processes are bounded by $\delta$. Before $\mathsf{GST}$ messages can get arbitrarily delayed or lost, although for simplicity we assume that self-addressed messages are never lost and are delivered to the sender instantaneously. As in [21], we assume that the values of $\mathsf{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. However, to state some of our latency bounds, we also assume the existence of a known upper bound $\Delta$ on the maximum value of $\delta$ in any execution [33]. 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. Finally, we assume that the processes are equipped with hardware clocks that can drift unboundedly from real time before $\mathsf{GST}$, but do not drift thereafter (our results can be trivially adjusted to handle bounded clock drift after $\mathsf{GST}$, but we omit this for conciseness). We denote the set of time points by $\mathsf{Time}$ (ranged over by t) and assume that local message processing takes zero time.

3 Synchronizer specification and implementation

We now define a view synchronizer interface sufficient for single-shot Byzantine consensus, and present its specification and implementation. Let $\mathsf{View}= \{1, 2, \ldots \}$ be the set of views, ranged over by v; we sometimes use 0 to denote an invalid view. The job of the synchronizer is to produce notifications $\mathtt{new\_view}(v)$ at each correct process, telling it to enter view v. A process can ensure that the synchronizer has started operating by calling a special $\mathtt{start}()$ function. We assume that each correct process eventually calls $\mathtt{start}()$.

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 $\mathsf{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: \mathsf{View}\cup \{0\} \rightarrow \mathsf{Time}$, which is monotone and such that $F(0) = 0$. The liveness of a protocol usually relies on $F$ reaching a particular value $u$:

$$\begin{aligned} \exists v.\,\forall v'.\, v'\ge v \implies F(v') \ge u. \end{aligned}$$

(1)

This can be satisfied, e.g., by letting $F(v) = 2v$ or $F(v) = 2^v$.

Fig. 2

Synchronizer properties (holding for some ${\mathcal {V}}\in \mathsf{View}$). Properties 1–5 specify the synchronizer abstraction, sufficient to ensure consensus liveness. Properties A–C give latency bounds specific to our FastSync synchronizer (Sect. 3.1). The latter satisfies Property 4 for $d = 2\delta$. The parameter $\rho$ is the retransmission interval used by FastSync

Properties 1–5 of Fig. 2 define our synchronizer specification, and Fig. 1 illustrates them visually. (We explain Properties A–C later; Property A is also illustrated in Fig. 1). The specification strikes a balance between usability and implementability. On one hand, it is sufficient to prove the liveness of a range of consensus protocols (as we show in Sect. 5). On the other hand, it can be efficiently implemented under partial synchrony by our FastSync synchronizer (Sect. 3.1).

Ideally, a synchronizer should ensure that all correct processes overlap in each view v for a duration determined by F(v). However, achieving this before $\mathsf{GST}$ is impossible due to network and clock asynchrony. Therefore, we require a synchronizer to provide nontrivial guarantees only after $\mathsf{GST}$ and starting from some view ${\mathcal {V}}$. To formulate the guarantees we use the following notation. Given a view v that was entered by a correct process $p_i$, we denote by $E_{i}(v)$ the time when this happens; we let $E_{\mathrm{first}}(v)$ and $E_{\mathrm{last}}(v)$ denote respectively the earliest and the latest time when some correct process enters v. We let $S_{\mathrm{first}}$ and $S_{\mathrm{last}}$ be respectively the earliest and the latest time when some correct process calls $\mathtt{start}()$, and $S_{k}$ the earliest time by which k correct processes do so. Thus, a synchronizer must guarantee that views may only increase at a given process (Property 1), and ensure view synchronization starting from some view ${\mathcal {V}}$, entered after $\mathsf{GST}$ (Property 2). Starting from ${\mathcal {V}}$, correct processes do not skip any views (Property 3), enter each view $v \ge {\mathcal {V}}$ within at most d of each other (Property 4) and stay there for a determined amount of time: until $F(v)$ after the first process enters v (Property 5). Our FastSync implementation satisfies Property 4 for $d = 2\delta$. Properties 4 and 5 imply a lower bound on the overlap between the time intervals during which all correct processes execute in view v:

$$\begin{aligned} \forall v&\ge {\mathcal {V}}.\, E_{\mathrm{first}}(v + 1) - E_{\mathrm{last}}(v) {} \nonumber \\&> (E_{\mathrm{first}}(v) + F(v)) - (E_{\mathrm{first}}(v) +d) \nonumber \\&= F(v) - d. \end{aligned}$$

(2)

Byzantine consensus protocols are often leader-driven, with leaders rotating round-robin across views. Hence, (2) allows us to prove their liveness by showing that there will eventually be a view with a correct leader (due to Property 3) where all correct processes will overlap for long enough (due to (1) for a large enough $u$). Having separate Properties 4 and 5 instead of a single property in (2) is required to prove the liveness of some protocols, e.g., two-phase HotStuff (Sect. 5.3) and Tendermint (Sect. 5.4).

3.1 FastSync: a bounded-space synchronizer for partial synchrony

In Algorithm 1 we present our FastSync synchronizer, which satisfies the synchronizer specification (Properties 1–5 of Fig. 2) for $d = 2\delta$. Despite tolerating message loss before $\mathsf{GST}$, FastSync only requires bounded space; it also does not rely on digital signatures.

FastSync measures view duration using a timer $\mathsf{timer\_view}$: when the synchronizer tells the process to enter a view v, it sets the timer for the duration F(v). When the timer expires, the synchronizer does not immediately move to the next view $v'$; instead, it disseminates a special $\mathtt{WISH}(v')$ message, announcing its intention. Each process maintains an array $\mathsf{max\_views}: \{1,\ldots , n\} \rightarrow \mathsf{View}\cup \{0\}$, whose j-th entry stores the maximal view received in a $\mathtt{WISH}$ message from process $p_j$ (initially 0, updated in line 13). Keeping track of only the maximal views allows the synchronizer to run in bounded space. The process also maintains two variables, $\mathsf{view}$ and $\mathsf{view}^+$, derived from $\mathsf{max\_views}$ (initially 0, updated in lines 14 and 15): $\mathsf{view}^+$ (respectively, $\mathsf{view}$) is equal to the maximal view such that at least $f+1$ processes (respectively, $2f+1$ processes) wish to switch to a view no lower than this. The two variables monotonically increase and we always have $\mathsf{view}\le \mathsf{view}^+$.

The process enters the view determined by the $\mathsf{view}$ variable (line 19) when the latter increases ($\mathsf{view}> \textit{prev\_v}$ in line 16; we explain the extra condition later). At this point the process also resets its $\mathsf{timer\_view}$ (line 18). Thus, a process enters a view only if it receives a quorum of $\mathtt{WISH}$es for this view or higher, and a process may be forced to switch views even if its $\mathsf{timer\_view}$ has not yet expired. The latter helps lagging processes to catch up, but poses another challenge. Byzantine processes may equivocate, sending $\mathtt{WISH}$ messages to some processes but not others. In particular, they may send $\mathtt{WISH}$es for views $\ge v$ to some correct process, helping it to form a quorum of $\mathtt{WISH}$es sufficient for entering v. But they may withhold the same $\mathtt{WISH}$es from another correct process, so that it fails to form a quorum for entering v, as necessary, e.g., for Property 4. To deal with this, when a process receives a $\mathtt{WISH}$ that makes its $\mathsf{view}^+$ increase, the process sends $\mathtt{WISH}(\mathsf{view}^+)$ (line 21). By the definition of $\mathsf{view}^+$, at least one correct process has wished to move to a view no lower than $\mathsf{view}^+$. The $\mathtt{WISH}(\mathsf{view}^+)$ message replaces those that may have been omitted by Byzantine processes and helps all correct processes to quickly form the necessary quorums of $\mathtt{WISH}$es.

An additional guard on entering a view is $\mathsf{view}^+= \mathsf{view}$ in line 16, which 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 timer of the current view expires (line 4), the process sends a $\mathtt{WISH}$ for the maximum of $\mathsf{view}+1$ and $\mathsf{view}^+$. In other words, if $\mathsf{view}= \mathsf{view}^+$, so that the values of the two variables have not changed since the process entered the current view, then the process sends a $\mathtt{WISH}$ for the next view ($\mathsf{view}+1$). Otherwise, $\mathsf{view}< \mathsf{view}^+$, and the process sends a $\mathtt{WISH}$ for the higher view $\mathsf{view}^+$.

To deal with message loss before $\mathsf{GST}$, a process retransmits the highest $\mathtt{WISH}$ it sent every $\rho$ units of time, according to its local clock (line 6). Depending on whether $\mathsf{timer\_view}$ is enabled, the $\mathtt{WISH}$ is computed as in lines 21 or 5. Finally, the $\mathtt{start}$ function ensures that the synchronizer has started operating at the process by sending $\mathtt{WISH}(1)$, unless the process has already done so in line 21 due to receiving $f+1$ $\mathtt{WISH}$es from other processes.

The guard $\mathsf{max\_views}[i] > 0$ in line 9 ensures that the first $\mathtt{WISH}$ sent by a process is always triggered by executing the code at line 3, 5, or 21. Since we assume that self-addressed messages are instantaneously delivered to the sender, this guard becomes permanently enabled as soon as the first $\mathtt{WISH}$ from any one of those lines has been sent.

Discussion FastSync requires only O(n) variables for storing views. The algorithm also ensures that eventually every view is entered by all correct processes (Property 3), and views entered by correct processes throughout an execution do not skip values; the latter is formalized by the following lemma, proved in Sect. 4.1.

Lemma 1

For all views v and $v'$ such that $0< v < v'$, if a correct process enters $v'$, then some correct process has previously entered v.

Thus, although the individual view values stored by FastSync are unbounded, Property 3 and Lemma 1 limit the power of the adversary to exhaust their allocated space, similarly to [9].

The basic mechanisms we use in our synchronizer—entering views supported by $2f+1$ $\mathtt{WISH}$es and relaying views supported by $f+1$ $\mathtt{WISH}$es—are similar to the ones used in Bracha’s algorithm for reliable Byzantine broadcast [11]. However, Bracha’s algorithm only makes a step upon receiving a set of identical messages. Thus, its naive application to view synchronization [41, §A.2] requires unbounded space to store the views v for which the number of received copies of $\mathtt{WISH}(v)$ still falls below the threshold required for delivery or relay. Moreover, tolerating message loss would require a process to retain a copy of every message it has broadcast, to enable retransmissions. FastSync can be viewed as specializing the mechanisms of Bracha broadcast to take advantage of the particular semantics of $\mathtt{WISH}$ messages, by keeping track of only the highest $\mathtt{WISH}$ received from each process and by acting on sets of $\mathtt{WISH}$es for non-identical views. This allows tolerating message loss before $\mathsf{GST}$ in bounded space and without compromising liveness, as illustrated by the following example.

We first show that, before $\mathsf{GST}$, we may end up in the situation where processes are split as follows: a set $P_1$ of f correct processes entered $v_1$, a set $P_2$ of f correct processes entered $v_2>v_1$, a correct process $p_i$ entered $v_2+1$, and f processes are faulty. To reach this state, assume that all correct processes manage to enter view $v_1$ and then all messages between $P_1$ and $P_2 \cup \{p_i\}$ start getting lost. The f faulty processes help the processes in $P_2 \cup \{p_i\}$ to enter all views between $v_1$ and $v_2$, by providing the required $\mathtt{WISH}$es (line 16), while the processes in $P_1$ get stuck in $v_1$. After the processes in $P_2 \cup \{p_i\}$ time out on $v_2$, they start sending $\mathtt{WISH}(v_2+1)$ (line 5), but all messages directed to processes other than $p_i$ get lost, so that the processes in $P_2$ get stuck in $v_2$. The faulty processes then help $p_i$ gather $2f+1$ messages $\mathtt{WISH}(v_2+1)$ and enter $v_2+1$ (line 16).

Assume now that $\mathsf{GST}$ occurs, the faulty processes go silent and the correct processes time out on the views they are in. Thus, the f processes in $P_1$ send $\mathtt{WISH}(v_1+1)$, the f processes in $P_2$ send $\mathtt{WISH}(v_2+1)$, and $p_i$ sends $\mathtt{WISH}(v_2+2)$ (line 10). The processes in $P_1$ eventually receive the $\mathtt{WISH}$es from $P_2 \cup \{p_i\}$, so that they set $\mathsf{view}^+= v_2+1$ and send $\mathtt{WISH}(v_2+1)$ (line 21). Note that here processes act on $f+1$ mismatching $\mathtt{WISH}$es, unlike in Bracha broadcast. Eventually, the processes in $P_1 \cup P_2$ receive 2f copies of $\mathtt{WISH}(v_2+1)$ and one $\mathtt{WISH}(v_2+2)$, which causes them to set $\mathsf{view}=v_2+1$ and enter $v_2+1$ (line 16). Note that here processes act on $2f+1$ mismatching $\mathtt{WISH}$es, again unlike in Bracha broadcast. Finally, the processes $P_1 \cup P_2$ time out and send $\mathtt{WISH}(v_2+2)$ (line 5), which allows all correct processes to enter $v_2+2$. Acting on sets of mismatching $\mathtt{WISH}$es is crucial for liveness in this example: if processes only accepted matching sets, like in Bracha broadcast, message loss before $\mathsf{GST}$ would cause them to get stuck, and they would never converge to the same view.

3.2 Correctness and latency bounds of FastSync

As we demonstrate shortly, the synchronizer specification given by Properties 1–5 in Fig. 1 serves to prove that consensus eventually reaches a decision. However, FastSync also satisfies some additional properties that allow us to quantify how quickly this happens under both favorable and unfavorable conditions. We list these properties in Fig. 2 and will explain them shortly.

Theorem 1

Consider an execution with an eventual message delay bound $\delta$, and assume that (1) holds for $u= 2\delta$. Then there exists a view ${\mathcal {V}}$ such that in this execution FastSync satisfies all the properties in Fig. 2 for $d = 2\delta$.

We prove this theorem in Sect. 4. An easy way to satisfy the premise of Theorem 1 in any execution is to pick a function $F$ that grows without bound, so that it eventually reaches $2\delta$. However, practical implementations stop increasing timeouts once they exceed a reasonable value. We can reflect this in our model using the fact that $\delta \le \Delta$ in any execution. Thus, to ensure that (1) holds for $u=N\delta$ for some $N\ge 1$, it is enough to require that the output of $F$ eventually becomes a constant $U=N\Delta$:

$$\begin{aligned} \exists v.\,\forall v'.\, v'\ge v \implies F(v') = U. \end{aligned}$$

(3)

Proposition 1

Let $\delta$ be the eventual message delay bound in some execution. Then, for all $N>0$, if (3) holds for $U=N\Delta$, then (1) holds for $u=N\delta$.

The above implies that the conclusion of Theorem 1 is satisfied provided (3) holds for $U=2\Delta$, i.e., the output of $F$ eventually becomes a known constant, and never changes afterwards.

We next describe the additional properties guaranteed by Theorem 1. Property A bounds the time for switching to the next view. This allows us to quantify the cost of switching between several views (e.g., due to faulty leaders), as formalized by the following proposition.

Proposition 2

For any v and $v'$ such that ${\mathcal {V}}\le v \le v'$,

$$\begin{aligned} E_{\mathrm{last}}(v') \le E_{\mathrm{last}}(v) + \sum \nolimits _{k=v}^{v'-1}(F(k)+\delta ). \end{aligned}$$

Proof

Given Property 3, we prove the proposition by induction on views $v' \ge v$. The base case of $v' = v$ holds trivially. For the inductive step, assume that the desired inequality holds for $v' = w \ge v$. By Property A, $E_{\mathrm{last}}(w+1) \le E_{\mathrm{last}}(w) + F(w) + \delta$. Combining this with the induction hypothesis, we get the desired inequality for $v' = w+1$:

$$\begin{aligned} E_{\mathrm{last}}(w+1)&\le E_{\mathrm{last}}(w) + F(w) + \delta \\&{} \le E_{\mathrm{last}}(v) + \sum \limits _{k=v}^{w-1}(F(k)+\delta ) + F(w) + \delta \\&{} \le E_{\mathrm{last}}(v) + \sum \limits _{k=v}^{w}(F(k)+\delta ). \end{aligned}$$

$\square$

Property B guarantees that, when the synchronizer starts after $\mathsf{GST}$ ($S_{\mathrm{first}}\ge \mathsf{GST}$) and the initial timeout is long enough ($F(1) \ge 2\delta$), processes synchronize in the very first view (${\mathcal {V}}= 1$) and enter it within $\delta$ of the last correct process calling $\mathtt{start}()$.

Let the global view at time t, denoted $\mathsf{GV}(t)$, be the maximum view entered by a correct process at or before t, or 0 if no view was entered by a correct process. Property  C quantifies the latency of view synchronization in a more general case when the synchronizer may be started before $\mathsf{GST}$. The property depends on the interval $\rho$ at which the synchronizer periodically retransmits its internal messages to deal with possible message loss. The property considers the highest view $\mathsf{GV}(\mathsf{GST}+\rho )$ a correct process has at time $\mathsf{GST}+\rho$ and ensures that all correct processes synchronize in the immediately following view within at most $\rho + F({\mathcal {V}}-1) + 3\delta$ after $\mathsf{GST}$. This is guaranteed under an assumption that the timeout of this view is at least $2\delta$, and $f+1$ correct processes call $\mathtt{start}()$ early enough. By Proposition 1, we can apply Theorem 1 if (3) holds for $U = 2\Delta$. Then $F({\mathcal {V}}-1) \le 2\Delta$, and therefore, Property  C implies $E_{\mathrm{last}}({\mathcal {V}}) \le \mathsf{GST}+ \rho + 2\Delta + 3\delta$.

In Appendix A we also analyze the FastSync latency after $\mathsf{GST}$ under the assumption that the timeout of the first view entered by a correct process after $\mathsf{GST}$ is $\le 2\delta$. We use this result to establish latency bounds assuming exponentially growing timeouts, which is a common choice in practice (e.g., [19]). In particular, we show that all correct processes are guaranteed to enter synchronized view within $O(\delta \lg {}\delta )$ after $S_{\mathrm{last}}$, if the protocol is started after $\mathsf{GST}$, and within $O(\max \{\delta \lg {}\delta , \Delta \})$ after $\mathsf{GST}+\rho$, otherwise. The latter guarantees that the latency of view synchronization is bounded after $\mathsf{GST}$.

4 Proof of FastSync correctness and latency bounds

To prove Theorem 1, in Sect. 4.1 we first prove that FastSync is a correct implementation of the synchronizer abstraction, as formalized by Properties 1–5 in Fig. 2. Then in Sect. 4.2 we prove the latency bounds stated by Properties A–C.

4.1 Proof of FastSync correctness

We now prove:

Theorem 2

Consider an execution with an eventual message delay bound $\delta$, and assume that (1) holds for $u= 2\delta$. Then there exists a view ${\mathcal {V}}$ such that in this execution FastSync satisfies Properties 1–5 in Fig. 2 for $d=2\delta$.

To prove the theorem, we first introduce the following definitions. The local view of a process $p_i$ at time t, denoted $\mathsf{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. Thus, $\mathsf{GV}(t) = \max \{\mathsf{LV}_{i}(t) \mid p_i \text {~is correct}\}$. We say that a process $p_i$ attempts to advance from a view $v \ge 0$ at time t if at this time $p_i$ executes the code in either line 3 or line 5, and $\mathsf{LV}_{i}(t) = v$.

The next three lemmas establish basic constraints on the ordering of events generated in an execution of $\textsc {FastSync}$. In particular, Lemma 2 shows that a $\mathtt{WISH}(v)$ message with $v>0$ can only be sent by a correct process if some correct process has already attempted to advance from the view $v-1$. Lemma 3 shows that a correct process can only enter a view $v>0$ if some correct process has already attempted to advance from the view $v-1$. Lemma 4 shows that some a correct process can only send a $\mathtt{WISH}$ message if some correct process has already called $\mathtt{start}$.

Lemma 2

For all times t and views $v>0$, if a correct process sends $\mathtt{WISH}(v)$ at t, then there exists a time $t' \le t$ such that some correct process attempts to advance from $v-1$ at $t'$.

Proof

We first prove the following auxiliary proposition:

$$\begin{aligned}&\forall p_i.\, \forall v.\, p_i \text {~is~correct} \wedge p_i \text {~sends~} \mathtt{WISH}(v) \text {~at~} t \implies \nonumber \\&\exists t' \le t.\, \exists v' \ge v-1.\, \exists p_j.\, p_j \text {~is~correct} \wedge {} \nonumber \\&p_j \text {~attempts~to~advance~from~} v' \text {~at~} t'. \end{aligned}$$

(4)

By contradiction, assume that a correct process $p_i$ sends $\mathtt{WISH}(v)$ at t, but for all $t' \le t$ and all $v' \ge v-1$, no correct process attempts to advance from $v'$ at $t'$. Consider the earliest time $t_k$ when some correct process $p_k$ sends a $\mathtt{WISH}(v_k)$ with $v_k \ge v$, so that $t_k \le t$. Then either $v_k = p_k.\mathsf{view}^+(t_k)$ or $p_k.\mathsf{view}(t_k) = p_k.\mathsf{view}^+(t_k) = v_k - 1$. If $p_k.\mathsf{view}^+(t_k) = v_k \ge v$, then $p_k.\mathsf{max\_views}(t_k)$ includes $f+1$ entries $\ge v_k \ge v$, and therefore, there exists a correct process $p_l$ that sent $\mathtt{WISH}(v')$ with $v' \ge v$ at $t_l < t_k$, contradicting the assumption that $t_k$ is the earliest time when this can happen. Suppose that $p_k.\mathsf{view}(t_k) = p_k.\mathsf{view}^+(t_k) = v_k - 1$. Then at $t_k$ the process $p_k$ executes either line 5 or line 10 and $\mathsf{LV}_{k}(t_k) = v_k - 1$. If $p_k$ executes line 5 at $t_k$, then since $\mathsf{LV}_{k}(t_k) = v_k - 1$, $p_k$ attempts to advance from $v_k-1 \ge v-1$ at $t_k\le t$, contradicting our assumption that no such attempt can occur.

Suppose now that $p_k$ executes the code in line 10 at $t_k$ and $p_k.\mathsf{view}(t_k) = p_k.\mathsf{view}^+(t_k) = v_k - 1$. Consider first the case when $v_k = 1$. Since $\mathsf{max\_views}[k] > 0$, $p_k$ has already sent $\mathtt{WISH}(v_k')$ for some view $v_k' \ge 1$ at a time $< t_k$. Since $v_k' \ge v_k \ge v$, this is a contradiction to our assumption that no $\mathtt{WISH}$ messages with views $\ge v$ can be sent before $t_k$. It remains to consider the case when $v_k > 1$. Then $E_{k}(v_k-1)$ is defined and satisfies $E_{k}(v_k-1) < t_k$. Thus, $p_k.\mathsf{view}(E_{k}(v_k-1)) = p_k.\mathsf{view}^+(E_{k}(v_k-1)) = v_k - 1$. Since $p_k$ starts $p_k.\mathsf{timer\_view}$ at $E_{k}(v_k-1)$, and $p_k.\mathsf{timer\_view}(t_k)$ is not enabled, there exists a time $t_k'$ such that $E_{k}(v_k-1)< t_k' < t_k$ and $p_k.\mathsf{timer\_view}$ expires at $t_k'$, triggering the execution of the $\mathsf{timer\_view}$ expiration handler. Since both $p_k.\mathsf{view}$ and $p_k.\mathsf{view}^+$ are non-decreasing, and both are equal to $v_k - 1$ at $E_{k}(v_k-1)$ as well as $t_k$, $p_k.\mathsf{view}(t_k') = p_k.\mathsf{view}^+(t_k') = v_k - 1$. Thus, $\mathsf{LV}_{k}(t_k') = v_k-1$, which implies that at $t_k' < t_k \le t$, $p_k$ attempts to advance from $v_k-1 \ge v - 1$, contradicting our assumption that no such attempt can happen. We conclude that (4) holds.

We now prove the lemma. Let t and v be such that some correct process sends $\mathtt{WISH}(v)$ at t. By (4), there exists a correct process that attempts to advance from a view $\ge v-1$ at or before t. Let $t'$ be the earliest time when some correct process attempts to advance from a view $\ge v-1$, and let $p_j$ be this process and $v' \ge v-1$ be the view from which $p_j$ attempts to advance at $t'$. Thus, at $t'$, $p_j$ executes the code in either line 3 or line 5, and $\mathsf{LV}_{j}(t') = v' \ge v - 1$. Suppose first that $p_j$ executes the code in line 5 at $t'$. Since $\mathsf{LV}_{j}(t') = v'$, there exists an earlier time at which $p_j.\mathsf{view}^+= p_j.\mathsf{view}= v'$. Since $p_j.\mathsf{view}^+$ is non-decreasing, $p_j.\mathsf{view}^+(t') \ge v'$. If $p_j.\mathsf{view}^+(t') > v'$, then given that $v' \ge v - 1$, $p_j.\mathsf{view}^+(t') \ge v$. Thus, there exists a correct process $p_k$ and time $t'' < t'$ such that $p_k$ sent $\mathtt{WISH}(v'')$ with $v'' \ge v$ to $p_j$ at $t''$. By (4), there exists a time $\le t'' < t'$ at which some correct process attempts to advance from a view $\ge v''-1 \ge v-1$, which is impossible. Thus, $p_j.\mathsf{view}^+(t') = v'$. Since $\mathsf{LV}_{j}(t') = v'$, we have $p_j.\mathsf{view}(t') = p_j.\mathsf{view}^+(t') = v'$. Suppose now that $p_j$ executes the code in line 3. Then $p_j.\mathsf{view}^+(t') = p_j.\mathsf{view}(t') = 0 = \mathsf{LV}_{j}(t') = v'$. Hence, in both cases

$$\begin{aligned} p_j.\mathsf{view}(t') = p_j.\mathsf{view}^+(t') = v' \ge v - 1. \end{aligned}$$

By the definitions of $\mathsf{view}$ and $\mathsf{view}^+$, $v'$ is both the lowest view among the highest $2f+1$ views in $p_j.\mathsf{max\_views}(t')$, and the lowest view among the highest $f+1$ views in $p_j.\mathsf{max\_views}(t')$. Hence, $p_j.\mathsf{max\_views}(t')$ includes $f+1$ entries equal to $v'$, and therefore, there exists a correct process $p_k$ such that

$$\begin{aligned}&p_j.\mathsf{view}(t') = p_j.\mathsf{view}^+(t') {}\nonumber \\&\quad = p_j.\mathsf{max\_views}[k](t') = v' \ge v-1. \end{aligned}$$

(5)

Also, for all correct processes $p_l$, $p_j.\mathsf{max\_views}[l](t') < v$: otherwise, some correct process sent $\mathtt{WISH}(v'')$ with $v'' \ge v$ at a time $< t'$, and therefore, by (4), some correct process attempted to advance from a view $\ge v-1$ earlier than $t'$, which is impossible. Thus,

$$\begin{aligned} p_j.\mathsf{view}(t') = p_j.\mathsf{view}^+(t') = p_j.\mathsf{max\_views}[k](t') < v. \end{aligned}$$

Together with (5), this implies

$$\begin{aligned} p_j.\mathsf{view}(t') = p_j.\mathsf{view}^+(t') = v - 1. \end{aligned}$$

Hence, $\mathsf{LV}_{j}(t') = v - 1$, and therefore, $p_j$ attempts to advance from $v-1$ at $t'$. Thus, $v' = v-1$ and $t' \le t$, as required. $\square$

Lemma 3

If a correct process $p_i$ enters a view v, then there exists a time $t < E_{i}(v)$ at which some correct process attempts to advance from $v-1$.

Proof

Since $p_i$ enters a view v, we have $p_i.\mathsf{view}(E_{i}(v)) = p_i.\mathsf{view}^+(E_{i}(v))=v$. By the definitions of $\mathsf{view}$ and $\mathsf{view}^+$, v is both the lowest view among the highest $2f+1$ views in $p_i.\mathsf{max\_views}(E_{i}(v))$, and the lowest view among the highest $f+1$ views in $p_i.\mathsf{max\_views}(E_{i}(v))$. Hence, $p_i.\mathsf{max\_views}(E_{i}(v))$ includes $f+1$ entries equal to v. Then there exists a time $t' < E_{i}(v)$ at which some correct process sends $\mathtt{WISH}(v)$. Hence, by Lemma 2, there exists a time $t \le t' < E_{i}(v)$ at which some correct process attempts to advance from $v-1$. $\square$

Lemma 4

For all times t and views $v>0$, if a correct process sends $\mathtt{WISH}(v)$ at t, then there exists a time $t' \le t$ such that some correct process calls $\mathtt{start}$ at $t'$.

Proof

Consider the earliest time $t_k \le t$ at which some correct process $p_k$ sends $\mathtt{WISH}(v_k)$ for some view $v_k$. By Lemma 2, there exists a time $t_j \le t_k$ at which some correct process attempts to advance from $v_k - 1 \ge 0$, and therefore, sends $\mathtt{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 3, some correct process attempts to advance from $v_k - 2$ by sending $\mathtt{WISH}(v_k - 1)$ earlier than $t_j = t_k$, which cannot happen. Thus, at $t_k$, $p_k$ attempts to advance from view 0, so that $v_k = 1$ and $\mathsf{LV}_{k}(t_k) = 0$. Assume first that $p_k$ executes the code in line 5 at $t_k$. Then $p_k.\mathsf{timer\_view}$ expires at $t_k$, and hence, there exists a time $s_k < t_k$ such that $p_k.\mathsf{timer\_view}$ is set at $s_k$. Thus, at $s_k$, $p_k$ enters a view $>0$. Since $\mathsf{LV}$ is non-decreasing, $\mathsf{LV}_{k}(t_k) > 0$, which is a contradiction. Thus, $p_k$ cannot execute line 5 at $t_k$, and has to call $\mathtt{start}$ at this time. $\square$

By Lemma 3, no correct process can enter a view before some correct process sends a $\mathtt{WISH}$ message. Since, by Lemma 4, this cannot happen before some correct process calls $\mathtt{start}$, we have

Corollary 1

$\forall v.\, S_{\mathrm{first}}< E_{\mathrm{first}}(v)$.

We now prove that the views entered by correct processes throughout an execution of FastSync do not skip values, as stipulated by Lemma 1 (Sect. 3.1).

Proof of Lemma 1

Fix $v'$ such that $v' \ge 2$ and assume that a correct process enters $v'$, so that $E_{\mathrm{first}}(v')$ is defined. We prove by induction on k that for each $k=0..(v'-1)$ some correct enters $v'-k$ no later than $E_{\mathrm{first}}(v')$. The base case of $k=0$ is trivial. For the inductive step, assume that the required holds for some k, so that $E_{\mathrm{first}}(v'-k) \le E_{\mathrm{first}}(v')$. Then by Lemma 3, there exists a time $t < E_{\mathrm{first}}(v'-k)$ at which some correct process $p_j$ attempts to advance from $v'-k-1$. But then $p_j$’s local view at t is $v'-k-1$. Hence, $p_j$ enters $v'-k-1$ before $t < E_{\mathrm{first}}(v'-k) \le E_{\mathrm{first}}(v')$, as required. $\square$

Lemma  5 below establishes that the views sent in the $\mathtt{WISH}$ messages by the same process can only increase. Its proof relies on the next proposition, stating a few simple invariants that follow immediately from the structure of the code and our assumption that every message sent by a process is instantaneously delivered to the sender (Sect. 3).

Proposition 3

Let $p_i$ be a correct process. The following conditions hold at all times in every execution of $\textsc {FastSync}$:

• 1. $\forall v.\forall t.\, p_i \text {~sends~} \mathtt{WISH}(v) \text {~at~} t {\implies }$ $v \in \{p_i.\mathsf{view}^+(t), p_i.\mathsf{view}^+(t)+1\}$.

• 2. $\forall v.\forall t.\, p_i \text {~sends~} \mathtt{WISH}(v) \text {~at~} t \wedge v = p_i.\mathsf{view}^+(t)+1 {\implies }p_i.\mathsf{view}^+(t)=\! \! p_i.\mathsf{view}(t) \wedge (p_i.\mathsf{timer\_view}\text {~is~disabled})$.

• 3. $\forall v.\forall t.\, p_i \text {~sends~} \mathtt{WISH}(v) \text {~at~} t {\implies }$ $\forall t'> t.\, p_i.\mathsf{max\_views}[i](t')> 0 \wedge p_i.\mathsf{view}^+(t') > 0$.

Lemma 5

For all views $v, v' > 0$, if a correct process sends $\mathtt{WISH}(v)$ before sending $\mathtt{WISH}(v')$, then $v \le v'$.

Proof

Let s and $s'$ such that $s < s'$ be the times at which a correct process $p_i$ sends $\mathtt{WISH}(v)$ and $\mathtt{WISH}(v')$ messages, respectively. We show that $v' \ge v$. By Proposition 3(1), $v \in \{p_i.\mathsf{view}^+(s), p_i.\mathsf{view}^+(s)+1\}$ and $v' \in \{p_i.\mathsf{view}^+(s'), p_i.\mathsf{view}^+(s')+1\}$. Hence, if $v = p_i.\mathsf{view}^+(s)$ or $v' = p_i.\mathsf{view}^+(s')+1$, then we get $v \le v'$ from the fact that $p_i.\mathsf{view}^+$ is non-decreasing. It thus remains to consider the case when $v = p_i.\mathsf{view}^+(s)+1$ and $v' = p_i.\mathsf{view}^+(s')$. In this case by Proposition 3(2), $p_i.\mathsf{view}^+(s)=p_i.\mathsf{view}(s)$ and $p_i.\mathsf{timer\_view}(s)$ is disabled. We now consider several cases depending on the line at which $\mathtt{WISH}(v')$ is sent.

• $\mathtt{WISH}(v')$ is sent at line 3. In this case we have $v' = 1$ and $p_i.\mathsf{view}^+(s') = 0$, so that $v' = p_i.\mathsf{view}^+(s') + 1$. But this contradicts the assumption that $v'=p_i.\mathsf{view}^+(s')$, and thus this case is impossible.

• $\mathtt{WISH}(v')$ is sent at lines 5 or 10. Then $v'=p_i.\mathsf{view}^+(s')=\max (p_i.\mathsf{view}(s')+1, p_i.\mathsf{view}^+(s'))$. Since $p_i.\mathsf{view}$ is non-decreasing, we get $p_i.\mathsf{view}^+(s') \ge p_i.\mathsf{view}(s')+1 > p_i.\mathsf{view}(s') \ge p_i.\mathsf{view}(s) = p_i.\mathsf{view}^+(s)$. Hence, $p_i.\mathsf{view}^+(s') > p_i.\mathsf{view}^+(s)$, and therefore, $v'=p_i.\mathsf{view}^+(s') \ge p_i.\mathsf{view}^+(s)+1=v$, as required.

• $\mathtt{WISH}(v')$ is sent at line 8. Then $p_i.\mathsf{timer\_view}(s')$ is enabled. Since $p_i.\mathsf{timer\_view}(s)$ is disabled, there exists a time $s''$ such that $s< s'' < s'$ and $p_i$ enters a view at $s''$. By the view entry condition $p_i.\mathsf{view}(s'') > p_i.\textit{prev\_v}(s'')$. Since $p_i.\mathsf{view}$ is non-decreasing, we get $p_i.\mathsf{view}^+(s') \ge p_i.\mathsf{view}(s') \ge p_i.\mathsf{view}(s'') > p_i.\mathsf{view}(s) = p_i.\mathsf{view}^+(s)$. Thus, $p_i.\mathsf{view}^+(s') > p_i.\mathsf{view}^+(s)$ and therefore, $v' = p_i.\mathsf{view}^+(s') \ge p_i.\mathsf{view}^+(s)+1 = v$, as required.

• $\mathtt{WISH}(v')$ is sent at line 21. Then $p_i.\mathsf{view}^+(s') > p_i.\textit{prev\_v}^+(s') \ge p_i.\mathsf{view}^+(s)$, and therefore, $v' = p_i.\mathsf{view}^+(s') \ge p_i.\mathsf{view}^+(s) + 1 = v$, as required.$\square$

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

$$\begin{aligned} \overline{\mathsf{GST}}= {\left\{ \begin{array}{ll} \mathsf{GST}+ \rho ,&{} \text {if } S_{\mathrm{first}}< \mathsf{GST};\\ S_{\mathrm{first}},&{} \text {otherwise}. \end{array}\right. } \end{aligned}$$

From this definition it follows that

$$\begin{aligned} \overline{\mathsf{GST}}\ge \mathsf{GST}. \end{aligned}$$

(6)

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

Lemma 6

For all correct processes $p_i$, times $t \ge \overline{\mathsf{GST}}$, and views v, if $p_i$ sends $\mathtt{WISH}(v)$ at a time $\le t$, then there exists a view $v' \ge v$ and a time $t'$ such that $\mathsf{GST}\le t' \le t$ and $p_i$ sends $\mathtt{WISH}(v')$ at $t'$.

Proof

Let $s \le t$ be the time at which $p_i$ sends $\mathtt{WISH}(v)$. We consider two cases. Suppose first that $S_{\mathrm{first}}\ge \mathsf{GST}$. By Lemma 4, $s \ge S_{\mathrm{first}}$, and therefore, $\mathsf{GST}\le s \le t$. Thus, choosing $t'=s$ and $v' = v$ validates the lemma. Suppose next that $S_{\mathrm{first}}< \mathsf{GST}$. Then by the definition of $\overline{\mathsf{GST}}$, $t \ge \mathsf{GST}+ \rho$. If $s \ge \mathsf{GST}$, then $\mathsf{GST}\le s \le t$, and therefore, choosing $t'=s$ and $v' = v$ validates the lemma. Assume now that $s < \mathsf{GST}$. Since after $\mathsf{GST}$ the $p_i$’s local clock advances at the same rate as real time, there exists a time $s'$ satisfying $\mathsf{GST}\le s' \le t$ such that $p_i$ executes the periodic retransmission code in lines 6–10 at $s'$. Since $p_i$ already sent a $\mathtt{WISH}$ message at $s < \mathsf{GST}\le s'$, by Proposition 3(3), $p_i.\mathsf{max\_views}[i](s') > 0$, and therefore, the code sending a $\mathtt{WISH}$ message is guaranteed to be reached at $s'$. Thus, there exists $v'$ such that $p_i$ sends $\mathtt{WISH}(v')$ at $s'$ by executing the code in either line 8 or line 10, and $\mathsf{GST}\le s' \le t$. By Lemma 5, $v' \ge v$, which implies the required. $\square$

We next state several lemmas that encapsulate the arguments showing the various properties in Fig. 2. The following lemma is used to prove Property 5.

Lemma 7

If a correct process enters a view $v>0$ and $E_{\mathrm{first}}(v) \ge \mathsf{GST}$, then for all $v' > v$, no correct process attempts to advance from $v'-1$ before $E_{\mathrm{first}}(v) + F(v)$.

Proof

Suppose by contradiction that there exists a time $t' < E_{\mathrm{first}}(v) + F(v)$ and a correct process $p_i$ such that $p_i$ attempts to advance from $v'-1 > v-1$ at $t'$. If $p_i$ executes the code in line 3 at $t'$, then $\mathsf{LV}_{i}(t') = 0 = v'-1 > v - 1 \ge 0$, which is impossible. Thus, at $t'$ the process $p_i$ executes the code in line 5, and $\mathsf{LV}_{i}(t') = v' - 1$. Since $p_i.\mathsf{timer\_view}$ is not enabled at $t'$, $p_i$ must have entered $v' - 1$ at least $F(v)$ before $t'$ according to its local clock. Since $v' - 1 \ge v$, by Lemma 1 we have $E_{\mathrm{first}}(v' - 1) \ge E_{\mathrm{first}}(v) \ge \mathsf{GST}$. Therefore, given that the clocks of all correct processes progress at the same rate as real time after $\mathsf{GST}$, we get

$$\begin{aligned} E_{\mathrm{first}}(v) \le E_{\mathrm{first}}(v' - 1) \le t' - F(v' - 1). \end{aligned}$$

Hence,

$$\begin{aligned} t' \ge E_{\mathrm{first}}(v) + F(v' - 1). \end{aligned}$$

Since $F$ is non-decreasing and $v' - 1 \ge v$, we have $F(v' - 1) \ge F(v)$, so that

$$\begin{aligned} t' \ge E_{\mathrm{first}}(v) + F(v), \end{aligned}$$

which contradicts our assumption that $t' < E_{\mathrm{first}}(v) + F(v)$. This contradiction shows the required. $\square$

Corollary 2

Consider a view v and assume that v is entered by a correct process. If $E_{\mathrm{first}}(v) \ge \mathsf{GST}$, then a correct process cannot send a $\mathtt{WISH}(v')$ with $v' > v$ earlier than $E_{\mathrm{first}}(v) + F(v)$.

Proof

Assume a correct process sends a $\mathtt{WISH}(v')$ with $v' > v$ at time $t'$. By Lemma 2, there exists a time $s \le t'$ such that some correct process $p_i$ attempts to advance from $v'-1 > v-1$ at s. By Lemma 7, $s \ge E_{\mathrm{first}}(v) + F(v)$, which implies that $t' \ge s \ge E_{\mathrm{first}}(v) + F(v)$, as required. $\square$

The following lemma is used to prove Property 4 for $d = 2\delta$.

Lemma 8

Consider a view $v>0$ and assume that v is entered by a correct process. If $E_{\mathrm{first}}(v) \ge \overline{\mathsf{GST}}$ and $F(v)\ge 2\delta$, then all correct processes enter v and $E_{\mathrm{last}}(v) \le E_{\mathrm{first}}(v) + 2\delta$.

Proof

Since $E_{\mathrm{first}}(v) \ge \overline{\mathsf{GST}}$, by (6), $E_{\mathrm{first}}(v)\ge \mathsf{GST}$. Since $F(v)\ge 2\delta$, Corollary 2 implies that no correct process can send $\mathtt{WISH}(v')$ with $v' > v$ earlier than $E_{\mathrm{first}}(v) + 2\delta$. Once any such $\mathtt{WISH}(v')$ is sent, it will take a non-zero time until it is received by any correct process. Thus, we have:

• (*) no correct process receives $\mathtt{WISH}(v')$ with $v' > v$ from a correct process until after $E_{\mathrm{first}}(v) + 2\delta$.

Let $p_i$ be a correct process that enters v at $E_{\mathrm{first}}(v)$. By the view entry condition, $p_i.\mathsf{view}(E_{\mathrm{first}}(v)) = v$, and therefore $p_i.\mathsf{max\_views}(E_{\mathrm{first}}(v))$ includes $2f+1$ entries $\ge 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 $\mathtt{WISH}(v)$ to all processes before $E_{\mathrm{first}}(v)$.

Since $E_{\mathrm{first}}(v) \ge \overline{\mathsf{GST}}$, by Lemma 6, every $p_j \in C$ also sends $\mathtt{WISH}(v')$ with $v'\ge v$ at some time $s_j$ such that $\mathsf{GST}\le s_j \le E_{\mathrm{first}}(v)$. Then by (*) we have $v'=v$. It follows that each $p_j \in C$ is guaranteed to send $\mathtt{WISH}(v)$ to all correct processes between $\mathsf{GST}$ and $E_{\mathrm{first}}(v)$. Since all messages sent by correct processes after $\mathsf{GST}$ are guaranteed to be received by all correct processes within $\delta$ of their transmission, by $E_{\mathrm{first}}(v) + \delta$ all correct processes will receive $\mathtt{WISH}(v)$ from at least $f+1$ correct processes.

Consider an arbitrary correct process $p_j$ and let $t_j \le E_{\mathrm{first}}(v) + \delta$ be the earliest time by which $p_j$ receives $\mathtt{WISH}(v)$ from $f+1$ correct processes. By (*), no correct process sends $\mathtt{WISH}(v')$ with $v' > v$ before $t_j < E_{\mathrm{first}}(v) + 2\delta$. Thus, $p_j.\mathsf{max\_views}(t_j)$ includes at least $f+1$ entries equal to v and at most f entries $>v$, so that $p_j.\mathsf{view}^+(t_j) = v$. Then $p_j$ sends $\mathtt{WISH}(v)$ to all processes no later than $t_j \le E_{\mathrm{first}}(v) + \delta$. Since $E_{\mathrm{first}}(v) \ge \overline{\mathsf{GST}}$, by Lemma 6, $p_j$ also sends $\mathtt{WISH}(v')$ with $v'\ge v$ in-between $\mathsf{GST}$ and $E_{\mathrm{first}}(v) + \delta$. By (*), $v'=v$, and therefore, $p_j$ sends $\mathtt{WISH}(v)$ to all processes sometime between $\mathsf{GST}$ and $E_{\mathrm{first}}(v) + \delta$. Hence, all correct processes are guaranteed to send $\mathtt{WISH}(v)$ to all correct processes between $\mathsf{GST}$ and $E_{\mathrm{first}}(v) + \delta$.

Consider an arbitrary correct process $p_k$ and let $t_k \le E_{\mathrm{first}}(v) + 2\delta$ be the earliest time by which $p_k$ receives $\mathtt{WISH}(v)$ from all correct processes. Then by (*), all entries of correct processes in $p_k.\mathsf{max\_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.\mathsf{max\_views}(t_k)$ are equal to v, and (ii) one of the $f+1$ highest entries in $p_k.\mathsf{max\_views}(t_k)$ is equal to v. From (i), $p_k.\mathsf{view}^+(t_k) \ge p_k.\mathsf{view}(t_k) \ge v$, and from (ii), $p_k.\mathsf{view}(t_k) \le p_k.\mathsf{view}^+(t_k) \le v$. Therefore, $p_k.\mathsf{view}(t_k) = p_k.\mathsf{view}^+(t_k) = v$, so that $p_k$ enters v no later than $t_k \le E_{\mathrm{first}}(v)+2\delta$. We have thus shown that by $E_{\mathrm{first}}(v)+2\delta$, all correct processes enter v, as required. $\square$

The following lemma shows that processes keep entering new views forever. This is used to prove Property 3.

Lemma 9

For all views v, there exists a view $v' > v$ such that some correct process eventually enters $v'$.

Proof

Assume by contradiction that the required does not hold and let v be the maximal view entered by a correct process; if there are no such views, we let $v=0$. Thus, we have

$$\begin{aligned} \forall t.\, \forall v' \!\ge \!v \!+ \!1.\, \forall p_i.\, \lnot (p_i \text {~enters~} v' \text {~at~} t \wedge p_i \text {~is~correct}). \end{aligned}$$

(7)

If there is a correct process that sends $\mathtt{WISH}(v')$ with $v' > v + 1$ at any time s, then by Lemma 2, a correct process $p_i$ attempts to advance from $v' - 1 > v$ at some time $s' \le s$. Thus, $\mathsf{LV}_{i}(s') = v' - 1 \ge v + 1 \ge 1$, which contradicts (7). Thus, we have

$$\begin{aligned} \forall t.\, \forall v' > v + 1.\, \forall p_i.\, \lnot (&p_i \text {~sends~} \mathtt{WISH}(v') \text {~at~} t \wedge {} \nonumber \\&p_i \text {~is~correct}). \end{aligned}$$

(8)

Since we assume that all correct processes eventually call $\mathtt{start}$, there exists a time $T_1=\max \{E_{\mathrm{first}}(v), \overline{\mathsf{GST}}, S_{\mathrm{last}}\}$. We consider two cases.

Suppose first that $v=0$, so that no correct process enters any view. Consider a correct process $p_i$. This process must call $\mathtt{start}$ at some time $t_i \le T_1$. If $p_i.\mathsf{view}^+= 0$ at $t_i$, then $p_i$ sends $\mathtt{WISH}(1)$ at $t_i$. On the other hand, if $p_i.\mathsf{view}^+> 0$ at $t_i$, then $p_i$ has already sent $\mathtt{WISH}(v')$ with $v'=p_i.\mathsf{view}^+>0$ when $p_i.\mathsf{view}^+$ first became $>0$ at some time before $t_i$. By (8), $v'=1$. Thus, in both cases, there exists a time $t_i' \le T_1$ such that $p_i$ sends $\mathtt{WISH}(1)$ at $t_i'$. Since $T_1 \ge \overline{\mathsf{GST}}$, by Lemma 6, there exists a view $v''\ge 1$ and a time $s_i$ such that $\mathsf{GST}\le s_i \le T_1$ and $p_i$ sends $\mathtt{WISH}(v'')$ at $s_i$. By (8), $v''=1$. Since the links are reliable after $\mathsf{GST}$, $\mathtt{WISH}(1)$ sent by $p_i$ at $s_i$ will be received by all correct processes. Thus, there exists a time $T_2 \ge T_1$ and a correct process $p_j$ such that $p_j$ receives $\mathtt{WISH}(1)$ from all correct processes at $t_j \le T_2$. By (8), all entries of correct processes in $p_j.\mathsf{max\_views}(t_j)$ are equal to 1. Since there are at least $2f+1$ correct processes: (i) at least $2f+1$ entries in $p_l.\mathsf{max\_views}(t_l)$ are equal to 1, and (ii) one of the $f+1$ highest entries in $p_l.\mathsf{max\_views}(t_l)$ is equal to 1. From (i), $p_l.\mathsf{view}^+(t_l) \ge p_l.\mathsf{view}(t_l) \ge 1$, and from (ii), $p_l.\mathsf{view}(t_l) \le p_l.\mathsf{view}^+(t_l) \le 1$. Hence, $p_l.\mathsf{view}(t_l) = p_l.\mathsf{view}^+(t_l) = 1$, and therefore, $p_j$ enters view 1 at $t_j$, contradicting (7).

Next, suppose $v > 0$. Then some correct process entered v, and thus there exists a set C consisting of $f+1$ correct processes all of which sent $\mathtt{WISH}(v')$ with $v'\ge v$ before $T_1$. Consider $p_i\in C$ and let $t_i \le T_1$ be a time such that at $t_i$ the process $p_i$ sends $\mathtt{WISH}(v_i)$ with $v_i \ge v$. Since $T_1 \ge \overline{\mathsf{GST}}$, by Lemma 6, there exists a view $v_i'\ge v_i$ and a time $s_i$ such that $\mathsf{GST}\le s_i \le T_1$ and $p_i$ sends $\mathtt{WISH}(v_i')$ at $s_i$. By (8), we have $v_i' \in \{v, v+1\}$. Since the links are reliable after $\mathsf{GST}$, the $\mathtt{WISH}(v_i')$ sent by $p_i$ at $s_i$ will be received by all correct processes.

Thus, there exists a time $T_2 \ge T_1 \ge \overline{\mathsf{GST}}$ by which all correct processes have received $\mathtt{WISH}(v')$ with $v' \in \{v, v+1\}$ from all processes in C. Consider an arbitrary correct process $p_j$. By (8), the entry of every process in C in $p_j.\mathsf{max\_views}(T_2)$ is equal to either v or $v+1$. Since $|C|\ge f+1$ and all processes in C are correct, $p_j.\mathsf{max\_views}(T_2)$ includes at least $f+1$ entries $\ge v$. Thus, $p_j.\mathsf{view}^+(T_2) \ge v$, and therefore, $p_j$ sends $\mathtt{WISH}(v_j)$ with $v_j \ge v$ no later than at $T_2$. Since $T_2 \ge \overline{\mathsf{GST}}$, by Lemma 6, there exists a view $v_j'\ge v_j$ and a time $s_j$ such that $\mathsf{GST}\le s_j \le t_j$ and $p_j$ sends $\mathtt{WISH}(v_j')$ at $s_j$. By (8), $v_j' \in \{v, v+1\}$. Since the links are reliable after $\mathsf{GST}$, the $\mathtt{WISH}(v_j')$ sent by $p_j$ at $s_j$ will be received by all correct processes.

Thus, there exists a time $T_3 \ge T_2 \ge \overline{\mathsf{GST}}$ by which all correct processes have received $\mathtt{WISH}(v')$ with $v' \in \{v, v+1\}$ from all correct processes. Consider an arbitrary correct process $p_k$. Then at $T_3$, all entries of correct processes in $p_k.\mathsf{max\_views}$ are $\ge v$. By (8), 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_l.\mathsf{max\_views}(T_3)$ are $\ge v$, and (ii) one of the $f+1$ highest entries in $p_k.\mathsf{max\_views}(T_3)$ is $\le v+1$. From (i), $p_k.\mathsf{view}^+(T_3) \ge p_k.\mathsf{view}(T_3) \ge v$, and from (ii), $p_k.\mathsf{view}(T_3) \le p_k.\mathsf{view}^+(T_3) \le v+1$. Hence, $p_k.\mathsf{view}(T_3), p_k.\mathsf{view}^+(T_3) \in \{v, v+1\}$. Since no correct process enters $v+1$, $p_k.\mathsf{view}(T_3)$ and $p_k.\mathsf{view}^+(T_3)$ cannot be both simultaneously equal to $v+1$. Thus, $p_k.\mathsf{view}(T_3) = v$, and either $p_k.\mathsf{view}^+(T_3) = v$ or $p_k.\mathsf{view}^+(T_3)=v+1$. If $p_k.\mathsf{view}^+(T_3) = v+1$, then $p_k$ has sent $\mathtt{WISH}(v_k)$ with $v_k=v+1$ when $p_k.\mathsf{view}^+$ has first become equal to $v+1$ sometime before $T_3$. On the other hand, if $p_k.\mathsf{view}(T_3) = p_k.\mathsf{view}^+(T_3) = v$, then $p_k$ has entered v and started $p_k.\mathsf{timer\_view}$ at or before $T_3$. Since $p_k$ does not enter any higher views, $p_k.\mathsf{timer\_view}$ will eventually expire, causing $p_k$ to send $\mathtt{WISH}(v_k)$ with $v_k > v$. By (8), $v_k=v+1$. Thus, there exists a time $t_k \ge T_3$ by which $p_k$ sends $\mathtt{WISH}(v+1)$ to all processes. Since $t_k \ge T_3 \ge \overline{\mathsf{GST}}$, by Lemma 6, there exists a view $v'_k\ge v+1$ and a time $s_k$ such that $\mathsf{GST}\le s_k \le T_3$ and $p_k$ sends $\mathtt{WISH}(v'_k)$ at $s_k$. By (8), $v'_k=v+1$. Since the links are reliable after $\mathsf{GST}$, the $\mathtt{WISH}(v+1)$ sent by $p_k$ will be received by all correct processes.

Thus, there exists a time $T_4 \ge T_3 \ge \overline{\mathsf{GST}}$ by which all correct processes have received $\mathtt{WISH}(v+1)$ from all correct processes. Fix an arbitrary correct process $p_l$. By (8), all entries of correct processes in $p_l.\mathsf{max\_views}(T_4)$ are equal to $v+1$. Since there are at least $2f+1$ correct processes: (i) at least $2f+1$ entries in $p_l.\mathsf{max\_views}(T_4)$ are equal to $v+1$, and (ii) one of the $f+1$ highest entries in $p_l.\mathsf{max\_views}(T_4)$ is equal to $v+1$. From (i), $p_l.\mathsf{view}^+(T_4) \ge p_l.\mathsf{view}(T_4) \ge v+1$, and from (ii), $p_l.\mathsf{view}(T_4) \le p_l.\mathsf{view}^+(T_4) \le v+1$. Hence, $p_l.\mathsf{view}(T_4) = p_l.\mathsf{view}^+(T_4) = v+1$, and therefore, $p_l$ enters $v+1$ by $T_4$, contradicting (7). $\square$

From Lemmas 9 and 1 we get

Corollary 3

For any view v, some correct process enters v.

Finally, the following lemma gives the core argument for the proof of Theorem 2.

Lemma 10

Consider an execution with an eventual message delay bound $\delta$ and a view ${\mathcal {V}}$ such that

$$\begin{aligned} {\mathcal {V}}\ge \mathsf{GV}(\overline{\mathsf{GST}}) + 1 \wedge F({\mathcal {V}}) \ge 2\delta . \end{aligned}$$

(9)

Then in this execution FastSync satisfies Properties 1–5 in Fig. 2 for $d=2\delta$.

Proof

Property 1 is satisfied trivially. Consider a view ${\mathcal {V}}$ such that (9) holds. By Corollary 3, some correct process enters ${\mathcal {V}}$, so that $E_{\mathrm{first}}({\mathcal {V}})$ is defined. Since $\mathsf{GV}$ is non-decreasing and ${\mathcal {V}}\ge \mathsf{GV}(\overline{\mathsf{GST}}) + 1$, no correct process can enter ${\mathcal {V}}$ until after $\overline{\mathsf{GST}}$. Thus, we get that $E_{\mathrm{first}}({\mathcal {V}}) \ge \overline{\mathsf{GST}}$.

Fix a view $v \ge {\mathcal {V}}$. By Corollary 3, some correct process enters v. Then by Lemma 1 and (6) we get

$$\begin{aligned} \forall v\ge {\mathcal {V}}.\, E_{\mathrm{first}}(v) \ge E_{\mathrm{first}}({\mathcal {V}}) \ge \overline{\mathsf{GST}}\ge \mathsf{GST}. \end{aligned}$$

(10)

Then Property 2 holds. Since $F$ is a non-decreasing function, $\forall v\ge {\mathcal {V}}.\, F(v) \ge F({\mathcal {V}}) \ge 2\delta$. Thus, from (10) and Lemma 8, all correct processes enter v and $E_{\mathrm{last}}(v) \le E_{\mathrm{first}}(v) + 2\delta$. This validates Properties 3 and 4 for $d=2\delta$.

It remains to prove Property 5. By Corollary 3, some correct process enters view $v+1$. Then by Lemma 3 there exist a time $t < E_{\mathrm{first}}(v+1)$ at which some correct process attempts to advance from v. By (10), $E_{\mathrm{first}}(v) \ge \mathsf{GST}$. Then by Lemma 7 we get $t \ge E_{\mathrm{first}}(v) + F(v)$, which implies $E_{\mathrm{first}}(v+1) > t \ge E_{\mathrm{first}}(v) + F(v)$, as required. We thus conclude that FastSync satisfies Properties 1–5 in Fig. 2 for $d = 2\delta$, as needed. $\square$

Proof of Theorem 2

Consider an execution of FastSync and let $\delta$ be the eventual message delay bound in this execution. Then (1) for $u = 2\delta$ implies that $F(v') \ge 2\delta$ for some view $v'$. Since $F$ is monotone, ${\mathcal {V}}= \max \{v', \mathsf{GV}(\overline{\mathsf{GST}}) + 1\}$ satisfies (9). Then the required follows from Lemma 10. $\square$

4.2 Proof of FastSync latency bounds

We next extend the proof of FastSync correctness to also establish the latency bounds for entering various views stated by Properties A–C in Fig. 2. Our proofs are structured as follows. Given a view v whose entry time we seek to bound, we first derive a bound on the time by which all correct processes must send a $\mathtt{WISH}$ for the view v or higher. We then apply the following lemma, which bounds the latency of entering v as a function of the time by which all correct processes have sent such $\mathtt{WISH}$es.

Lemma 11

For all views $v>0$ and times s, if all correct processes $p_i$ send $\mathtt{WISH}(v_i)$ with $v_i \ge v$ no later than at s, and some correct process enters v, then $E_{\mathrm{last}}(v) \le \max (s, \overline{\mathsf{GST}}) + \delta$.

Proof

Fix an arbitrary correct process $p_i$ that sends $\mathtt{WISH}(v_i)$ with $v_i \ge v$ to all processes at time $t_i \le s \le \max (s, \overline{\mathsf{GST}})$. Since $\max (s, \overline{\mathsf{GST}}) \ge \overline{\mathsf{GST}}$, by Lemma 6 there exists a time $t_i'$ such that $\mathsf{GST}\le t_i' \le \max (s, \overline{\mathsf{GST}})$ and at $t_i'$, $p_i$ sends $\mathtt{WISH}(v_i')$ with $v_i' \ge v_i \ge v$ to all processes. Since $t_i' \ge \mathsf{GST}$, all correct processes receive $\mathtt{WISH}(v_i')$ from $p_i$ no later than at $t_i' + \delta \le \max (s, \overline{\mathsf{GST}}) + \delta$.

Consider an arbitrary correct process $p_j$ and let $t_j \le \max (s, \overline{\mathsf{GST}}) + \delta$ be the earliest time by which $p_j$ receives receives $\mathtt{WISH}(v_i')$ with with $v_i' \ge v$ from each correct processes $p_i$. Thus, at $t_j$, the entries of all correct processes in $p_j.\mathsf{max\_views}$ are occupied by views $\ge v$. Since at least $2f+1$ entries in $p_j.\mathsf{max\_views}$ belong to correct processes, the $(2f+1)$th highest entry is $\ge v$. Thus, $p_j.\mathsf{view}(t_j) \ge v$. Since $p_j.\mathsf{view}$ is non-decreasing, there exists a time $t_j' \le t_j$ at which $p_j.\mathsf{view}$ first became $\ge v$. If $p_j.\mathsf{view}(t_j') = p_j.\mathsf{view}^+(t_j') = v$, then $p_j$ enters v at $t_j'$. Otherwise, either $p_j.\mathsf{view}(t_j') > v$ or $p_j.\mathsf{view}^+(t_j') > v$. Since both $p_j.\mathsf{view}$ and $p_j.\mathsf{view}^+$ are non-decreasing, $p_j$ will never enter v after $t_j'$. Thus, a correct process cannot enter v after $\max (s, \overline{\mathsf{GST}}) + \delta$. Since by the lemma’s premise, some correct process does enter v, $E_{\mathrm{last}}(v) \le \max (s, \overline{\mathsf{GST}}) + \delta$, as needed. $\square$

The next lemma gives an upper bound on the duration of time a correct process may spend in a view before sending a $\mathtt{WISH}$ for a higher view.

Lemma 12

If a correct process $p_k$ enters a view $v > 0$, then $p_k$ sends $\mathtt{WISH}(v_k)$ with $v_k \ge v+1$ no later than at $\max (E_{\mathrm{last}}(v), \mathsf{GST}) + F(v)$.

Proof

Suppose that $p_k$ enters $v>0$ at time $s_k \le E_{\mathrm{last}}(v)$, and starts $p_k.\mathsf{timer\_view}$ for the duration of $F(v)$ at $s_k$. Then

$$\begin{aligned} p_k.\mathsf{view}(s_k) = p_k.\mathsf{view}^+(s_k) = v. \end{aligned}$$

Since the clocks of the correct processes advance at the same rate as real time after $\mathsf{GST}$, $p_k.\mathsf{timer\_view}$ cannot last past $\max (E_{\mathrm{last}}(v), \mathsf{GST})+F(v)$. Let $s_k'$ such that

$$\begin{aligned} s_k \le s_k' \le \max (E_{\mathrm{last}}(v), \mathsf{GST})+F(v) \end{aligned}$$

be the time at which $p_k.\mathsf{timer\_view}$ either expires or is stopped prematurely by executing the code in line 17. If $p_k.\mathsf{timer\_view}$ expires at $s_k'$, then $p_k$ sends $\mathtt{WISH}(v_k)$ with $v_k = \max (p_k.\mathsf{view}(s_k')+1, p_k.\mathsf{view}^+(s_k'))$. Since both $p_k.\mathsf{view}$ and $p_k.\mathsf{view}^+$ are non-decreasing, we have $p_k.\mathsf{view}(s_k') \ge v$ and $p_k.\mathsf{view}^+(s_k') \ge v$. Thus, $v_k \ge v + 1$, as required. On the other hand, if $p_k.\mathsf{timer\_view}$ is stopped prematurely at $s_k'$, then $p_k.\mathsf{view}(s_k') > p_k.\mathsf{view}(s_k) = v$ and therefore, $p_k.\mathsf{view}^+(s_k') \ge p_k.\mathsf{view}(s_k') \ge v+1$. Since $p_k.\mathsf{view}^+$ is non-decreasing and $p_k.\mathsf{view}^+(s_k)=v$, $p_k.\mathsf{view}^+$ must have changed its value from v to $v_k'' \ge v+1$ at some time $s_k''$ such that $s_k < s_k'' \le s_k'$. Thus, the condition in line 20 holds at $s_k''$, which means that $p_k$ sends $\mathtt{WISH}(v_k)$ with $v_k \ge v+1$ at $s_k''$. Thus, in all cases, $p_k$ sends $\mathtt{WISH}(v_k)$ with $v_k \ge v+1$ no later than at $\max (E_{\mathrm{last}}(v), \mathsf{GST}) + F(v)$, as required. $\square$

We now use the above two lemmas to bound the time it takes for a correct process that has entered a view v to enter the view $v+1$, as required by Property A.

Corollary 4

For all times t, if all correct processes enter $v > 0$, $E_{\mathrm{last}}(v) \ge \overline{\mathsf{GST}}$, and some correct process enters $v+1$, then $E_{\mathrm{last}}(v+1) \le E_{\mathrm{last}}(v) + F(v) + \delta$.

Proof

Instantiating Lemma 12 for the special case when all correct processes enter v at $\overline{\mathsf{GST}}$ or later, and given that by (6), $\overline{\mathsf{GST}}\ge \mathsf{GST}$, we get that every correct $p_k$ sends $\mathtt{WISH}(v_k)$ with $v_k\ge v+1$ no later than at $E_{\mathrm{last}}(v) + F(v) \ge \overline{\mathsf{GST}}$. Then the required follows from Lemma 11. $\square$

We now prove several lemmas needed for Properties B and C. First, given an arbitrary time t such that $t \ge \overline{\mathsf{GST}}$ and $\mathsf{GV}(t) > 0$, we derive an upper bound on the latency of reaching the next view $\mathsf{GV}(t)+1$ starting from t. To this end, we first bound the time by which all correct processes must send a $\mathtt{WISH}$ for a view $\ge \mathsf{GV}(t) + 1$ (Lemma 13), and then apply Lemma 11 to bound the latency of entering $\mathsf{GV}(t) + 1$ (Corollary 5). In the following, we instantiate this result for $t=\mathsf{GST}+\rho$ to establish Property C for the case of $\mathsf{GV}(\mathsf{GST}+\rho ) > 0$ (Corollary 7).

Lemma 13

Consider a time $t\ge \overline{\mathsf{GST}}$ and suppose that $\mathsf{GV}(t) > 0$. Let $T=t + F(\mathsf{GV}(t))+\delta$. If some correct process enters $\mathsf{GV}(t)+1$, then all correct processes $p_k$ send $\mathtt{WISH}(v_k)$ with $v_k \ge \mathsf{GV}(t)+1$ to all processes no later than at $T + \delta$.

Proof

Since $\mathsf{GV}(t) > 0$, the definition of $\mathsf{GV}$ implies that there exists a correct process $p_l$ such that $p_l$ entered $\mathsf{GV}(t)$ and $E_{l}(\mathsf{GV}(t)) \le t$. By the view entry condition, $p_l.\mathsf{view}(E_{l}(\mathsf{GV}(t))) = \mathsf{GV}(t)$, and therefore $p_l.\mathsf{max\_views}(E_{l}(\mathsf{GV}(t)))$ includes $2f+1$ entries $\ge \mathsf{GV}(t)$. Since $f+1$ of these entries belong to correct processes, there exists a set C of $f+1$ correct processes $p_i$, each of which sent $\mathtt{WISH}(v_i)$ with $v_i\ge \mathsf{GV}(t)$ to all processes before $E_{l}(\mathsf{GV}(t)) \le t$. Since $t \ge \overline{\mathsf{GST}}$, by Lemma 6, $p_i$ sends $\mathtt{WISH}(v_i')$ with $v_i' \ge v_i \ge \mathsf{GV}(t)$ sometime between $\mathsf{GST}$ and t. Since after $\mathsf{GST}$ every message sent by a correct process is received by all correct processes within $\delta$ of its transmission, the above implies that by $t + \delta$ every correct process receives a $\mathtt{WISH}(v_i')$ with $v_i' \ge \mathsf{GV}(t)$ from each process $p_i \in C$.

Consider an arbitrary correct process $p_j$ and let $t_j \le t + \delta$ be the earliest time by which $p_j$ receives $\mathtt{WISH}(v_i)$ with $v_i \ge \mathsf{GV}(t)$ from each process $p_i \in C$. Thus, for all processes $p_i\in C$, $p_j.\mathsf{max\_views}[i](t_j) \ge \mathsf{GV}(t)$. Since $|C|=f+1$, the $(f+1)$th highest entry in $p_j.\mathsf{max\_views}[i](t_j)$ is $\ge \mathsf{GV}(t)$, and therefore, $p_j.\mathsf{view}^+(t_j) \ge \mathsf{GV}(t)$. Then each correct process $p_j$ sends $\mathtt{WISH}(v_j)$ with $v_j \ge \mathsf{GV}(t)$ to all correct processes no later than $t_j \le t + \delta$. Since $t+\delta > t \ge \overline{\mathsf{GST}}$ and, by the definition of $\mathsf{GV}$, some correct process entered $\mathsf{GV}(t)$, by Lemma 11,

$$\begin{aligned} E_{\mathrm{last}}(\mathsf{GV}(t)) \le t + 2\delta . \end{aligned}$$

(11)

In addition, by Lemma 6, there exists a time $t_j'$ such that $\mathsf{GST}\le t_j' \le t+\delta$ and $p_j$ sends $\mathtt{WISH}(v_j')$ with $v_j' \ge v_j \ge \mathsf{GV}(t)$ at $t_j'$. Since a message sent by a correct process after $\mathsf{GST}$ is received by all correct processes within $\delta$ of its transmission, all correct processes must have received $\mathtt{WISH}(v_j')$ with $v_j' \ge \mathsf{GV}(t)$ from each correct process $p_j$ in-between $\mathsf{GST}$ and $t + 2\delta$.

Consider an arbitrary correct process $p_k$. If $p_k$ enters $\mathsf{GV}(t)$, then by Lemma 12, $p_k$ sends $\mathtt{WISH}(v_k)$ with $v_k \ge \mathsf{GV}(t)+1$ at some time $t_k \le \max (E_{\mathrm{last}}(\mathsf{GV}(t)), \mathsf{GST}) + F(\mathsf{GV}(t))$. If $E_{\mathrm{last}}(\mathsf{GV}(t)) \ge \mathsf{GST}$, then by (11),

$$\begin{aligned} t_k \!\le \!E_{\mathrm{last}}(\mathsf{GV}(t)) \!+\! F(\mathsf{GV}(t)) \le \! t + 2\delta + F(\mathsf{GV}(t)) \!=\! T+\delta . \end{aligned}$$

On the other hand, if $\mathsf{GST}> E_{\mathrm{last}}(\mathsf{GV}(t))$, then since $t \ge \overline{\mathsf{GST}}$, and by (6), $\overline{\mathsf{GST}}\ge \mathsf{GST}$, we have

$$\begin{aligned} t_k \le \mathsf{GST}+ F(\mathsf{GV}(t)) \le t + F(\mathsf{GV}(t)) < T + \delta . \end{aligned}$$

Thus, we conclude that if $p_k$ enters $\mathsf{GV}(t)$, then the required holds.

Suppose now that $p_k$ never enters $\mathsf{GV}(t)$, and let $t_k$ be the earliest time $\ge \mathsf{GST}$ by which $p_k$ receives $\mathtt{WISH}(v_j')$ from each correct process $p_j$; we have $t_k \le t+2\delta$. Since $v_j' \ge \mathsf{GV}(t)$, and there are $2f+1$ correct processes, $p_k.\mathsf{max\_views}(t_k)$ includes at least $2f+1$ entries $\ge \mathsf{GV}(t)$. Thus, $p_k.\mathsf{view}(t_k) \ge \mathsf{GV}(t)$. Since $p_k$ never enters $\mathsf{GV}(t)$, we have either $p_k.\mathsf{view}^+(t_k) \ge p_k.\mathsf{view}(t_k) \ge \mathsf{GV}(t)+1$ or $p_k.\mathsf{view}(t_k) = \mathsf{GV}(t) \wedge p_k.\mathsf{view}^+(t_k) \ge \mathsf{GV}(t)+1$. Thus, $p_k.\mathsf{view}^+(t_k) \ge \mathsf{GV}(t) + 1$ and therefore, $p_k$ sends $\mathtt{WISH}(v_k)$ with $v_k\ge \mathsf{GV}(t)+1$ by $t_k \le t+2\delta \le T+\delta$. Hence, we get that all correct processes send $\mathtt{WISH}(v_k)$ with $v_k \ge \mathsf{GV}(t)+1$ to all correct processes no later than $T+\delta$, validating the lemma. $\square$

Lemmas 11 and 13 imply an upper bound on the latency of reaching the view $\mathsf{GV}(t)+1$ from an arbitrary time t such that $t\ge \overline{\mathsf{GST}}$ and $\mathsf{GV}(t)>0$.

Corollary 5

Consider a time $t\ge \overline{\mathsf{GST}}$ and suppose that $\mathsf{GV}(t) > 0$. If some correct process enters the view $\mathsf{GV}(t)+1$, then $E_{\mathrm{last}}(\mathsf{GV}(t)+1) \le t + F(\mathsf{GV}(t)) + 3\delta$.

We next derive a bound on the latency of entering view 1. This is used to prove Property B as well as Property  C for the case of $\mathsf{GV}(\mathsf{GST}+\rho ) = 0$.

Lemma 14

If some correct process enters view 1, then $E_{\mathrm{last}}(1) \le \min (t_1+2\delta , t_2+\delta )$, where $t_1 = \max (S_{f+1}, \overline{\mathsf{GST}})$ and $t_2 = \max (S_{\mathrm{last}}, \overline{\mathsf{GST}})$. Equivalently:

$$\begin{aligned} E_{\mathrm{last}}(1) \le {}&t_2+\delta ; \end{aligned}$$

(12)

$$\begin{aligned} E_{\mathrm{last}}(1) \le {}&t_1+2\delta . \end{aligned}$$

(13)

Proof

We consider three cases:

• $\overline{\mathsf{GST}}\le S_{f+1} \le S_{\mathrm{last}}$, so that $t_1 = S_{f+1}$ and $t_2 = S_{\mathrm{last}}$. We consider two cases:

  • $S_{f+1} + \delta < S_{\mathrm{last}}$. Let C be the set of the $f+1$ correct processes $p_i$ calling $\mathtt{start}()$ at $t_i \le S_{f+1}$. If $p_i.\mathsf{view}^+(t_i) = 0$, then at $t_i$, $p_i$ sends $\mathtt{WISH}(1)$ to all processes by executing the code in line 3. Otherwise, $p_i.\mathsf{view}^+(t_i) \ge 1$, and $p_i$ sent $\mathtt{WISH}(v_i)$ with $v_i\ge 1$ when $p_i.\mathsf{view}^+$ first became equal to $v_i$ at some time $s_i < t_i \le S_{f+1}$. Since $t_i \le S_{f+1}$ and $S_{f+1} \ge \overline{\mathsf{GST}}$, in both cases, by Lemma 6, $p_i$ sends $\mathtt{WISH}(v_i')$ with $v_i' \ge v_i \ge 1$ sometime between $\mathsf{GST}$ and $S_{f+1}$. Thus, we get that all processes $p_i \in C$ send $\mathtt{WISH}(v_i')$ with $v_i'\ge 1$ to all processes in-between $\mathsf{GST}$ and $S_{f+1}$. It follows that all correct processes receive all these $\mathtt{WISH}(v_i')$ messages no later than $S_{f+1}+\delta$. Consider a correct process $p_j$, and let $t_j$ be the earliest time by which $p_j$ receives the $\mathtt{WISH}(v_i')$ messages sent by the processes $p_i\in C$ in-between $\mathsf{GST}$ and $S_{f+1}$; then $\mathsf{GST}\le t_j \le S_{f+1}+\delta$. Thus, $p_j.\mathsf{max\_views}[k](t_j) \ge 1$ for all $p_k \in C$. Since $|C|\ge f+1$, the $(f+1)$th highest entry in $p_j.\mathsf{max\_views}[k](t_j)$ is $\ge 1$, and therefore, $p_j.\mathsf{view}^+(t_j) \ge 1$. Thus, $p_j$ sends $\mathtt{WISH}(v_j)$ with $v_j \ge 1$ to all processes no later than $t_j \le S_{f+1} + \delta$, and we also have $S_{f+1} + \delta > \overline{\mathsf{GST}}$. Since some correct process enters view 1, by Lemma 11, $E_{\mathrm{last}}(1) \le S_{f+1} + 2\delta = t_1 + 2\delta$. Since $t_1 + \delta < t_2$, we also have $E_{\mathrm{last}}(1) \le \min (t_1 + 2\delta , t_2 + \delta )$, as needed.

  • $S_{f+1} + \delta \ge S_{\mathrm{last}}$. Let $p_i$ be a correct process calling $\mathtt{start}()$ at $t_i \le S_{\mathrm{last}}$. If $p_i.\mathsf{view}^+(t_i) = 0$, then at $t_i$, $p_i$ sends $\mathtt{WISH}(1)$ to all processes by executing the code in line 3. Otherwise, $p_i.\mathsf{view}^+(t_i) \ge 1$, and $p_i$ sent $\mathtt{WISH}(v_i)$ with $v_i \ge 1$ when $p_i.\mathsf{view}^+$ first became equal to $v_i$ at some time $s_i < t_i \le S_{\mathrm{last}}$. Thus, all correct processes send $\mathtt{WISH}(v_i)$ with $v_i \ge 1$ to all processes no later than $S_{\mathrm{last}}\ge \overline{\mathsf{GST}}$. Since some correct process enters view 1, by Lemma 11, $E_{\mathrm{last}}(1) \le S_{\mathrm{last}}+ \delta = t_2 + \delta$. Since $t_1 + \delta \ge t_2$, we also have $E_{\mathrm{last}}(1) \le \min (t_1 + 2\delta , t_2 + \delta )$, as needed.

• $S_{f+1} < \overline{\mathsf{GST}}\le S_{\mathrm{last}}$, so that $t_1 = \overline{\mathsf{GST}}$ and $t_2 = S_{\mathrm{last}}$. We consider two cases:

  • $\overline{\mathsf{GST}}+ \delta < S_{\mathrm{last}}$. Let C be the set of the $f+1$ correct processes $p_i$ calling $\mathtt{start}()$ at $t_i < \overline{\mathsf{GST}}$. If $p_i.\mathsf{view}^+(t_i) = 0$, then at $t_i$, $p_i$ sends $\mathtt{WISH}(1)$ to all processes by executing the code in line 3. Otherwise, $p_i.\mathsf{view}^+(t_i) \ge 1$, and $p_i$ sent $\mathtt{WISH}(v_i)$ with $v_i \ge 1$ when $p_i.\mathsf{view}^+$ first became equal to $v_i$ at sometime before $t_i$. Since $t_i < \overline{\mathsf{GST}}$, by Lemma 6, there exists a time $s_i$ such that $\mathsf{GST}\le s_i < \overline{\mathsf{GST}}$ and at $s_i$, $p_i$ sends $\mathtt{WISH}(v_i')$ with $v_i' \ge v_i \ge 1$ to all processes. Thus, we get that all processes in C send $\mathtt{WISH}(v_i')$ with $v_i \ge 1$ to all processes in-between $\mathsf{GST}$ and $\overline{\mathsf{GST}}$. It follows that all correct processes receive all these $\mathtt{WISH}(v_i')$ messages no later than $\overline{\mathsf{GST}}+\delta$. Consider a correct process $p_j$, and let $t_j$ be the earliest time by which $p_j$ receives the $\mathtt{WISH}(v_i')$ messages sent by the processes in C in-between $\mathsf{GST}$ and $\overline{\mathsf{GST}}$; then $\mathsf{GST}\le t_j \le \overline{\mathsf{GST}}+\delta$. Thus, $p_j.\mathsf{max\_views}[k](t_j) \ge 1$ for all $p_k \in C$. Since $|C|\ge f+1$, the $(f+1)$th highest entry in $p_j.\mathsf{max\_views}[k](t_j)$ is $\ge 1$. Thus, $p_j.\mathsf{view}^+(t_j) \ge 1$, so that $p_j$ sends $\mathtt{WISH}(v_j)$ with $v_j \ge 1$ to all processes no later than $t_j \le \overline{\mathsf{GST}}+ \delta$. Since some correct process enters view 1, by Lemma 11, $E_{\mathrm{last}}(1) \le \overline{\mathsf{GST}}+ 2\delta = t_1 + 2\delta$. Since $t_1 + \delta < t_2$, we also have $E_{\mathrm{last}}(1) \le \min (t_1 + 2\delta , t_2+\delta )$, as needed.

  • $\overline{\mathsf{GST}}+ \delta \ge S_{\mathrm{last}}$. Let $p_i$ be a correct process calling $\mathtt{start}()$ at $t_i \le S_{\mathrm{last}}$. If $p_i.\mathsf{view}^+(t_i) = 0$, then at $t_i$, $p_i$ sends $\mathtt{WISH}(1)$ to all processes by executing the code in line 3. Otherwise, $p_i.\mathsf{view}^+(t_i) \ge 1$, and $p_i$ sent $\mathtt{WISH}(v_i)$ with $v_i \ge 1$ when $p_i.\mathsf{view}^+$ first became equal to $v_i$ at some time $s_i < t_i \le S_{\mathrm{last}}$. Thus, we get that all correct processes $p_i$ send $\mathtt{WISH}(v_i)$ with $v_i \ge 1$ to all processes no later than $S_{\mathrm{last}}\ge \overline{\mathsf{GST}}$. Since some correct process enters view 1, by Lemma 11, $E_{\mathrm{last}}(1) \le S_{\mathrm{last}}+ \delta = t_2 + \delta$. Since $t_2 \le t_1 + \delta$, we also have $E_{\mathrm{last}}(1) \le \min (t_1 + 2\delta , t_2 + \delta )$, as needed.

• $S_{f+1} \le S_{\mathrm{last}}< \overline{\mathsf{GST}}$, so that $t_1 = t_2 = \overline{\mathsf{GST}}$. Let $p_i$ be a correct process calling $\mathtt{start}()$ at $t_i \le S_{\mathrm{last}}< \overline{\mathsf{GST}}$. If $p_i.\mathsf{view}^+(t_i) = 0$, then at $t_i$, $p_i$ sends $\mathtt{WISH}(1)$ to all processes by executing the code in line 3. Otherwise, $p_i.\mathsf{view}^+(t_i) \ge 1$, and $p_i$ sent $\mathtt{WISH}(v_i)$ with $v_i \ge 1$ when $p_i.\mathsf{view}^+$ first became equal to $v_i$ at some time $s_i< t_i \le S_{\mathrm{last}}< \overline{\mathsf{GST}}$. By Lemma 6, in both cases $p_i$ sends $\mathtt{WISH}(v_i')$ with $v_i' \ge v_i \ge 1$ sometime between $\mathsf{GST}$ and $\overline{\mathsf{GST}}$. Since some correct process enters view 1, by Lemma 11, we get that $E_{\mathrm{last}}(1) \le \overline{\mathsf{GST}}+ \delta = t_2 + \delta$. Since $t_1 = t_2$, we also have $E_{\mathrm{last}}(1) \le \min (t_1 + 2\delta , t_2 + \delta )$, as needed.

Thus, we get that in all three cases above, $E_{\mathrm{last}}(1) \le \min (t_1 + 2\delta , t_2 + \delta )$, as needed. $\square$

We now instantiate the bound (12) of Lemma 14 for the special case of all correct processes starting the protocol after $\mathsf{GST}$ to obtain the latency bound stipulated by Property B.

Corollary 6

If $S_{\mathrm{first}}\ge \mathsf{GST}$ and a correct process enters view 1, then $E_{\mathrm{last}}(1) \le S_{\mathrm{last}}+ \delta$.

Proof

Let $S_{\mathrm{first}}\ge \mathsf{GST}$. Then $\overline{\mathsf{GST}}=S_{\mathrm{first}}$ by the definition of $\overline{\mathsf{GST}}$. We now use the bound (12) of Lemma 14 with $t_1 = \max (S_{f+1}, S_{\mathrm{first}}) = S_{f+1}$ and $t_2 = \max (S_{\mathrm{last}}, S_{\mathrm{first}}) = S_{\mathrm{last}}$. We get $E_{\mathrm{last}}(1) \le t_2+\delta = S_{\mathrm{last}}+ \delta$, as required. $\square$

Finally, by combining Corollary 5 and the bound (13) of Lemma 14, we obtain the following bound, used to prove Property  C.

Corollary 7

Assume that $S_{\mathrm{first}}< \mathsf{GST}$ and $S_{f+1} \le \mathsf{GST}+\rho$. Then if a correct process enters $\mathsf{GV}(\mathsf{GST}+\rho )+1$, then

$$\begin{aligned} E_{\mathrm{last}}(\mathsf{GV}(\mathsf{GST}+\rho )+1) \le \mathsf{GST}+\rho + F(\mathsf{GV}(\mathsf{GST}+\rho )) + 3\delta . \end{aligned}$$

Proof

Since $S_{\mathrm{first}}< \mathsf{GST}$, by the definition of $\overline{\mathsf{GST}}$, we have $\overline{\mathsf{GST}}= \mathsf{GST}+ \rho$. If $\mathsf{GV}(\mathsf{GST}+ \rho )=0$, then choosing $t_1=\max (S_{f+1}, \mathsf{GST}+ \rho )$, and $t_2 = \max (S_{\mathrm{last}}, \mathsf{GST}+ \rho )$, by the bound (13) of Lemma 14 we get $E_{\mathrm{last}}(\mathsf{GV}(\mathsf{GST}+ \rho )+1) \le t_1+2\delta$. Since $S_{f+1} \le \mathsf{GST}+ \rho$, we have $t_1=\mathsf{GST}+ \rho$, and therefore,

$$\begin{aligned}&E_{\mathrm{last}}(\mathsf{GV}(\mathsf{GST}+ \rho )+1) \le \mathsf{GST}+ \rho +2\delta < {}\\&\mathsf{GST}+ \rho + F(\mathsf{GV}(t)) + 3\delta , \end{aligned}$$

as required. On the other hand, if $\mathsf{GV}(\mathsf{GST}+ \rho )>0$, then by Corollary 5,

$$\begin{aligned} E_{\mathrm{last}}(\mathsf{GV}(\mathsf{GST}+ \rho )+1) \le \mathsf{GST}+ \rho + F(\mathsf{GV}(\mathsf{GST}+ \rho )) + 3\delta , \end{aligned}$$

as required. $\square$

Proof of Theorem 1

Consider an execution of FastSync and let $\delta$ be the eventual message delay bound in this execution. We first show how to select a view ${\mathcal {V}}$ such that (9) holds. We consider the following cases. First, if

$$\begin{aligned} S_{\mathrm{first}}\ge \mathsf{GST}\wedge F(1) \ge 2\delta , \end{aligned}$$

(14)

then we let ${\mathcal {V}}=1$. Since $S_{\mathrm{first}}\ge \mathsf{GST}$, the definition of $\overline{\mathsf{GST}}$ implies $\overline{\mathsf{GST}}=S_{\mathrm{first}}$, and therefore, (9) holds. Second, if

$$\begin{aligned}&S_{\mathrm{first}}< \mathsf{GST}\wedge S_{f+1} \le \mathsf{GST}+ \rho \wedge {} \nonumber \\&F(\mathsf{GV}(\mathsf{GST}+ \rho )+1) \ge 2\delta , \end{aligned}$$

(15)

then we let ${\mathcal {V}}=\mathsf{GV}(\mathsf{GST}+\rho ) + 1$. Since $S_{\mathrm{first}}< \mathsf{GST}$, the definition of $\overline{\mathsf{GST}}$ implies $\overline{\mathsf{GST}}=\mathsf{GST}+\rho$, and therefore, (9) holds. In all other cases, (1) for $u = 2\delta$ implies that $F(v') \ge 2\delta$ for some view $v'$, and therefore, by the monotonicity of $F$, ${\mathcal {V}}= \max \{v', \mathsf{GV}(\overline{\mathsf{GST}}) + 1\}$ satisfies (9).

Thus, by Lemma 10, Properties 1–5 in Fig. 2 hold for ${\mathcal {V}}$ chosen as above and $d=2\delta$.

To prove Property A, fix $v\ge {\mathcal {V}}$. By Property 3, all correct processes enter v. By (9), $v \ge {\mathcal {V}}\ge \mathsf{GV}(\overline{\mathsf{GST}})+1$. Given that $\mathsf{GV}$ is non-decreasing, this implies that no correct process can enter v until after $\overline{\mathsf{GST}}$. Thus, $E_{\mathrm{last}}(v) \ge E_{\mathrm{first}}(v) > \overline{\mathsf{GST}}$, and by Corollary 4 we get $E_{\mathrm{last}}(v+1) \le E_{\mathrm{last}}(v) + F(v) + \delta$, validating Property A. Finally, by our choice of ${\mathcal {V}}$, (14) implies ${\mathcal {V}}=1$, and (15) implies ${\mathcal {V}}=\mathsf{GV}(\mathsf{GST}+ \rho ) + 1$. Thus, Property B follows from Corollary 6, and Property  C from Corollary 7. We therefore, conclude that FastSync satisfies all properties in Fig. 2 for $d=2\delta$ and ${\mathcal {V}}$ chosen as above. $\square$

5 Liveness and latency of Byzantine consensus protocols

We show that our synchronizer abstraction allows ensuring liveness and establishing latency bounds for several consensus protocols. The protocols solve a variant of the Byzantine consensus problem that relies on an application-specific $\mathsf{valid}()$ predicate to indicate whether a value is valid [16, 23]. In the context of blockchain systems a value represents a block, which may be invalid if it does not include correct signatures authorizing its transactions. Assuming that each correct process proposes a valid value, each of them has to decide on a value so that:

• Agreement. No two correct processes decide on different values.

• Validity. A correct process decides on a valid value, i.e., satisfying $\mathsf{valid}()$.

• Termination. Every correct process eventually decides on a value.

5.1 Single-shot PBFT

We first consider the seminal Practical Byzantine Fault Tolerance (PBFT) protocol [19]. This protocol was originally presented as implementing state-machine replication, where the processes agree on a sequence of commands. In Algorithm 2 we present its specialization to consensus, in the style of DLS [27]. The protocol in Algorithm 2 works in a succession of views produced by the synchronizer. Each view v has a fixed leader $\mathsf{leader}(v) = p_{((v-1)\ \mathrm{mod}\ n) + 1}$ that is responsible for proposing a value to the other processes, which vote on the proposal. A correct leader needs to choose its proposal carefully so that, if some process decided a value in a previous view, the leader will propose the same value. To enable the leader to do this, when a process receives a notification from the synchronizer to move to a view v (line 1), it sends a $\mathtt{NEWLEADER}$ message to the leader of v with some information about the latest value it accepted in a previous view. The process also stores the view v in a variable $\mathsf{curr\_view}$, and sets a flag $\mathsf{voted}$ to $\textsc {false}$, to record that it has not yet received any proposal from the leader in the current view. Various messages sent in the protocol are tagged with the view of the sender; a receiver accepts a message only if it is in the same view according to the $\mathsf{curr\_view}$ variable.

The leader computes its proposal based on a quorum of $\mathtt{NEWLEADER}$ messages (line 5) and sends the proposal, along with some supporting information, in a $\mathtt{PROPOSE}$ message to all processes (for uniformity, including itself). We describe the proposal computation in detail after describing the rest of the protocol. The leader’s proposal is processed in two phases, each with an all-to-all message exchange among processes. A process receiving a proposal $x$ from the leader of its view v (line 11) first checks that $\mathsf{voted}$ is $\textsc {false}$, so that it has not yet accepted a proposal in v. It also checks that x satisfies a $\mathsf{SafeProposal}$ predicate (also explained later), which ensures that a faulty leader cannot reverse decisions reached in previous views. The process then sets $\mathsf{voted}$ to $\textsc {true}$ and stores $x$ in $\mathsf{curr\_val}$.

Since a faulty leader may send different proposals to different processes, the process next communicates with others to check that they received the same proposal. To this end, the process disseminates a $\mathtt{PREPARED}$ message with the hash of the proposal it received. The process then waits until it gathers a set C of $\mathtt{PREPARED}$ messages from a quorum with a hash matching the proposal (line 16). We call this set of messages a prepared certificate for the value and check it using the following predicate:

$$\begin{aligned}&\mathsf{prepared}(C, v, h) \iff \\&\quad \exists Q.\, \mathsf{quorum}(Q) \wedge C = \{\langle \mathtt{PREPARED}(v, h) \rangle _j \mid p_j \in Q\}. \end{aligned}$$

Once a process assembles a prepared certificate, the process stores it in $\mathsf{cert}$, the view in which it was formed in $\mathsf{prepared\_view}$, and the value it corresponds to in $\mathsf{prepared\_val}$. At this point we say that the process prepared the value. Since a prepared certificate consists of at least $2f+1$ $\mathtt{PREPARED}$ messages and there are $3f+1$ processes in total, it is impossible to prepare different values in the same view: this would require some correct process to send two $\mathtt{PREPARED}$ messages with different hashes in the same view, which cannot happen due to the check on the $\mathsf{voted}$ flag in line 12. Formally, let us write $\mathsf{wf}(C)$ (for well-formed) if the set of correctly signed messages C was generated in the execution of the protocol.

Proposition 4

$$\begin{aligned} \forall v, C, C', x, x'.\,&\mathsf{prepared}(C, v, \mathsf{hash}(x)) \wedge {} \\&\mathsf{prepared}(C', v, \mathsf{hash}(x')) \wedge {} \\&\mathsf{wf}(C) \wedge \mathsf{wf}(C') {\implies } x= x'. \end{aligned}$$

Since the synchronizer transitions processes through increasing views (Property 1 in Fig. 2), we also get

Proposition 5

The variables $\mathsf{curr\_view}$ and $\mathsf{prepared\_view}$ at a correct process never decrease and we always have $\mathsf{prepared\_view}\le \mathsf{curr\_view}$.

Having prepared a value, the process participates in another message exchange: it disseminates a $\mathtt{COMMITTED}$ message with the hash of the value and waits until it gathers a quorum of matching $\mathtt{COMMITTED}$ messages for this value (line 22). We call such a quorum a committed certificate and let

$$\begin{aligned}&\mathsf{committed}(C, v, h) \iff \\&\quad \exists Q.\, \mathsf{quorum}(Q) \wedge C = \{\langle \mathtt{COMMITTED}(v, h) \rangle _j \mid p_j \in Q\}. \end{aligned}$$

Once a process assembles a committed certificate for a value $x$, it decides on $x$.

When the synchronizer triggers a $\mathtt{new\_view}$ notification at a process (line 1), the process sends a $\mathtt{NEWLEADER}$ message to the new leader. Since preparing a value is a prerequisite for deciding on it, by Proposition 4 forming a prepared certificate for a value $x$ in a view v guarantees that $x$ is the only value that can possibly be decided in v. For this reason, it is this certificate, together with the corresponding value and view, that the process sends upon a view change to the new leader in a $\mathtt{NEWLEADER}$ message (line 4). The leader makes its proposal based on a quorum of well-formed $\mathtt{NEWLEADER}$ messages (line 5), as checked by a $\mathsf{ValidNewLeader}$ predicate:

$$\begin{aligned}&\mathsf{ValidNewLeader}(\langle \mathtt{NEWLEADER}(v', v, x, C) \rangle _{\_}) \iff \nonumber \\&\quad v < v' \wedge ({v \not = 0} {\implies } \mathsf{prepared}(C, v, \mathsf{hash}(x))). \end{aligned}$$

(16)

Similarly to Paxos [37], the leader selects as its proposal the value prepared in the highest view, or, if there are no such values, its own proposal given by $\mathtt{myval}()$. Since a faulty leader may not follow this rule, the processes need to check that the leader has selected the proposal correctly. To this end, the leader’s $\mathtt{PROPOSE}$ message carries, in addition to the proposal, the $\mathtt{NEWLEADER}$ messages on the basis of which it was computed (line 4). Processes check its correctness by redoing the leader’s computation, as specified by the $\mathsf{SafeProposal}$ predicate (line 12):

$$\begin{aligned}&\mathsf{SafeProposal}(\langle \mathtt{PROPOSE}(v, x, M) \rangle _j) \iff {} \nonumber \\&\quad p_j = \mathsf{leader}(v) \wedge \mathsf{valid}(x) \wedge {} \nonumber \\&\quad \exists Q, view , val , cert .\, \mathsf{quorum}(Q) \wedge {} \nonumber \\&\quad M = \{\langle \mathtt{NEWLEADER}(v, view _k, val _k, cert _k) \rangle _k \mid p_k \in Q\} {\wedge } {} \nonumber \\&\quad (\forall m \in M.\, \mathsf{ValidNewLeader}(m)) \wedge {} \nonumber \\&\quad ((\exists k.\, view _k \not = 0) {\implies } \nonumber \\&\qquad (\exists k.\, view _k = \max \{ view _{l} \mid p_l \in Q\} \wedge x= val _k)). \end{aligned}$$

(17)

Note that the $\mathsf{SafeProposal}$ check still allows a faulty leader to send different proposals to different processes, e.g., by selecting different quorums of $\mathtt{NEWLEADER}$ messages, or by selecting different values in case when none of the $\mathtt{NEWLEADER}$ messages carries a prepared certificate. Hence, the $\mathsf{SafeProposal}$ check does not make the exchange of $\mathtt{PREPARED}$ messages unnecessary, as it protects against such behavior. On the other hand, exchanging $\mathtt{COMMITTED}$ messages before deciding is needed to preserve decisions across views and thereby validate the Agreement property of consensus. It guarantees that, if a process decides on a value $x$, then at least $f+1$ correct processes have prepared $x$. Regardless of whether the leader of the next view is correct or faulty, due to the $\mathsf{SafeProposal}$ check it will make a proposal based on prepared values from at least $2f+1$ processes. Then at least one correct process out of these will report the value $x$, which the leader will have to take into account. This is the core argument in the proof of Agreement we give below (Theorem 9).

Note that, when a process enters view 1, it trivially knows that no decision could have been reached in prior views. Hence, the leader of view 1 can send its proposal immediately, without waiting to receive a quorum of $\mathtt{NEWLEADER}$ messages. Processes can avoid sending $\mathtt{NEWLEADER}$ messages to this leader, and can accept its proposal after checking that it satisfies $\mathsf{valid}$ rather than $\mathsf{ValidNewLeader}$. For brevity, we omit this optimization from the pseudocode, even though we take it into account in our latency analysis.

Since the synchronizer is not guaranteed to switch processes between views all at the same time, a process in a view v may receive a message from a higher view $v' > v$, which needs to be stored in case the process finally switches to $v'$. If implemented naively, this would require a process to store unboundedly many messages. Instead, we allow a process to store, for each message type and sender, only the message of this type received from this sender that has the highest view. As we show below (Theorem 15), this does not violate liveness. Thus, assuming consensus proposals of bounded size, the protocol Algorithm 2 runs in bounded space, and so does the overall consensus protocol with the FastSync synchronizer.

Safety In PBFT, deciding on a value requires preparing it, which implies

Proposition 6

$$\begin{aligned}&\forall v, C, h.\, \mathsf{committed}(C, v, h) \wedge \mathsf{wf}(C) {\implies } \\&\exists C'.\, \mathsf{prepared}(C', v, h) \wedge \mathsf{wf}(C'). \end{aligned}$$

Furthermore, the validity check in $\mathsf{SafeProposal}$ ensures that any prepared value is valid:

Proposition 7

$$\begin{aligned} \forall v, C, x.\, \mathsf{prepared}(C, v, \mathsf{hash}(x)) \wedge \mathsf{wf}(C) {\implies } \mathsf{valid}(x). \end{aligned}$$

The above two propositions imply

Corollary 8

Single-shot PBFT satisfies Validity.

The Agreement property of consensus follows from the next lemma, ensuring that if a committed certificate was assembled for a value in a given view, then only this value can be prepared in any higher view.

Lemma 15

$$\begin{aligned} \forall v, v', C, C', x, x'.\,&\mathsf{committed}(C, v, \mathsf{hash}(x)) \wedge {} \\&\mathsf{prepared}(C', v', \mathsf{hash}(x')) \wedge {} \\&\mathsf{wf}(C) \wedge \mathsf{wf}(C') \wedge v < v' {\implies } x= x'. \end{aligned}$$

Proof

Fix v, C and $x$, and assume $\mathsf{committed}(C, v, \mathsf{hash}(x))$ and $\mathsf{wf}(C)$; then $v > 0$. We prove by induction on $v'$ that

$$\begin{aligned}&\forall v', C', x'.\, v < v' \wedge \mathsf{prepared}(C', v', \mathsf{hash}(x')) \wedge \mathsf{wf}(C') \\&{\implies } x' = x. \end{aligned}$$

Assume this holds for all $v' < v^*$; we now prove it for $v' = v^*$. To this end, assume $v < v'$, $\mathsf{prepared}(C', v', \mathsf{hash}(x'))$ and $\mathsf{wf}(C')$.

From the induction hypothesis it follows that

$$\begin{aligned}&\forall C'', v'', x''.\, v< v'' < v' \wedge \mathsf{prepared}(C'', v'', \mathsf{hash}(x'')) \\&\wedge \mathsf{wf}(C'') {\implies } x= x''. \end{aligned}$$

Furthermore, by Propositions 4 and 6 we have

$$\begin{aligned} \forall C'', x''.\, \mathsf{prepared}(C'', v, \mathsf{hash}(x'')) \!\wedge \!\mathsf{wf}(C'') {\implies } x\!=\! x'', \end{aligned}$$

so that overall we get

$$\begin{aligned}&\forall C'', v'', x''.\, v \le v'' < v' \wedge \mathsf{prepared}(C'', v'', \mathsf{hash}(x'')) \nonumber \\&\wedge \mathsf{wf}(C'') \implies x= x''. \end{aligned}$$

(18)

Since $\mathsf{prepared}(C', v', \mathsf{hash}(x'))$ and $\mathsf{wf}(C')$, some correct process has received a message $m = \langle \mathtt{PROPOSE}(v',x', M)\rangle _{\_}$ from the leader of $v'$ such that $\mathsf{SafeProposal}(m)$ (line 12). Let

$$\begin{aligned} M = \{\langle \mathtt{NEWLEADER}(v', view _j, val _j, cert _j) \rangle _j \mid p_j \in Q'\} \end{aligned}$$

for some quorum $Q'$. Since $\mathsf{SafeProposal}(m)$, we have $\forall m' \in M.\, \mathsf{ValidNewLeader}(m')$, so that

$$\begin{aligned}&\forall p_j \in Q'.\, view _j < v' \wedge ({ view _j \not = 0} {\implies } \\&\mathsf{prepared}( cert _j, view _j, \mathsf{hash}( val _j)) \wedge \mathsf{wf}( cert _j)). \end{aligned}$$

From this and (18) we get that

$$\begin{aligned} \forall p_j \in Q'.\, { view _j \ge v} {\implies } val _j = x. \end{aligned}$$

(19)

Since $\mathsf{committed}(C, v, \mathsf{hash}(x))$ and $\mathsf{wf}(C)$, a quorum Q of processes sent $\mathtt{COMMITTED}(v, \mathsf{hash}(x))$. The quorums Q and $Q'$ have to intersect in some correct process $p_k$, which has thus sent both $\mathtt{COMMITTED}(v, \mathsf{hash}(x))$ and $\mathtt{NEWLEADER}(v', view _k, val _k, cert _k)$. Since $v< v'$, this process $p_k$ must have sent the $\mathtt{COMMITTED}$ message before the $\mathtt{NEWLEADER}$ message. Before sending $\mathtt{COMMITTED}(v, \mathsf{hash}(x))$ the process set $\mathsf{prepared\_view}$ to v (line 19). Then by Proposition 5 process $p_k$ must have had $\mathsf{prepared\_view}\ge v$ when it sent the $\mathtt{NEWLEADER}$ message. Hence, $view _k \ge v \not = 0$ and $\max \{ view _l \mid p_l \in Q'\} \ge v$. Then from (19) for any j such that $view _j = \max \{ view _{l} \mid p_l \in Q'\}$ we must have $val _j = x$. Since $\mathsf{SafeProposal}(m)$ holds, this implies $x' = x$. $\square$

Corollary 9

Single-shot PBFT satisfies Agreement.

Proof

Assume two correct processes decide on values $x$ and $x'$ in views v and $v'$, respectively. Then

$$\begin{aligned} \mathsf{committed}(C, v, \mathsf{hash}(x)) \wedge \mathsf{committed}(C', v', \mathsf{hash}(x')) \end{aligned}$$

for some well-formed C and $C'$. By Proposition 6 we have

$$\begin{aligned} \mathsf{prepared}(C_0, v, \mathsf{hash}(x)) \wedge \mathsf{prepared}(C'_0, v', \mathsf{hash}(x')) \end{aligned}$$

for some well-formed $C_0$ and $C'_0$. Without loss of generality assume $v \le v'$. If $v = v'$, then $x= x'$ by Proposition 4. If $v < v'$, then $x= x'$ by Lemma 15. $\square$

Liveness and latency Assume that the protocol is used with a synchronizer satisfying Properties 1–5 in Fig. 2. To simplify the following latency analysis, we assume $d = 2\delta$, as for FastSync (the liveness proof in the general case is virtually identical to the one given here). The next theorem states requirements on a view sufficient for the protocol to reach a decision and quantifies the resulting latency.

Theorem 3

Consider an execution of single-shot PBFT with an eventual message delay bound $\delta$, and let $v \ge {\mathcal {V}}$ be a view such that $F(v) \ge 6\delta$ and $\mathsf{leader}(v)$ is correct. Then all correct processes decide in view v by $E_{\mathrm{last}}(v)+4\delta$.

Proof

By Property 2, we have $E_{\mathrm{first}}(v) \ge \mathsf{GST}$, so that all messages sent by correct processes after $E_{\mathrm{first}}(v)$ get delivered to all correct processes within $\delta$. Once a correct process enters v, it sends its $\mathtt{NEWLEADER}$ message, so that $\mathsf{leader}(v)$ is guaranteed to receive a quorum of such messages by $E_{\mathrm{last}}(v) + \delta$. When this happens, the leader will send its proposal in a $\mathtt{PROPOSE}$ message, which correct processes will receive by $E_{\mathrm{last}}(v)+2\delta$. If they deem the proposal safe, it takes them at most $2\delta$ to exchange the sequence of $\mathtt{PREPARED}$ and $\mathtt{COMMITTED}$ messages leading to decisions. By (2), all correct processes will stay in v until at least $E_{\mathrm{last}}(v)+(F(v) - d) \ge E_{\mathrm{last}}(v)+4\delta$ and thus will not send a message with a view $>v$ until this time. Then none of the above messages will be discarded at correct processes before this time, and assuming the safety checks pass, the sequence of message exchanges will lead to decisions by $E_{\mathrm{last}}(v)+4\delta$.

It remains to show that the proposal $x$ that $\mathsf{leader}(v)$ makes in view v (line 5) will be deemed safe by all correct processes according to the $\mathsf{SafeProposal}$ predicate (line 11). All the conjuncts of $\mathsf{SafeProposal}$ except for $\mathsf{valid}(x)$ are trivially satisfied given that $\mathsf{leader}(v)$ is correct. If the leader is choosing its own proposal as $x$, then it is valid because correct processes propose valid values. Otherwise, from $\mathsf{ValidNewLeader}$ we get that $\mathsf{prepared}(C, {\_} , \mathsf{hash}(x))$ for a well-formed C. Hence, by Proposition 7 we again have $\mathsf{valid}(x)$. $\square$

Since by Property 3 correct processes enter every view starting from ${\mathcal {V}}$ and, by the definition of $\mathsf{leader}()$, leaders rotate round-robin, we are always guaranteed to encounter a correct leader after at most f view changes. Then Theorem 3 implies that the protocol is live when the timeouts are high enough.

Corollary 10

Consider an execution with an eventual message delay bound $\delta$, and assume that (1) holds for $u= 6\delta$. Then in this execution single-shot PBFT satisfies Termination.

We can ensure that single-shot PBFT is always live by picking a function $F$ that grows without bound. Alternatively, we can prevent timeouts from growing unboundedly by picking $F$ that satisfies (3) for $U= 6\Delta$: then by Proposition 1, (1) holds for $u= 6\delta$.

When single-shot PBFT is used with the FastSync synchronizer, rather than an arbitrary one, we can use Properties A–C in Fig. 2 to bound how quickly the protocol reaches a decision after $\mathsf{GST}$. To this end, we combine Theorem 3 with Property  C, which bounds the latency of view synchronization when the protocol is started before $\mathsf{GST}$, and Proposition 2, which bounds the latency of going through up to f views with faulty leaders.

Corollary 11

Let $v = \mathsf{GV}(\mathsf{GST}+\rho )+1$ and assume that $S_{\mathrm{first}}< \mathsf{GST}$, $F(v) \ge 6\delta$ and $S_{f+1} \le \mathsf{GST}+ \rho$. Then in single-shot PBFT all correct processes decide by $\mathsf{GST}+ \rho + \sum _{k=v-1}^{v+f-1} (F(k)+\delta ) + 6\delta$.

We can also quantify the latency of the protocol under favorable conditions, when it is started after $\mathsf{GST}$. In this we rely on Property B, which gives conditions under which processes synchronize in view 1. The following corollary of Theorem 3 exploits this property to bound the latency of PBFT when it is started after $\mathsf{GST}$ and the initial timeout is set appropriately, but the protocol may still go through a sequence of up to f faulty leaders. The summation in the bound (coming from Proposition 2) quantifies the overhead in the latter case.

Corollary 12

Assume that $S_{\mathrm{first}}\ge \mathsf{GST}$ and $F(1) \ge 6\delta$. Then in single-shot PBFT all correct processes decide by $S_{\mathrm{last}}+\sum _{k=1}^{f} (F(k)+\delta ) + 5\delta$.

Finally, the next corollary bounds the latency when additionally the leader of view 1 is correct, in which case the protocol can benefit from the optimized execution of this view noted earlier. The corollary follows from Property B and an easy strengthening of Theorem 3 for the special case of $v = {\mathcal {V}}=1$.

Corollary 13

Assume that $S_{\mathrm{first}}\ge \mathsf{GST}$, $F(1) \ge 5\delta$ and $\mathsf{leader}(1)$ is correct. Then in single-shot PBFT all correct processes decide by $S_{\mathrm{last}}+ 4\delta$.

Assume that $F$ is such that (3) holds for $U= 6\Delta$; then as we noted above, single-shot PBFT with FastSync is live. Furthermore, under the conditions of Corollaries 11 and 12, the latency of the protocol is bounded even when it has to go through multiple views before deciding: by $\mathsf{GST}+ \rho + (6\Delta +\delta )(f+1) + 6\delta$ if starting before $\mathsf{GST}$, and by $S_{\mathrm{last}}+(6\Delta +\delta )f + 5\delta$ if starting after $\mathsf{GST}$.

Communication complexity To reach a decision in a single view with a correct leader, the protocol requires exchanging messages with $O(n^3)$ signatures: this is because the leader has to forward prepared certificates to processes together with its proposal to prove the correctness of the latter. This can be lowered to $O(n^2)$ by using threshold signatures, which combine multiple signatures into one [31]. We next consider a protocol that lowers the communication complexity further.

5.2 Single-shot HotStuff

We consider the more recent HotStuff protocol [45]. The protocol was originally presented as solving an inherently multi-shot problem, agreeing on a hash-chain of blocks. In Algorithm 3 we present its single-shot version that concisely expresses the key idea and allows comparing the protocol with others. For brevity, we also eschew the use of threshold signatures, used in the original presentation. This still yields a protocol with lower communication complexity than PBFT.

HotStuff delegated view synchronization to a separate component [45], but did not provide its practical implementation or analyze how view synchronization affects the protocol latency. We show that our single-shot version of HotStuff is live when used with a synchronizer satisfying the specification in Sect. 3 and give precise bounds on its latency. We also show that the protocol requires only bounded space when using our synchronizer FastSync.

Like single-shot PBFT, the protocol in Algorithm 3 switches views when told by the synchronizer, with view leaders rotating round-robin. However, the leader’s proposal is processed in three phases instead of two. The protocol starts in the same way as PBFT: processes send $\mathtt{NEWLEADER}$ messages with prepared certificates to the leader (line 4), the leader chooses its proposal as before and distributes it in a $\mathtt{PROPOSE}$ message (line 11). The processes then assemble prepare certificates by exchanging $\mathtt{PREPARED}$ messages (line 16), so that Proposition 4 still holds. However, after forming a prepared certificate for a value, a process participates in an additional message exchange: it disseminates a $\mathtt{PRECOMMITTED}$ message with the hash of the value and waits until it gathers a quorum of $\mathtt{PRECOMMITTED}$ messages matching the prepared value (line 22). This ensures that at least $f+1$ correct processes have prepared the value $x$. Since the leader of the next view will gather prepared commands from at least $2f+1$ processes, at least one correct process will tell the leader about the value $x$, and thus the leader will be aware of this value as a potential decision in the current view.

Having gathered a quorum of $\mathtt{PRECOMMITTED}$ messages for a value, the process becomes locked on this value, which is recorded by setting a special variable $\mathsf{locked\_view}$ to the current view. From this point on, the process will not accept a proposal of a different value from a leader of a future view, unless the leader can convince the process that no decision was reached in the current view. This is ensured by the $\mathsf{SafeProposal}$ check the process does on a $\mathtt{PROPOSE}$ message from a leader (line 12):

$$\begin{aligned}&\mathsf{SafeProposal}(\langle \mathtt{PROPOSE}(v, x, C) \rangle _j) \iff \nonumber \\&\quad p_j = \mathsf{leader}(v) \wedge \mathsf{valid}(x) \wedge {} \nonumber \\&\quad (\mathsf{locked\_view}\not = 0 {\implies } x= \mathsf{prepared\_val}\vee {} \nonumber \\&\quad (\exists v'.\, v> v'>\mathsf{locked\_view}\wedge \mathsf{prepared}(C, v', \mathsf{hash}(x)))). \end{aligned}$$

(20)

This checks that the value is valid and that, if the process has previously locked on a value, then either the leader proposes the same value, or its proposal is justified by a prepared certificate from a higher view than the lock. In the latter case the process can be sure that no decision was reached in the view it is locked on.

Having locked a value, the process participates in the final message exchange: it disseminates a $\mathtt{COMMITTED}$ message with the hash of the value and waits until it assembles a committed certificate (line 26). Once a process assembles a committed certificate for a value $x$, it decides on $x$. Assembling a committed certificate for $x$ ensures that at least $f+1$ correct processes are locked on the same value. This guarantees that a leader in a future view cannot get processes to decide on a different value: this would require $2f+1$ processes to accept the leader’s proposal; but at least one correct process out of these would be locked on $x$ and would refuse to accept a different value due to the $\mathsf{SafeProposal}$ check. Thus, while the exchange of $\mathtt{PRECOMMITTED}$ messages ensures that a future correct leader will be aware of the value being decided and will be able to make a proposal passing $\mathsf{SafeProposal}$ checks (liveness), the exchange of $\mathtt{COMMITTED}$ ensures that a faulty leader cannot revert the decision (safety).

Note that, when a process enters view 1, it trivially knows that no decision could have been reached in prior views. Hence, the leader of view 1 can send its proposal immediately, without waiting to receive a quorum of $\mathtt{NEWLEADER}$ messages (line 10), and processes can avoid sending these messages to this leader. For brevity, we omit this optimization from the pseudocode, even though we take it into account in our latency analysis.

Since the synchronizer is not guaranteed to switch processes between views all at the same time, a process in a view v may receive a message from a higher view $v' > v$, which needs to be stored in case the process finally switches to $v'$. If implemented naively, this would require a process to store unboundedly many messages. Instead, we allow a process to store, for each message type and sender, only the message of this type received from this sender that has the highest view. As we show below (Theorem 4), this does not violate liveness. Thus, assuming consensus proposals of bounded size, the protocol in Algorithm 3 runs in bounded space, and so does the overall consensus protocol with the FastSync synchronizer.

Safety First note that, due to Property 1 of the synchronizer, we have

Proposition 8

The variables $\mathsf{locked\_view}$, $\mathsf{prepared\_view}$ and $\mathsf{curr\_view}$ at a correct process never decrease and we always have $\mathsf{locked\_view}\le \mathsf{prepared\_view}\le \mathsf{curr\_view}$.

The Validity property of consensus is proved like for PBFT (Sect. 5.1). The Agreement property follows from the following analog of Lemma 15.

Lemma 16

$$\begin{aligned} \forall v, v', C, C', x, x'.\,&\mathsf{committed}(C, v, \mathsf{hash}(x)) \wedge {} \\&\mathsf{prepared}(C', v', \mathsf{hash}(x')) \wedge {} \\&\mathsf{wf}(C) \wedge \mathsf{wf}(C') \wedge v < v' {\implies } x= x'. \end{aligned}$$

Proof

Fix v, C and $x$, and assume $\mathsf{committed}(C, v, \mathsf{hash}(x))$ and $\mathsf{wf}(C)$. We prove by induction on $v'$ that

$$\begin{aligned}&\forall v', C', x'.\, \mathsf{prepared}(C', v', \mathsf{hash}(x')) \wedge \mathsf{wf}(C') \wedge v < v' \\&{\implies } x= x'. \end{aligned}$$

Assume this holds for all $v' < v^*$; we now prove it for $v' = v^*$. To this end, assume $v < v'$ and $\mathsf{prepared}(C', v', \mathsf{hash}(x'))$ for a well-formed $C'$.

Since $\mathsf{committed}(C, v, \mathsf{hash}(x))$ and $\mathsf{wf}(C)$, a quorum Q of processes sent $\mathtt{COMMITTED}(v, \mathsf{hash}(x))$. Since $\mathsf{prepared}(C', v', \mathsf{hash}(x'))$ and $\mathsf{wf}(C')$, a quorum $Q'$ of processes sent $\mathtt{PREPARED}(v', \mathsf{hash}(x'))$. The quorums Q and $Q'$ have to intersect in some correct process $p_k$, which has thus sent both $\mathtt{COMMITTED}(v, \mathsf{hash}(x))$ and $\mathtt{PREPARED}(v', \mathsf{hash}(x'))$. Since $v< v'$, process $p_k$ must have sent $\mathtt{COMMITTED}(v, \mathsf{hash}(x))$ before $\mathtt{PREPARED}(v', \mathsf{hash}(x'))$. Before sending $\mathtt{COMMITTED}(v, \mathsf{hash}(x))$ the process set $\mathsf{locked\_view}$ to v (line 24) and had $\mathsf{prepared\_val}=x$.

Assume towards a contradiction that $x\not = x'$. Let $v''$ be the first view after v when $p_k$ prepared some proposal $x'' \not = x$, so that $v'' \le v'$. When this happened, by Proposition 8 process $p_k$ must have had $\mathsf{prepared\_val}= x$ and $\mathsf{locked\_view}\ge v$. Then by the $\mathsf{SafeProposal}$ check (line 12), the leader of $v''$ provided a well-formed prepared certificate $C''$ such that $\mathsf{prepared}(C'', v''', \mathsf{hash}(x''))$ for $v'''$ such that $v< v''' < v'' \le v'$. But then by induction hypothesis we have $x'' = x$, and above we established $x'' \not = x$: a contradiction. Hence, we must have $x= x'$, as required. $\square$

Corollary 14

Single-shot HotStuff satisfies Agreement.

Proof

Analogous to the proof of Corollary 9, but using Lemma 16 instead of Lemma 15. $\square$

Liveness and latency Assume that the protocol is used with a synchronizer satisfying Properties 1–5 in Fig. 2; to simplify the following latency analysis, we assume $d = 2\delta$, as for FastSync. The next theorem states requirements on a view sufficient for the protocol to reach a decision and quantifies the resulting latency.

Theorem 4

Consider an execution of single-shot HotStuff with an eventual message delay bound $\delta$, and let $v \ge {\mathcal {V}}$ be a view such that $F(v) \ge 7\delta$ and $\mathsf{leader}(v)$ is correct. Then all correct processes decide in view v by $E_{\mathrm{last}}(v)+5\delta$.

Proof

Once a correct process enters v, it sends its $\mathtt{NEWLEADER}$ message, so that $\mathsf{leader}(v)$ is guaranteed to receive a quorum of such messages by $E_{\mathrm{last}}(v) + \delta$. When this happens, the leader will send its proposal in a $\mathtt{PROPOSE}$ message, which correct processes will receive by $E_{\mathrm{last}}(v)+2\delta$. If they deem the proposal safe, it takes them at most $3\delta$ to exchange the sequence of $\mathtt{PREPARED}$, $\mathtt{PRECOMMITTED}$ and $\mathtt{COMMITTED}$ messages leading to decisions. By (2), all correct processes will stay in v until at least $E_{\mathrm{last}}(v)+(F(v) - d) \ge E_{\mathrm{last}}(v)+5\delta$, and thus will not send a message with a view $>v$ until this time. Then none of the above messages will be discarded at correct processes before this time, and assuming the safety checks pass, the sequence of message exchanges will lead to decisions by $E_{\mathrm{last}}(v)+5\delta$.

It remains to show that the proposal $\mathsf{leader}(v)$ makes in view v (line 5) will satisfy $\mathsf{SafeProposal}$ at all correct processes (line 12). It is easy to show that the proposal satisfies $\mathsf{valid}$, so we now need to prove the last conjunct of $\mathsf{SafeProposal}$. This trivially holds if no correct process is locked on a value when receiving the $\mathtt{PROPOSE}$ message from the leader.

We now consider the case when some correct process is locked on a value when receiving the $\mathtt{PROPOSE}$ message, and let $p_i$ be a process that is locked on the highest view among correct processes. Let $x= p_i.\mathsf{prepared\_val}$ be the value locked and $v_0 = p_i.\mathsf{locked\_view}< v$ be the corresponding view. Since $p_i$ locked $x$ at $v_0$, it must have previously received messages $\mathtt{PRECOMMITTED}(v_0, \mathsf{hash}(x))$ from a quorum of processes (line 22), at least $f+1$ of which have to be correct. The latter processes must have assembled a prepared certificate for the value $x$ at view $v_0$ (line 16). By Proposition 8, when each of these $f+1$ correct processes enters view v, it has $\mathsf{prepared\_view}\ge v_0$ and thus sends the corresponding value and its prepared certificate in the $\mathtt{NEWLEADER}(v, \ldots )$ message to $\mathsf{leader}(v)$. The leader is guaranteed to receive at least one of these messages before making a proposal, since it only does this after receiving at least $2f+1$ $\mathtt{NEWLEADER}$ messages (line 5). Hence, the leader proposes a value $x'$ with a prepared certificate formed at some view $v' \ge v_0$ no lower than any view that a correct process is locked on when receiving the leader’s proposal. Furthermore, if $v' = v_0$, then by Proposition 4 we have that $x' = x$ and $x$ is the only value that can be locked by a correct process at $v_0$. Hence, the leader’s proposal will satisfy $\mathsf{SafeProposal}$ at each correct process. $\square$

Corollary 15

Consider an execution with an eventual message delay bound $\delta$, and assume that (1) holds for $u= 7\delta$. Then in this execution single-shot HotStuff satisfies Termination.

Similarly to Sect. 5.1, when the protocol is used with the FastSync synchronizer, we can quantify its latency in both unfavorable scenarios (when starting before $\mathsf{GST}$) and favorable scenarios (when starting after $\mathsf{GST}$). The first corollary of Theorem 5 below uses Property  C and Proposition 2, and the following two corollaries, Property B. Like in Sect. 5.2, the last corollary takes into account the optimized execution of view 1.

Corollary 16

Let $v = \mathsf{GV}(\mathsf{GST}+\rho )+1$ and assume that $S_{\mathrm{first}}< \mathsf{GST}$, $F(v) \ge 7\delta$ and $S_{f+1} \le \mathsf{GST}+ \rho$. Then in single-shot HotStuff all correct processes decide by $\mathsf{GST}+ \rho + \sum _{k=v-1}^{v+f-1} (F(k)+\delta ) + 7\delta$.

Corollary 17

Assume that $S_{\mathrm{first}}\ge \mathsf{GST}$ and $F(1) \ge 7\delta$. Then in single-shot HotStuff all correct processes decide by $S_{\mathrm{last}}+\sum _{k=1}^{f} (F(k)+\delta ) + 6\delta$.

Corollary 18

Assume that $S_{\mathrm{first}}\ge \mathsf{GST}$, $F(1) \ge 6\delta$, and $\mathsf{leader}(1)$ is correct. Then in single-shot HotStuff all correct processes decide by $S_{\mathrm{last}}+ 5\delta$.

Assume that $F$ is such that (3) holds for $U= 7\Delta$. Then by Proposition 1 and Corollary 15 single-shot HotStuff with FastSync is live. Furthermore, under the conditions of Corollaries 16 and 17 its latency is bounded by $\mathsf{GST}+ \rho + (7\Delta +\delta )(f+1) + 7\delta$ if starting before $\mathsf{GST}$, and by $S_{\mathrm{last}}+(7\Delta +\delta )f + 6\delta$ if starting after $\mathsf{GST}$. As expected, the latency bounds for HotStuff are higher than those for PBFT (Sect. 5.1) due to an extra message exchange.

Communication complexity To reach a decision in a single view with a correct leader, the protocol requires exchanging messages with $O(n^2)$ signatures. Using threshold signatures, this communication complexity can be lowered to O(n) [45]. To this end, instead of performing an all-to-all message exchange processes can send partial signatures to the leader, which aggregates them into a single threshold signature and distributes it to processes. Our results can be easily adjusted to this variant of the protocol.

5.3 Two-phase HotStuff

We next consider a two-phase variant of HotStuff [45], which processes the leader’s proposals in two phases instead of three (Algorithm 4). To keep the same communication complexity as the three-phase HotStuff, the two-phase version uses timeouts not just for view synchronization, but also in the core consensus protocol to delimit different stages of a single view. This is similar to Tendermint [14] and Casper [15], which use timeouts for the same purposes. By handling two-phase HotStuff we demonstrate that our synchronizer specification is strong enough to deal with interactions between the timeouts in different parts of the overall protocol. We also show that the protocol requires only bounded space when used with our FastSync synchronizer.

In two-phase HotStuff, a process handles a proposal from the leader in the same way as in the three-phase one, by sending a $\mathtt{PREPARED}$ message (line 14 in Algorithm 4). Upon assembling a prepared certificate for a value $x$ (line 19), a process stores the value in $\mathsf{prepared\_val}$ and the certificate in $\mathsf{cert}$. In contrast to HotStuff, the process then immediately becomes locked on the value, without exchanging $\mathtt{PRECOMMITTED}$ messages; this is recorded by assigning $\mathsf{locked\_view}$ to the current view (the $\mathsf{prepared\_view}$ variable is thus unnecessary). The process then sends a $\mathtt{COMMITTED}$ message with the hash of the locked value, and assembling a quorum of such messages causes the process to decide on the value (line 25). Upon entering a new view (line 1), a process sends to the leader a $\mathtt{NEWLEADER}$ message with the information about the last value it prepared, and therefore locked (line 7). The leader computes its proposal from $\mathtt{NEWLEADER}$ messages in the same way as in three-phase HotStuff (line 10).

The two-phase version of HotStuff satisfies Validity and Agreement for the same reasons as the three-phase one: as we noted in Sect. 5.2, the exchange of $\mathtt{PRECOMMITTED}$ messages, omitted from the current protocol, is only needed for liveness, not safety. However, ensuring liveness in two-phase HotStuff requires a different mechanism: since a correct process $p_i$ gets locked on a value immediately after preparing it, gathering prepared values from an arbitrary quorum of processes is not enough for the leader to ensure it will make a proposal that will pass the $\mathsf{SafeProposal}$ check at $p_i$: the quorum may well exclude this process. To solve this problem, the leader waits before making a proposal so that eventually in some view it will receive $\mathtt{NEWLEADER}$ messages from all correct processes. This ensures the leader will eventually make a proposal that will pass the $\mathsf{SafeProposal}$ checks at all of them. In more detail, when a process enters a view where it is the leader, it sets a special timer $\mathsf{timer\_newleader}$ for the duration determined by a function $F_{p}$. The leader makes a proposal only after the timer expires (line 8).

For the leader to make an acceptable proposal, the duration of $\mathsf{timer\_newleader}$ needs to be long enough for all $\mathtt{NEWLEADER}$ messages for this view from correct processes to reach the leader. For the protocol to decide, after $\mathsf{timer\_newleader}$ expires, processes also need to stay in the view long enough to complete the necessary message exchanges. The following theorem characterizes these requirements formally, again assuming $d = 2\delta$ in Property 4. Note that in the proof of the theorem we rely on the guarantees about the timing of correct processes entering a view (Property 4) to show that $\mathsf{timer\_newleader}$ fulfills its intended function.

Theorem 5

Consider an execution of two-phase HotStuff with an eventual message delay bound $\delta$, and let $v \ge {\mathcal {V}}$ be a view such that $F_{p}(v) \ge 3\delta$, $F(v) - F_{p}(v) \ge 5\delta$ (so that $F(v) \ge 8\delta$) and $\mathsf{leader}(v)$ is correct. Then all correct processes decide in view v by $E_{\mathrm{last}}(v)+F_{p}(v)+3\delta$.

Proof

Once a correct process enters v, it sends its $\mathtt{NEWLEADER}$ message, so that $\mathsf{leader}(v)$ is guaranteed to receive such messages from all correct processes by $E_{\mathrm{last}}(v) + \delta$. By Property 4 of the synchronizer, the leader enters v by $E_{\mathrm{last}}(v)-2\delta$ at the earliest. Since the leader starts its $\mathsf{timer\_newleader}$ when it enters v and $F_{p}(v) \ge 3\delta$, the leader is guaranteed to receive $\mathtt{NEWLEADER}$ messages from all correct processes before $\mathsf{timer\_newleader}$ expires. When $\mathsf{timer\_newleader}$ expires, which happens no later than $E_{\mathrm{last}}(v)+F_{p}(v)$, the leader will send its proposal in a $\mathtt{PROPOSE}$ message, which correct processes will receive by $E_{\mathrm{last}}(v)+F_{p}(v)+\delta$. If they deem the proposal safe, it takes them at most $2\delta$ to exchange the sequence of $\mathtt{PREPARED}$ and $\mathtt{COMMITTED}$ messages leading to decisions. By (2), all correct processes will stay in v until at least $E_{\mathrm{last}}(v)+(F(v) - d) \ge E_{\mathrm{first}}(v)+F_{p}(v)+3\delta$. Then none of the above messages will be discarded at correct processes before this time, and assuming the safety checks pass, the sequence of message exchanges will lead to decisions by $E_{\mathrm{last}}(v)+F_{p}(v)+3\delta$.

It remains to show that the proposal $\mathsf{leader}(v)$ makes in view v (line 8) will satisfy $\mathsf{SafeProposal}$ at all correct processes (line 14). It is easy to show that this proposal satisfies $\mathsf{valid}$, so we now need to prove the last conjunct of $\mathsf{SafeProposal}$. This trivially holds if no correct process is locked on a value when receiving the $\mathtt{PROPOSE}$ message from the leader.

We now consider the case when some correct process is locked on a value when receiving the $\mathtt{PROPOSE}$ message, and let $p_i$ be a process that is locked on the highest view among correct processes. Let $x= p_i.\mathsf{prepared\_val}$ be the value locked and $v_0 = p_i.\mathsf{locked\_view}< v$ be the corresponding view. Since $\mathsf{leader}(v)$ receives all of the $\mathtt{NEWLEADER}$ messages sent by correct processes before making its proposal, it proposes a value $x'$ with a prepared certificate formed at some view $v' \ge v_0$. Also, if $v' = v_0$, then by Proposition 4, $x' = x$ and $x$ is the only value that can be locked by a correct process at $v_0$. Hence, the leader’s proposal will satisfy $\mathsf{SafeProposal}$ at each correct process. $\square$

Corollary 19

Consider an execution with an eventual message delay bound $\delta$, and assume that $F$ is such that (1) holds respectively for $F$ and $u= 8\delta$, and for $F-F_{p}$ and $u= 5\delta$. Then in this execution two-phase HotStuff satisfies Termination.

Thus, one way to ensure the liveness of two-phase HotStuff is to pick functions $F$ and $F_{p}$ such that both of these, as well as the difference between them, grow without bound. This can be satisfied, e.g., by letting $F(v) = 2v$ and $F_{p}(v) = v$. By Proposition 1, another way to ensure liveness is to pick $F$ such that (3) holds for $U= 8\Delta$, and $F_{p}$ is such that the same property holds for $U= 3\Delta$; this option prevents the timeouts from growing unboundedly.

Latency The following corollaries of Theorem 4 quantify the latency of two-phase HotStuff with the with the FastSync synchronizer in different scenarios. The first corollary uses Property  C and Proposition 2, and the following two corollaries, Property B. Like in Sect. 5.1, the last corollary takes into account the optimized execution of view 1.

Corollary 20

Let $v = \mathsf{GV}(\mathsf{GST}+\rho )+1$ and assume that $S_{\mathrm{first}}< \mathsf{GST}$, $S_{f+1} \le \mathsf{GST}+ \rho$, $F_{p}(v) \ge 3\delta$ and $F(v) - F_{p}(v) \ge 5\delta$. Then in two-phase HotStuff all correct processes decide by $\mathsf{GST}+ \rho + \sum _{k=v-1}^{v+f-1} (F(k)+\delta ) + F_{p}(v+f) + 5\delta$.

Corollary 21

Assume that $S_{\mathrm{first}}\ge \mathsf{GST}$, $F_{p}(1) \ge 3\delta$ and $F(1) - F_{p}(1) \ge 5\delta$. Then in two-phase HotStuff all correct processes decide by $S_{\mathrm{last}}+\sum _{k=1}^{f} (F(k)+\delta ) + F_{p}(f+1) + 4\delta$.

Corollary 22

Assume that $S_{\mathrm{first}}\ge \mathsf{GST}$, $F(1) \ge 5\delta$ and $\mathsf{leader}(1)$ is correct. Then in two-phase HotStuff all correct processes decide by $S_{\mathrm{last}}+ 4\delta$.

Assume that $F$ is such that (3) holds for $U= 8\Delta$, and $F_{p}$ is such that the same property holds for $U= 3\Delta$; then as we noted above, two-phase HotStuff with FastSync is live. Furthermore, under the conditions of Corollaries 20 and 21 its latency is bounded by $\mathsf{GST}+ \rho + (8\Delta +\delta )(f+1) + 3\Delta + 5\delta$ if starting before $\mathsf{GST}$, and by $S_{\mathrm{last}}+(8\Delta +\delta )f + 3\Delta + 4\delta$ if starting after $\mathsf{GST}$.

The latency bounds we established allow us to compare the two-phase version of HotStuff with the its three-phase version (Sect. 5.2) and PBFT (Sect. 5.1). In the ideal case when the network is synchronous, the timeouts are set to the minimal values ensuring liveness, and the leader of view 1 is correct, two-phase HotStuff has the same latency as PBFT and a lower latency than three-phase HotStuff: $4\delta$ in Corollaries 13 and 22 vs $5\delta$ in Corollary 18. When the initial leader is faulty, all protocols incur the overhead of switching through several views until they encounter a correct leader (Corollaries 12, 17 and 21). In this case, the latency of deciding in the first view with a correct leader is at most $6\delta$ for three-phase HotStuff, $5\delta$ for PBFT and $F_{p}(f+1) + 4\delta$ for two-phase one. In the worst case the latency of two-phase HotStuff is $F_{p}(f+1) + 4\delta \le 3\Delta + 4\delta$. This is much higher than the latency of the other protocols, since in practice $\Delta$ gives only a conservative estimate of the message delay. But even when $F_{p}(f+1)$ is the optimal $3\delta$, the two-phase HotStuff bound yields $7\delta$—a higher latency than for three-phase HotStuff and PBFT. The latency bounds for the case of starting before $\mathsf{GST}$ relate similarly (Corollaries 11, 16 and 20). The higher latency of two-phase HotStuff in these cases are caused by the inclusion of the timeout $F_{p}(f+1)$, which reflects the lack of “optimistic responsiveness” of this protocol [45].

5.4 Summary and additional case studies

We have shown that our synchronizer specification is strong enough to guarantee liveness under partial synchrony for three Byzantine consensus protocols using different approaches:

• In PBFT the leader proposals go through two phases of message exchanges. Both safety and liveness are ensured by the leader sending supporting information together with its proposal that allows processes to verify the proposal’s correctness.

• HotStuff lowers the communication complexity by reducing the amount of supporting information the leader has to send with its proposal. Achieving liveness then requires an additional message exchange to ensure that the leader has an up-to-date information when making its proposal.

• Two-phase HotStuff eliminates the extra message exchange of HotStuff and instead ensures liveness using a timeout within a view: the leader waits until it receives the information from all correct processes before making its proposal.

To further demonstrate the wide applicability of our synchronizer specification, we have also used it to prove the correctness and analyze the latency of single-shot versions of SBFT [31] and Tendermint [14]. We defer the details to [12, §B]. SBFT is a recent improvement of PBFT that adds a fast path for cases when all processes are correct, and our analysis quantifies the latency of both paths. Tendermint is similar to two-phase HotStuff; in particular, it also processes leader proposals in two phases and uses timeouts both for view synchronization and to delimit different stages of a single view. However, the protocol never sends messages with certificates, and thus, like FastSync, does not need digital signatures. Tendermint integrates the functionality required for view synchronization with the core consensus protocol, breaking its control flow in multiple places. We consider its variant that delegates this functionality to the synchronizer, thus simplifying the protocol. Our analysis of the resulting protocol is similar to the one of two-phase HotStuff in Sect. 5.3. Apart from deriving latency bounds for the protocol, our analysis exploits the synchronizer specification to give a proof of its liveness that is more rigorous than the existing ones [6, 14], which lacked a detailed correctness argument for the view synchronization mechanism used in the protocol.

6 Related work

Most Byzantine consensus protocols are based on the concept of views (aka rounds), and thus include a mechanism for view synchronization. This mechanism is typically integrated with the core consensus protocol, which complicates the design [14, 19, 31]. Subtle view synchronization mechanisms have often come without a proof of liveness (e.g., PBFT [18]) or had liveness bugs (e.g., Tendermint [5] and Casper [35]). Furthermore, liveness proofs have not usually given concrete bounds on the latency of reaching a decision (exceptions are [4, 39]).

Several papers suggested separating the functionality of view synchronization into a distinct component, including the seminal DLS paper on consensus under partial synchrony [27] and its more modern implementation [25]. DLS specified the guarantees provided by view synchronization indirectly, by proving that its implementation simulated an abstract computational model with a built-in notion of rounds. The model guarantees that, eventually, a process in a round r receives all messages sent by correct processes in r. This property is needlessly strong for Byzantine consensus, since protocols such as PBFT (Sect. 5.1) and HotStuff (Sect. 5.2) can make progress in a given view if they receive messages from any quorum; executing such protocols in the DLS model would thus undermine their optimistic responsiveness [45]. DLS implemented rounds using a distributed protocol that synchronizes process-local clocks obtained by counting state transitions of each process. This protocol has to synchronize local clocks on every step of the consensus algorithm, which results in prohibitive communication overheads and makes this solution impractical.

Abraham et al. [1] build upon ideas from fault-tolerant clock synchronization [24, 43] to implement view synchronization assuming that processes have access to hardware clocks with bounded drift. But this work only gives a solution for a synchronous system. Our FastSync synchronizer also assumes hardware clocks but removes the assumption of bounded drift before $\mathsf{GST}$, thus making them compatible with partial synchrony. We note that, although the problems of clock and view synchronization are different, they are closely related at the algorithmic level. We therefore believe that our view synchronization techniques can in the future be adapted to obtain an efficient partially synchronous clock synchronization protocol.

The HotStuff protocol [45] delegated the functionality of view synchronization to a separate component, called a pacemaker. But it did not provide a formal specification of this component or a practical implementation. To address this, Naor et al. have recently formalized view synchronization as a separate problem [41, 42]. Unlike us, they did not provide a comprehensive study of the applicability of their specifications to a wide range of modern Byzantine consensus protocols. In particular, their specifications do not expose bounds on how quickly processes switch views (Property 4 in Fig. 2), which are necessary for protocols such as two-phase HotStuff (Sect. 5.3) and Tendermint (Sect. 5.4).

Naor et al. also proposed synchronizer implementations in a simplified variant of partial synchrony where $\delta$ is known a priori, and messages sent before $\mathsf{GST}$ are guaranteed to arrive by $\mathsf{GST}+ \delta$ [41, 42]. These implementations focus on optimizing communication complexity, making it linear in best-case scenarios [41] or in expectation [42]. They achieve linearity by relying on digital signatures (more precisely, threshold signatures), which FastSync eschews. Unlike FastSync, they also require unbounded space (for the reasons explained in Sect. 3.1). Finally, we give exact latency bounds for FastSync under both favorable and unfavorable conditions whereas [41, 42] only provide expected latency analysis. It is interesting to investigate whether the benefits of the two approaches can be combined to tolerate message loss before $\mathsf{GST}$ with both bounded space and a low communication complexity.

DiemBFT [44] extends HotStuff with a view synchronization mechanism, integrated with the core protocol; the protocol assumes reliable channels. DiemBFT is optimized to solve repeated consensus, whereas in this paper we focus on single-shot one.

The original idea of using synchronizers to simulate a round-based synchronous system on top of an asynchronous one is due to Awerbuch [8]. This work however, did not consider failures. Augmented round models to systematically study properties of distributed consensus under various failure and environment assumptions were proposed in [10, 22, 29, 36]. These papers however, do not deal with implementing the proposed models under partial synchrony. Upper bounds for deciding after $\mathsf{GST}$ in round-based crash fault-tolerant consensus algorithms were studied in [3, 26]. While we derive similar bounds for Byzantine failures, it remains open if these are optimal or can be further improved. Failure detectors [20, 21], which abstract away the timeliness guarantees of the environment, have been extensively used for developing and analyzing consensus algorithms [21, 40] in the presence of benign failures. However, since capturing all possible faulty behaviors is algorithm-specific, the classical notion of a failure detector does not naturally generalize to Byzantine settings. As a result, the existing work on Byzantine failure detectors either limits the types of failures being addressed (e.g., [38]), or focuses on other means (such as accountability [32]) to mitigate faulty behavior.

The generalized partial synchrony model stipulating the existence of a fixed but unknown post-$\mathsf{GST}$ message delay bound $\delta$ is due to [21]. The time complexity measure combining $\delta$ with an a priori known conservative message delay bound $\Delta \ge \delta$ was first introduced in [33, 34]. This work, however, assumed a stronger variant of partial synchrony where $\delta$ is unknown but holds throughout the entire execution, rather than eventually [27]. We adopt a similar metric for our latency analysis, but only require that the two bounds $\delta$ and $\Delta$ hold after $\mathsf{GST}$. To the best of our knowledge, our analysis of Byzantine consensus latency is the first one in this model.

7 Conclusion

We have proposed a modular approach for ensuring liveness in Byzantine consensus under a general variant of the partial synchrony model, which permits unlimited message loss and out-of-sync clocks before GST, and does not stipulate the knowledge of communication delay bounds after GST. To this end, we have proposed a specification of a view synchronizer that is strong enough to ensure liveness in a number of well-known Byzantine consensus algorithms. We have also shown that this specification is implementable under partial synchrony in bounded space, despite message loss before GST. We believe that our synchronizer abstraction provides a much needed tool for facilitating the design of partially synchronous Byzantine consensus protocols, and for enabling a systematic analysis of their performance guarantees. In our current work we are generalizing the results presented here from (single-shot) Byzantine consensus to Byzantine state-machine replication [13].

Appendix A: General latency bounds

We now augment the set of properties in Fig. 2 with two additional latency bounds given by Properties D and E in Fig. 3. These two properties are analogous to Properties B and C, but handle the cases when $F(1) < 2\delta$ and $F(\mathsf{GV}(\mathsf{GST}+\rho )+1)<2\delta$, respectively. We then prove Theorem 6, which generalizes Theorem 1 to establish that FastSync also satisfies Properties D and E in Fig. 3 in addition to those given in Fig. 2.

The resulting set of properties can be used to derive latency bounds for specific instantiations of the timeout function $F$. We demonstrate how to do this for an exponentially growing timeout function, which is a common choice in practice (e.g., [19]). Specifically, we prove that if $\forall v>0.\, F(v) = 2^v$, then all correct processes are guaranteed to enter a synchronized view within $O(\delta \lg {}\delta )$ after $S_{\mathrm{last}}$ if the protocol is started after $\mathsf{GST}$ (Theorem 7); and within $O(\max \{\delta \lg {}\delta , \Delta \})$ after $\mathsf{GST}+\rho$, otherwise (Corollary 23). The latter guarantees that the latency of view synchronization is bounded after $\mathsf{GST}$.

Theorem 6

Consider an execution with an eventual message delay bound $\delta$, and assume that (1) holds for $u= 2\delta$. Then there exists a view ${\mathcal {V}}$ such that in this execution FastSync satisfies all the properties in Figs. 2 and 3 for $d = 2\delta$.

To prove the Theorem 6, we first prove the following proposition, which is an easy consequence of the definition of $\mathsf{GV}$.

Proposition 9

For all views v, if a correct process enters v, then $\mathsf{GV}(E_{\mathrm{first}}(v))=v$.

Proof

By definition of $\mathsf{GV}$, $\mathsf{GV}(E_{\mathrm{first}}(v)) \ge v$. Assume by contradiction that $\mathsf{GV}(E_{\mathrm{first}}(v)) > v$. Thus, there exists a correct process that enters a view $v' > v$ at time $t' < E_{\mathrm{first}}(v)$. By Lemma 1, there exists a time $t < t'$ such that some correct process enters v at t. Thus, $E_{\mathrm{first}}(v) \le t< t' < E_{\mathrm{first}}(v)$, which is a contradiction. $\square$

The next lemma generalizes Corollary 7 to bound the latency of entering an arbitrary view $\ge \mathsf{GV}(t)+1$ for all $t \ge \overline{\mathsf{GST}}$ and $\mathsf{GV}(t)>0$.

Lemma 17

Let $t \ge \overline{\mathsf{GST}}$ and suppose that $\mathsf{GV}(t) > 0$. If for all $k \ge 1$, some correct process enters every view $\mathsf{GV}(t)+k$, then $E_{\mathrm{last}}(\mathsf{GV}(t)+k) \le t + \sum _{i=0}^{k-1} F(\mathsf{GV}(t)+i) + 3k\delta$.

Proof

By induction on $k \ge 1$. Since some correct process enters $\mathsf{GV}(t)+1$ and $\mathsf{GV}(t) > 0$, Corollary 7 implies that $E_{\mathrm{last}}(\mathsf{GV}(t)+1) \le t + F(\mathsf{GV}(t)) + 3\delta$. Thus, the required holds for the base case of $k=1$.

For the inductive step, assume that the required holds for $k=l$ where $l\ge 1$, and consider $k=l+1$. Suppose that

$$\begin{aligned} t \ge \overline{\mathsf{GST}}\wedge \mathsf{GV}(t) > 0. \end{aligned}$$

Then, by the induction hypothesis,

$$\begin{aligned} E_{\mathrm{last}}(\mathsf{GV}(t)+l) \le t + \sum _{i=0}^{l-1} F(\mathsf{GV}(t)+i) + 3l\delta . \end{aligned}$$

(21)

Since some correct process enters $\mathsf{GV}(t)+l$, $E_{\mathrm{first}}(\mathsf{GV}(t)+l)$ is defined. Thus, by Lemma 9, we have

$$\begin{aligned} \mathsf{GV}(E_{\mathrm{first}}(\mathsf{GV}(t)+l))=\mathsf{GV}(t)+l> \mathsf{GV}(t) > 0. \end{aligned}$$

Since $\mathsf{GV}$ is non-decreasing, the above implies that

$$\begin{aligned} E_{\mathrm{first}}(\mathsf{GV}(t)+l) > t \ge \overline{\mathsf{GST}}. \end{aligned}$$

Thus, by Corollary 7,

$$\begin{aligned}&E_{\mathrm{last}}(\mathsf{GV}(t)+l+1) {}\\&\quad \le E_{\mathrm{first}}(\mathsf{GV}(t)+l) + F(\mathsf{GV}(t)+l) + 3\delta {}\\&\quad \le E_{\mathrm{last}}(\mathsf{GV}(t)+l) + F(\mathsf{GV}(t)+l) + 3\delta , \end{aligned}$$

which by (21), implies

$$\begin{aligned}&E_{\mathrm{last}}(\mathsf{GV}(t)+l+1) {}\\&\quad \le E_{\mathrm{last}}(\mathsf{GV}(t)+l) + F(\mathsf{GV}(t)+l) + 3\delta {}\\&\quad \le t + \sum _{i=0}^{l-1} F(\mathsf{GV}(t)+i) + 3l\delta + F(\mathsf{GV}(t)+l) + 3\delta \\&\quad = t + \sum _{i=0}^{(l+1)-1} F(\mathsf{GV}(t)+i) + 3(l+1)\delta , \end{aligned}$$

as required. $\square$

Fig. 3

Additional FastSync latency bounds

Proof of Theorem 6

Consider an execution of FastSync and let $\delta$ be the eventual message delay bound in this execution. We first show how to select a view ${\mathcal {V}}$ such that (9) holds. We consider the following cases. First, if

$$\begin{aligned} S_{\mathrm{first}}\ge \mathsf{GST}\wedge F(1) \ge 2\delta , \end{aligned}$$

(22)

then we let ${\mathcal {V}}=1$. Since $S_{\mathrm{first}}\ge \mathsf{GST}$, the definition of $\overline{\mathsf{GST}}$ implies $\overline{\mathsf{GST}}=S_{\mathrm{first}}$, and therefore, (9) holds. Second, if

$$\begin{aligned}&S_{\mathrm{first}}< \mathsf{GST}\ \wedge \ S_{f+1}\ \le \ \mathsf{GST}+ \rho \wedge {} \nonumber \\&F(\mathsf{GV}(\mathsf{GST}+ \rho )+1) \ge 2\delta , \end{aligned}$$

(23)

then we let ${\mathcal {V}}=\mathsf{GV}(\mathsf{GST}+\rho ) + 1$. Since $S_{\mathrm{first}}< \mathsf{GST}$, the definition of $\overline{\mathsf{GST}}$ implies $\overline{\mathsf{GST}}=\mathsf{GST}+\rho$, and therefore, (9) holds. Third, if

$$\begin{aligned} S_{\mathrm{first}}\ge \mathsf{GST}\wedge F(1) < 2\delta , \end{aligned}$$

(24)

then we let ${\mathcal {V}}=\min \{v \mid F(v) \ge 2\delta \}$. Since $S_{\mathrm{first}}\ge \mathsf{GST}$, the definition of $\overline{\mathsf{GST}}$ implies $\overline{\mathsf{GST}}=S_{\mathrm{first}}$. By the monotonicity of $F$, $F(1) < 2\delta$ implies that ${\mathcal {V}}> 1 = \mathsf{GV}(S_{\mathrm{first}}) + 1$. Thus, (9) holds. Fourth, if

$$\begin{aligned}&S_{\mathrm{first}}< \mathsf{GST}\ \wedge \ S_{f+1}\ \le \ \mathsf{GST}+ \rho \ \wedge {}\nonumber \\&F(\mathsf{GV}(\mathsf{GST}+ \rho )+1) < 2\delta , \end{aligned}$$

(25)

then we let ${\mathcal {V}}=\min \{v \mid F(v) \ge 2\delta \}$. Since $S_{\mathrm{first}}< \mathsf{GST}$, the definition of $\overline{\mathsf{GST}}$ implies $\overline{\mathsf{GST}}=\mathsf{GST}+\rho$. By the monotonicity of $F$, $F(\mathsf{GV}(\mathsf{GST}+ \rho )+1) < 2\delta$ implies that ${\mathcal {V}}> \mathsf{GV}(\mathsf{GST}+ \rho )+1$, and therefore, (9) holds. In all other cases, (1) for $u = 2\delta$ implies that $F(v') \ge 2\delta$ for some view $v'$, and therefore, by the monotonicity of $F$, ${\mathcal {V}}= \max \{v', \mathsf{GV}(\overline{\mathsf{GST}}) + 1\}$ satisfies (9). Thus, by Lemma 10, Properties 1–5 in Fig. 2 hold for ${\mathcal {V}}$ chosen as above and $d=2\delta$.

To prove Property A, fix $v\ge {\mathcal {V}}$. By Property 3, all correct processes enter v. By (9), $v \ge {\mathcal {V}}\ge \mathsf{GV}(\overline{\mathsf{GST}})+1$. Given that $\mathsf{GV}$ is non-decreasing, this implies that no correct process can enter v until after $\overline{\mathsf{GST}}$. Thus, $E_{\mathrm{last}}(v) \ge E_{\mathrm{first}}(v) > \overline{\mathsf{GST}}$, and by Corollary 4 we get $E_{\mathrm{last}}(v+1) \le E_{\mathrm{last}}(v) + F(v) + \delta$, validating Property A. Next, by our choice of ${\mathcal {V}}$, (22) implies ${\mathcal {V}}=1$, and (23) implies ${\mathcal {V}}=\mathsf{GV}(\mathsf{GST}+ \rho ) + 1$. Thus, Property B follows from Corollary 6, and Property  C from Corollary 7.

We now prove Property D in Fig. 3. By our choice of ${\mathcal {V}}$, (24) implies that ${\mathcal {V}}=\min \{v \mid F(v) \ge 2\delta \}$. By Lemma 9, $\mathsf{GV}(E_{\mathrm{first}}(1)) = 1$. Since $F(1) < 2\delta$, the monotonicity of $F$ implies ${\mathcal {V}}>1$, and therefore,

$$\begin{aligned} \exists k \ge 1.\, {\mathcal {V}}= 1 + k. \end{aligned}$$

(26)

Instantiating Lemma 17 with $t=E_{\mathrm{first}}(1) > S_{\mathrm{first}}=\overline{\mathsf{GST}}$ and $\mathsf{GV}(E_{\mathrm{first}}(1))=1>0$, we get

$$\begin{aligned} E_{\mathrm{last}}(1+k) \le E_{\mathrm{first}}(1) + \sum _{i=0}^{k-1} F(1+i) + 3k\delta , \end{aligned}$$

which by (26) implies

$$\begin{aligned}&E_{\mathrm{last}}({\mathcal {V}}) \le E_{\mathrm{first}}(1) + \sum _{i=0}^{{\mathcal {V}}-2} F(1+i) + 3({\mathcal {V}}-1)\delta {}\\&\quad \le E_{\mathrm{last}}(1) + \sum _{i=0}^{{\mathcal {V}}-2} F(1+i) + 3({\mathcal {V}}-1)\delta . \end{aligned}$$

Hence, by Corollary 6, we have

$$\begin{aligned}&E_{\mathrm{last}}({\mathcal {V}}) \le S_{\mathrm{last}}+ \delta + \sum _{i=0}^{{\mathcal {V}}-2} F(i+1) + 3({\mathcal {V}}-1)\delta {}\nonumber \\&\quad = S_{\mathrm{last}}+ \sum _{i=1}^{{\mathcal {V}}-1} F(i) + (3{\mathcal {V}}-2)\delta , \end{aligned}$$

(27)

as required.

Lastly, we prove Property E in Fig. 3. By our choice of ${\mathcal {V}}$, (25) implies that ${\mathcal {V}}=\min \{v \mid F(v) \ge 2\delta \}$. By Lemma 9, $\mathsf{GV}(E_{\mathrm{first}}(\mathsf{GV}(\mathsf{GST}+\rho ) + 1)) = \mathsf{GV}(\mathsf{GST}+\rho ) + 1$. Since $F(\mathsf{GV}(\mathsf{GST}+\rho ) + 1) < 2\delta$, the monotonicity of $F$ implies ${\mathcal {V}}>\mathsf{GV}(\mathsf{GST}+\rho ) + 1$, and therefore,

$$\begin{aligned} \exists k \ge 1.\, {\mathcal {V}}= \mathsf{GV}(\mathsf{GST}+\rho ) + 1 + k. \end{aligned}$$

(28)

Instantiating Lemma 17 with $t=E_{\mathrm{first}}(\mathsf{GV}(\mathsf{GST}+\rho ) + 1) > \mathsf{GST}+\rho =\overline{\mathsf{GST}}$ and $\mathsf{GV}(E_{\mathrm{first}}(\mathsf{GV}(\mathsf{GST}+\rho ) + 1))=\mathsf{GV}(\mathsf{GST}+\rho ) + 1>0$, we get

$$\begin{aligned}&E_{\mathrm{last}}(\mathsf{GV}(\mathsf{GST}+\rho )+1+k) {}\\&\quad \le E_{\mathrm{first}}(\mathsf{GV}(\mathsf{GST}+\rho ) + 1) {}\\&\quad + \sum _{i=0}^{k-1} F(\mathsf{GV}(\mathsf{GST}+\rho ) + 1+i) + 3k\delta , \end{aligned}$$

which by (28) implies

$$\begin{aligned}&E_{\mathrm{last}}({\mathcal {V}}) \le E_{\mathrm{first}}(\mathsf{GV}(\mathsf{GST}+\rho ) + 1) {}\\&\quad + \sum _{i=0}^{{\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho )-2} F(\mathsf{GV}(\mathsf{GST}+\rho ) + 1+i) {}\\&\quad +3({\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho )-1)\delta \le {}\\&E_{\mathrm{last}}(\mathsf{GV}(\mathsf{GST}+\rho ) + 1) {}\\&\quad +\sum _{i=0}^{{\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho )-2} F(\mathsf{GV}(\mathsf{GST}+\rho ) + 1+i) {}\\&\quad +\,3({\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho )-1)\delta . \end{aligned}$$

Hence, by Corollary 7, we have

$$\begin{aligned}&E_{\mathrm{last}}({\mathcal {V}}) \le E_{\mathrm{last}}(\mathsf{GV}(\mathsf{GST}+\rho ) + 1) {}\\&\quad + \sum _{i=0}^{{\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho )-2} F(\mathsf{GV}(\mathsf{GST}+\rho ) + 1+i) {}\\&\quad + 3({\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho )-1)\delta {}\\&\quad \le \mathsf{GST}+\rho + F(\mathsf{GV}(\mathsf{GST}+\rho )) + 3\delta {}\\&\quad + \sum _{i=0}^{{\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho )-2} F(\mathsf{GV}(\mathsf{GST}+\rho ) + 1+i) {}\\&\quad + 3({\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho )-1)\delta {}\\&\quad = \mathsf{GST}+\rho + \sum _{i=0}^{{\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho )-1} F(\mathsf{GV}(\mathsf{GST}+\rho )+i) {}\\&\quad +3({\mathcal {V}}-\mathsf{GV}(\mathsf{GST}+\rho ))\delta {}\\&\quad \le \mathsf{GST}+\rho + \sum _{i=0}^{{\mathcal {V}}-1} F(i) + 3{\mathcal {V}}\delta , \end{aligned}$$

as required. $\square$

We now use Theorem 6 to derive closed-form expressions for view ${\mathcal {V}}$ and the latency of reaching it after $\mathsf{GST}$ assuming an exponentially growing timeout function $F(v)=2^v$ for all $v>0$. Below we show that if the protocol starts after $\mathsf{GST}$ ($S_{\mathrm{first}}\ge \mathsf{GST}$), then all correct processes are guaranteed to synchronize in the view ${\mathcal {V}}= \max \{\lceil \lg {}2\delta \rceil , 1\}$, which they enter within $O(\delta \lg {}\delta )$ of the last correct process calling $\mathtt{start}$.

Theorem 7

Consider an execution of with an eventual message delay bound $\delta$, and assume that (1) holds for $u= 2\delta$, $S_{\mathrm{first}}\ge \mathsf{GST}$, and $\forall v>0.\, F(v)=2^v$. Then in this execution FastSync satisfies all the properties in Figs. 2 and 3 for ${\mathcal {V}}=\max \{\lceil \lg {}2\delta \rceil , 1\}$ and $d = 2\delta$. Furthermore, it holds:

$$\begin{aligned} E_{\mathrm{last}}({\mathcal {V}}) \le S_{\mathrm{last}}+ 3\delta \lg {}\delta + 8\delta = S_{\mathrm{last}}+ O(\delta \lg {}\delta ). \end{aligned}$$

Proof

We consider two cases. Suppose first that $F(1) \ge 2\delta$. Then, by Theorem 6, all the properties in Figs. 2 and 3 hold for ${\mathcal {V}}=1$ and $d=2\delta$, and by Property B,

$$\begin{aligned} E_{\mathrm{last}}({\mathcal {V}}) \le S_{\mathrm{last}}+ \delta . \end{aligned}$$

(29)

Since $F(1) \ge 2\delta$, by our choice of the timeout function, $2^{1} \ge 2\delta$. Hence, $\lg {}2\delta \le 1$, and therefore, $\lceil \lg {}2\delta \rceil \in \{0, 1\}$. Thus, we get ${\mathcal {V}}=1=\max \{\lceil \lg {}2\delta \rceil , 1\}$, as needed.

Suppose next that $F(1) < 2\delta$. Then, by Theorem 6, all the properties in Figs. 2 and 3 hold for ${\mathcal {V}}=\min \{v \mid F(v) \ge 2\delta \}$ and $d=2\delta$, and by Property D,

$$\begin{aligned} E_{\mathrm{last}}({\mathcal {V}}) \le S_{\mathrm{last}}+ \sum _{i=1}^{{\mathcal {V}}-1} F(i) + (3{\mathcal {V}}-2)\delta . \end{aligned}$$

(30)

Since $F(1) < 2\delta$, ${\mathcal {V}}> 1$, and therefore,

$$\begin{aligned}&{\mathcal {V}}=\min \{v \mid 2^v \ge 2\delta \wedge v> 1\} {} \\&\quad = \min \{v \mid v \ge \lg {}2\delta \wedge v > 1\}, \end{aligned}$$

which implies

$$\begin{aligned} {\mathcal {V}}= \max \{\lceil \lg {}2\delta \rceil , 1\}, \end{aligned}$$

(31)

as needed.

Finally, plugging (31) into (30) and using the fact that $\lceil \lg {}2\delta \rceil \le \lg {}2\delta + 1$, we get

$$\begin{aligned}&E_{\mathrm{last}}({\mathcal {V}}) \le S_{\mathrm{last}}+ \sum _{i=1}^{\lg {}2\delta } 2^i + (3\lg {}2\delta + 1)\delta {}\nonumber \\&\quad \le S_{\mathrm{last}}+ 3\delta \lg {}\delta + 8\delta = S_{\mathrm{last}}+ O(\delta \lg {}\delta ). \end{aligned}$$

(32)

Thus, from (29) and (32), we get

$$\begin{aligned} E_{\mathrm{last}}({\mathcal {V}}) \le 3\delta \lg {}\delta + 8\delta = S_{\mathrm{last}}+ O(\delta \lg {}\delta ), \end{aligned}$$

as required. $\square$

We now show that if some correct process calls $\mathtt{start}$ before $\mathsf{GST}$ ($S_{\mathrm{first}}< \mathsf{GST}$), then all correct processes are guaranteed to synchronize in the view ${\mathcal {V}}= \max \{\lceil \lg {}2\delta \rceil , \mathsf{GV}(\mathsf{GST}){+\rho }+1\}$, which they enter within $O(\max \{\delta \lg {}\delta , F({\mathcal {V}}-1))$ after $\mathsf{GST}+\rho$.

Theorem 8

Consider an execution of with an eventual message delay bound $\delta$, and assume that (1) holds for $u= 2\delta$, $S_{\mathrm{first}}< \mathsf{GST}$, and $\forall v>0.\, F(v)=2^v$. Then in this execution FastSync satisfies all the properties in Figs. 2 and 3 for ${\mathcal {V}}=\max \{\lceil \lg {}2\delta \rceil , \mathsf{GV}(\mathsf{GST}+\rho )+1\}$ and $d = 2\delta$. Furthermore, it holds:

$$\begin{aligned}&E_{\mathrm{last}}({\mathcal {V}}) \le \mathsf{GST}+ \rho + \max \{3\delta \lg {}\delta , F({\mathcal {V}}-1)\} + 10\delta {}\\&\quad = \mathsf{GST}+ \rho + O(\max \{\delta \lg {}\delta , F({\mathcal {V}}-1)\}). \end{aligned}$$

Proof

We consider two cases. Suppose first that $F(\mathsf{GV}(\mathsf{GST}+\rho )+1) \ge 2\delta$. Then, by Theorem 6, all the properties in Figs. 2 and 3 hold for ${\mathcal {V}}=\mathsf{GV}(\mathsf{GST}+\rho )+1$ and $d=2\delta$, and by Property C,

$$\begin{aligned} E_{\mathrm{last}}({\mathcal {V}}) \le \mathsf{GST}+\rho +F({\mathcal {V}}-1)+3\delta . \end{aligned}$$

(33)

Since $F(\mathsf{GV}(\mathsf{GST}+\rho )+1) \ge 2\delta$, by our choice of the timeout function, $2^{\mathsf{GV}(\mathsf{GST}+\rho )+1} \ge 2\delta$. Hence, $\lg {}2\delta \le \mathsf{GV}(\mathsf{GST}+\rho )+1$, and therefore, $\lceil \lg {}2\delta \rceil \le \mathsf{GV}(\mathsf{GST}+\rho )+1$. Thus, we get ${\mathcal {V}}=\mathsf{GV}(\mathsf{GST}+\rho )+1=\max \{\lceil \lg {}2\delta \rceil , \mathsf{GV}(\mathsf{GST}+\rho )+1\}$, as needed.

Suppose next that $F(\mathsf{GV}(\mathsf{GST}+\rho )+1) < 2\delta$. Then, by Theorem 6, all the properties in Figs. 2 and 3 hold for ${\mathcal {V}}=\min \{v \mid F(v) \ge 2\delta \}$ and $d=2\delta$, and by Property E,

$$\begin{aligned} E_{\mathrm{last}}({\mathcal {V}}) \le \mathsf{GST}+\rho + \sum _{i=0}^{{\mathcal {V}}-1} F(i) + 3{\mathcal {V}}\delta . \end{aligned}$$

(34)

Since $F(\mathsf{GV}(\mathsf{GST}+\rho )+1) < 2\delta$, ${\mathcal {V}}> \mathsf{GV}(\mathsf{GST}+\rho )+1$, and therefore,

$$\begin{aligned}&{\mathcal {V}}=\min \{v \mid 2^v \ge 2\delta \wedge v> \mathsf{GV}(\mathsf{GST}+\rho )+1\} {}\\&\quad = \min \{v \mid v \ge \lg {}2\delta \wedge v > \mathsf{GV}(\mathsf{GST}+\rho )+1\}, \end{aligned}$$

and therefore,

$$\begin{aligned} {\mathcal {V}}= \max \{\lceil \lg {}2\delta \rceil , \mathsf{GV}(\mathsf{GST}+\rho )+1\}, \end{aligned}$$

(35)

as needed.

Finally, plugging (35) into (34) and using the fact that $\lceil \lg {}2\delta \rceil \le \lg {}2\delta + 1$, we get

$$\begin{aligned}&E_{\mathrm{last}}({\mathcal {V}}) \le \mathsf{GST}+\rho + \sum _{i=1}^{\lg {}2\delta } 2^i + 3(\lg {}2\delta + 1)\delta {}\nonumber \\&\quad \le \mathsf{GST}+\rho + 3\delta \lg {}\delta + 10\delta {}\nonumber \\&\quad = \mathsf{GST}+\rho + O(\delta \lg {}\delta ). \end{aligned}$$

(36)

Thus, from (29) and (36), and since $F({\mathcal {V}}-1)$ can be arbitrarily large, we get

$$\begin{aligned}&E_{\mathrm{last}}({\mathcal {V}}) \le \mathsf{GST}+ \rho + \max \{3\delta \lg {}\delta , F({\mathcal {V}}-1)\} + 10\delta {}\\&\quad =\mathsf{GST}+ \rho + O(\max \{\delta \lg {}\delta , F({\mathcal {V}}-1)\}), \end{aligned}$$

as required. $\square$

By Proposition 1, we can apply Theorem 8 if (3) holds for $U = 2\Delta$. Then $F({\mathcal {V}}-1) \le 2\Delta$, which implies the following:

Corollary 23

Suppose that (3) holds for $U = 2\Delta$, and $\forall v>0.\, F(v)=2^v$. Then, every execution of FastSync with the eventual message delay $\delta$ such that $S_{\mathrm{first}}< \mathsf{GST}$ satisfies all the properties in Figs. 2 and 3 for ${\mathcal {V}}=\max \{\lceil \lg {}2\delta \rceil , \mathsf{GV}(\mathsf{GST}+\rho )+1\}$ and $d = 2\delta$, and it holds:

$$\begin{aligned}&E_{\mathrm{last}}({\mathcal {V}}) \le \mathsf{GST}+ \rho + \max \{3\delta \lg {}\delta , 2\Delta \} + 10\delta {}\\&\quad = \mathsf{GST}+ \rho + O(\max \{\delta \lg {}\delta , \Delta \}). \end{aligned}$$