1
38
E. Borowsky et al.
ꢀ
Define a run of process j of P to be a sequence of the
{sim-mem-local(j)i : sim-steps(j)i = k and status(j)i
∈ {unsafe, safe}}.
form ρ = s0, c1, s1, c2, s2, . . . , sk,where each si is a state
of process j,and each ci is a “change”,that is,one of the
following: (“init”, v), (“snap”, w), (“update”, r), “local”,
“decide”, v); the first state is the unique start state,and each
change yields a transition from the preceding to the succeeding
state.
Proof. Let s be any reachable state of Q composed with ab-
stract safe agreement modules and a user U. For s equal to the
initial state it is simple to check that the lemma holds. Assume
it holds for some state s,and we prove that it holds for any state
(
ꢀ
ꢀ
s ,after a step (s, π, s ). Let ρ = s0, c1, s1, . . . , sk be a run of
A consequence of the next lemma is that every process
i that simulates steps of a process j simulates the same run
of j. As we shall see,the run is determined by the i process
that is furthest ahead in the simulation of j; thus,only such
an i process can affect the outcome of the next step of j.
Moreover,it can affect only the outcome of snapshot steps.
Once the outcome of a snapshot step is determined, i can
proceed with the simulation of j locally (without reading the
shared variable),up to the next snapshot step.
Invariant 1 relates the information in the processes of Q
and the safe agreement modules. Invariants 2 and 3 relate the
processes of Q and a given run ρ of process j. Invariants 4
and 5 relate ρ and the safe agreement modules. Invariant 6
relates all three types of information: it relates information in
certain processes of Q,the run ρ (those that are “current” in
their simulation of j,according to ρ) and the safe agreement
modules.
process j,corresponding to s,whose existence is guaranteed
ꢀ
ꢀ
by the lemma. We prove there is a run ρ corresponding to s ,
ꢀ
that satisfies the requirements of the lemma. The run ρ will
be either equal to ρ,or else obtained from ρ by appending a
change ck+1 and a state sk+1. We skip the proof of invariant 1,
which is simple and does not talk about ρ.
ꢀ
For state s, k = maxi{s.sim-steps(j)i}. Let k be the cor-
ꢀ
ꢀ
ꢀ
responding value in s ; i.e. k = maxi{s .sim-steps(j)i}.
ꢀ
First assume k = k + 1. Then,for some i, π must be one
+
of: agree(w)j,0,i, agree(w)j,ꢁ,i for % ∈ N , sim-update ,
j,i
sim-localj,i,or sim-decidej,i,since these are the only cases
that increment a sim-steps component. Moreover,we have
s.sim-steps(j)i = k,and hence,by part 3(a) of the lemma,
ꢀ
sk = s.sim-state(j)i. For each one of these possibilities, ρ
is obtained from ρ by appending the corresponding change:
(
“init”, w) for an agree(w)j,0,i; (“snap”, w) for an agree
+
(
w)j,ꢁ,i, % ∈ N ; (“update”, r) for a sim-update ; “local”
j,i
for a sim-localj,i; (“decide”, v) for a sim-decidej,i,and after
the change,appending to the run the state sk+1,resulting from
the corresponding transition function (trans-init, trans-snap,
or trans) applied to sk. That is, sk+1 = s .sim-state(j)i. Thus,
in s ,process i is the first one to finish the simulation of the
Lemma 3. For every reachable state of Q composed with ab-
stract safe agreement modules and a user U, and for each
process j, there is a run ρ = s0, c1, s1, . . . , sk of process j
such that:
ꢀ
ꢀ
ꢀ
ꢀ
ꢀ
1
. For any i:
(
(
k -th step of j and s .sim-steps(j)i = k ; while for every other
ꢀ
ꢀ
ꢀ
a) sim-steps(j)i ≥ 1 if and only if i ∈ agreed-procsj,0.
process i , s .sim-steps(j)iꢀ < k .
ꢀ
First notice that part 2 of the lemma clearly holds for s .
b) For any % ≥ 1, sim-snaps(j)i ≥ % if and only if i ∈
+
Consider the case of π = agree(w)j,ꢁ,i for % ∈ N (we
agreed-procs
.
j,ꢁ
omit the proofs of the other cases,which are analogous). For
part 3 of the lemma,we need to consider only the case of
(
c) i ∈ proposed-procs − agreed-procs if and only
j,0
j,0
if nextop(sim-state(j)i) = “init” and status(j)i ∈
%
= k + 1,since the cases of % < k + 1 hold by the in-
{
unsafe, safe}.
duction hypothesis. Thus,we need to consider only process i.
Part (a) holds by the definition of sk+1. Part (b) holds because
s.sim-snaps(j)i is the number of snap’s among c1, . . . , ck,
(
d) Forany% ≥ 1, i ∈ proposed-procs −agreed-procs
j,ꢁ
j,ꢁ
if and only if nextop(sim-state(j)i) = “snap”, sim-
snaps(j)i = % − 1, and status(j)i ∈ {unsafe, safe}.
ꢀ
and s .sim-snaps(j)i = s.sim-snaps(j)i + 1,while ck+1 =
2
3
. k = maxi{sim-steps(j)i}.
(
“snap”, w). Part (c),(d),and part 4(a) of the lemma hold by
. For any i, if sim-steps(j)i = % then:
induction hypothesis. For part 4(b) of the lemma,notice that
(
(
a) sim-state(j)i = sꢁ.
ꢀ
there are %−1 snap’s in ρ. Thus,in ρ there are % snap’s,and in-
b) sim-snaps(j)i is the number of “snap”’s among c1,
deed agreed-val = w. Part 5 holds trivially because process
j,ꢁ
.
. . , cꢁ.
iisthefirstonetofinishthesimulationofthe %-thsnapofj,and
(
c) mem(i).sim-mem(j) is the value written in the last
update” among c1, . . . , cꢁ, if any, else r0.
d) mem(i).sim-steps(j) is the number of the last
update” among c1, . . . , cꢁ, if any, else 0.
. (a) (“init”, v) appears in ρ if and only if agreed-valj,0 = v.
ꢀ
ꢀ
henceproposed-valsj,ꢁ
ꢀ
ꢂ
ꢀ
ꢂ
j,ꢁ
“
while proposed-valsj,ꢁ
ꢀ
= ∅ and agreed-val
ꢀ
j,ꢁ
=⊥ for % > %.
(
Finally,consider part 6. Since in s there are no processes i
with sim-steps(j)iꢀ = k + 1 and status(j)iꢀ ∈ {unsafe, safe},
“
4
5
then we have to prove proposed-vals
= ∅. Observe that
(
b) (“snap”, w) is the %’th snapshot in ρ if and only if
s.sim-snaps(j)iꢀ = % − 1 for any i with s.sim-steps(j)iꢀ = k.
agreed-valj,ꢁ = w.
Then, s.sim-snaps(j)iꢀ < % for all i ,and hence no i has yet
executed a propose(w)j,ꢁ+1.
. If proposed-valsj,ꢁ
ꢂ= ∅ and agreed-val =⊥ for some %
j,ꢁ
then
ꢀ
Now assume k = k. In this case, ρ = ρ. Clearly part 2
(
a) If % = 0 then ρ consists of only one state s, and
nextop(s) = “init”.
b) If % ≥ 1, then nextop(sk) = “snap”, and the number
of the lemma holds. The cases of π equal to agree(w)j,0,i,
agree(w)j,ꢁ,i, %
∈
N , sim-update , sim-localj,i,or
(
sim-decidej,i,are similar to each other. Let us consider the
most interesting: π = agree(w)j,ꢁ,i. We have that s.sim-
of snaps in ρ is % − 1.
6
. For any % ≥ 1, if nextop(sk) = “snap” and the num-
snaps(j)i = % − 1 and s .sim-snaps(j)i = %. Assume s.sim-
ber of “snaps” in ρ is % − 1, then proposed-vals
=
steps(j)i = k1, k1 < k. To prove part 3 take % = k1 + 1.
j,ꢁ