Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 35

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 35)

Now we claim that this construction works in the concurrent case also.For intuition, re-consider the previous example, now with the gateway. Suppose that wemanage to get the processes to the point where p and q have 3:4 and 3:5, resp., and r has4:1 (see Figure 14.8).Processes p and q can choose 4:2 concurrently. Now let p write, and delay q as before. Ifp and r now leapfrog around the 4 component, they do so around the cycle. But this meansthat they never get back to the position 4:2, and thus, when q eventually writes there, it willbe ordered earlier than the \leapfrogging" processes, and the total order will be preserved.Note that there are now 3 processes in the 4 component, i.e., it is \overfull". But that isn'ttoo harmful, since there are only 2 within the cycle.

If q now picks another label, it will1712r13222qp131133Figure 14.6: initial conguration for counter-example in the concurrent case.observe that component 4 is already full, and will choose 5:1.For general n, we claim that although components can become overfull, (i.e., for a level1 k n ; 1, a component could have more than n ; k processes), the cycle of level k nevercontains more than n ; k processes. For general n, we can prove the invariant that in everycycle at every level, at most two of the three subcomponents are occupied, which implies atotal ordering of the labels. We remark that the precise statements of the invariants are alittle trickier than this (see below).14.2.3 Correctness ProofGawlick, Lynch and Shavit have carried out an invariant proof for the CTS algorithm.

Thefollowing invariants are used.Invariant 1 Let L be any set of n labels obtained by choosing, for each i, exactly one oflabel i and newlabel i . Then L is totally ordered by the label order relation.Note that Invariant 1 says not only that the written labels are totally ordered, but alsothat so are all the pending ones, and any combination of the two kinds. Given this, we candene lmax to be the max label value, and imax to be the largest index of a process having17243125Figure 14.7: structure of one level of the concurrent-case domain.r1243pq5Figure 14.8: initial conguration for concurrent case.label lmax .Invariant 2 If i = imax then newlabel i = label i.Invariant 2 says that any pending label from the known max is the same as its old label(it would never have had any reason to increase its label if it's the max).The following invariant describes a property that any pending label that's greater thanthe current known max must satisfy.

Dene the nextlabel function to yield the very nextvalue at the indicated level.Invariant 3 If lmax < newlabel i then newlabel i = nextlabel (lmax k) for some k, 1 k n ; 1.The previous three invariants, 1, 2, and 3, are sucient to complete the proof. Theothers are just used to make the induction go through. However, in order to prove thesethree invariants by induction, we require three additional technical invariants. Thus, for alllevels k, 1 k n ; 1, we have the following three technical claims.

First, we have oneabout \old" pending labels it constrains how dierent these pending labels can be from thecorresponding actual labels.173Invariant 4 If newlabel i lmax and label i is in the same level k component as lmax, thenso is newlabel i .The next invariant describes some more constraints on the newlabel values, based on thecorresponding actual labels. This time, the constraint refers to newlabel values in the cycleof a component containing the max label.Invariant 5 If newlabel i is in the cycle of the level k component containing lmax , then label iis in that level k component.And nally, we have an invariant saying that it is sometimes possible to deduce that thecomponent containing the max label contains lots of processes.Invariant 61. If newlabel i = nextlabel (lmax k) then there are at least n ; k processes excluding iwhose label values are in the same k ; 1 component as lmax .2. If lmax is not in level k component numbered 1, then there are at least n ; k + 1processes whose label values are in the same k ; 1 component as lmax.This invariants are proved by induction, as usual.

We remark that the proofs are notshort { they are fairly long, detailed case analyses.The upshot of the invariants is that we have the total ordering property preserved, butthis doesn't exactly show that we have behavior inclusion.Recall that we need to show that all well-formed behaviors of the bounded object are alsowell-formed behaviors of the unbounded object. The right way to show this is to give a formalcorrespondence between the two objects. Recall the case of the stopping-failure synchronousconsensus algorithm, where we showed a formal correspondence between an inecient butunderstandable algorithm and an optimized version. We did this using invariants relatingthe states of the two algorithms when they run using the same inputs and failure pattern.We are going to do essentially the same thing here.

Now, however, we don't have anyconvenient notion analogous to the \(inputs, failure-pattern)" pair to determine the courseof the execution. We are in a setting in which there is much more nondeterminism, both inthe order in which various actions occur, and in what state changes happen when a particularaction happens (consider the choice of the new label in the unbounded object). But notethat now, we don't have to show an equivalence, saying that everything that either algorithmdoes the other does also.

Rather, we only need a one-directional relationship, showing thateverything that the bounded algorithm does, the unbounded can also do (this is exactlyinclusion of external behaviors).We shall use the notion of forward simulation relation dened in a Lecture 13 applying itto get a simulation from B , the bounded object, to U , the unbounded object. Incidentally, in174this case we don't need to use the well-formedness restriction | the correspondence betweenthe objects also holds in the non-well-formed case (although it is not so interesting in thatcase).

We remark that if we only wanted to consider inclusion in the restricted case, say forsome other implementation that didn't work in the case of non-well-formed executions, wecould just enlarge the system by explicit composition with a \most general" well-formedpreserving environment and prove inclusion for the resulting composed systems.It turns out that the forward simulation mapping f is quite simple.

(Note the similarityin style to the earlier proof for synchronous consensus, with invariants about the pair ofstates.) We dene u 2 f (s) provided that the following hold for all i, j , where i 6= j :1. s:pci = u:pci2.s:label i s:label js:label i s:newlabel js:newlabel i s:label js:newlabel i s:newlabel j()()()()u:label i < u:label ju:label i < u:newlabel ju:newlabel i < u:label ju:newlabel i < u:newlabel j3.

s:order i = u:order i4. s:value i = u:value i5. s:snapvalue i = u:snapvalue iIn other words, everything is exactly the same except for the two kinds of label values,and in these cases, the ordering relationship is the same. Now we need to show that thiscorrespondence is preserved. Formally, we have to show the conditions of the denition ofa simulation relation. To help us, we use Invariants 1, 2, and 3. The interesting step isthe snap step embedded in a label operation, since it is the one that has the potential toviolate the nice ordering relationships by choosing newlabel. So consider a snap i step withina label operation.

If i detects itself to be the max (based on the label values that it readsin the snapshot), it doesn't make any changes in either algorithm, so the correspondence ispreserved. So suppose that it doesn't detect itself to be the max (which is same in both).So a particular label is chosen in B . We must dene some corresponding label in U , whichshould satisfy the same ordering conditions. We know that this new label will be strictlygreater than all the label s in B , so we might be tempted to just choose one plus the max ofthose, for use in U . But we have to also preserve the relative order of this newlabel and allthe other newlabel s.

There are scenarios in which this new one might not be greater than175all the others, in fact, it possibly could be strictly less than some. But Invariant 2 impliesthat we don't have to worry about the newlabel s that are not greater than the maximumlabel in B , and Invariant 3 characterizes the form of the newlabel 's that are greater thanthe maximum label in B . Now it is easy to see how the new label now being chosen ts inrelative to these, and we can choose a new label in U in the same way.14.2.4 Application to Lamport's Bakery AlgorithmWe can use a CTS algorithm to provide a bounded-register variant of the Lamport's bakeryalgorithm.

Характеристики

Список файлов книги