Consensus in the Presence of Partial Synchrony 309 TICK(b): forj=l,...,Ndo send (Q + l)-tick to pj; CLAIM(b). FIG. 2. The TICK and CLAIM procedures. CLAIM(b): forj= l,...,Ndo send (b + I)-claim to pi; if c, > b then TICK(G) else CLAIM(b). The following lemmas describe limitations on the rates of the master clock and the local clocks. The first three lemmas do not involve A and +‘, and so apply to either partially synchronous model (delta and phi holding eventually or delta and phi unknown). LEMMA 5.1. For all s L 0 andfor all i such that pi is correct, Ci(S) s C(s). PROOF. The proof is by induction on s. The basis s = 0 is obvious since Ci(0) = C(0) = 0 by definition. Fix some s and some correct pi, and assume that the statement of the lemma is true for all s’ < s and all correct pk. Let j = Ci(S). By the definition of the private clock, there are two possibilities: (1) pi has received j+-claims from 2t + 1 different processors. Since at least t + 1 of these j’-claims are from correct processors, C(s) 2 j by definition of the master clock. (2) pi has received messages from t + 1 different processors, each of which is either (j + I)+-tick or a (j + I)+-claim. Consider the earliest real time, s’, when some correct processor, say pk, sends a (j + I)+-tick. Note that s’ < s, so ck(s’) 5 C(s’) by the inductive hypothesis. By definition of the protocol, c&‘) 2 j. Therefore, j 5 f&(d) 5 c(s’) 5 c(s). 0 LEMMA 5.2. For all s 2 0, the largest tick sent by a correct processor at real time s has size at most C(s) + 1. PROOF. This proof is immediate from the protocol and Lemma 5.1. Cl LEMMA 5.3. For all s, x 2 0, C(s + x) I C(s) + x. PROOF. The proof is by induction on x. For the basis, let x = 1. By Lemma 5.2 the largest tick sent by a correct processor by time s has size at most C(s) + 1, so the maximum tick that can be broadcast by t + 1 processors by time s + 1 is a (C(s) + I)-tick. Thus, C(s + 1) 5 C(s) + 1. Assume the lemma holds for some x. Then C(s + (x + 1)) = C((s + 1) + x) I C(s + 1) + x (by the induction hypothesis) sC(s)+(x+ 1) (by the basis). 0 The preceding lemmas are independent of both communication and processor synchrony. Now we give several lemmas that assume such synchrony. We would like to state the lemmas in a way that applies to both kinds of partially synchronous models (delta and phi holding eventually and delta and phi unknown). So fix A and + (for either case). Also fix GST for the model in which A and cf, hold