Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 20
Текст из файла (страница 20)
But rst, we proceedwith an argument for the deadlock-freedom property.Lemma 3 Dijkstra's algorithm is deadlock-free.Proof: We again argue by contradiction. Suppose there is some fair execution thatreaches a point where there is at least one process in T , and no process in C , and suppose97Shared variables:ag : an array indexed by 1..n] of integers from f0,1,2g initially all 0,written by pi and read by allturn : integer from f1,...,ng, initially arbitrary,written and read by allCode for pi**Remainder region**try iL: hag i] 1iwhile hturn 6= ii doif hag turn ] = 0i then hturn iiend ifend whilehag i] 2ij=6 ihag j ] = 2ifordoifend ifend forthen goto Lcrit i**Critical region**exit ihag i] 0irem iFigure 8.6: Dijkstra's algorithm showing atomic actions98t1t2t3Figure 8.7: At time t1, p sets ag i] to 2 at time t2 p nds that ag i] 6= 2 at time t3 p exitsC.ijithat after this point, no process ever enters C .
We begin by removing some complications.Note that all processes in T E continue taking steps in , and hence, if some of the processesare in E , then after one step they will be in R. So, after some point in , all processes arein T R. Moreover, since there are only nitely many processes, after some point no newprocesses enter T , so after some point, no new processes enter T . That is, after some pointin , all the processes are in T R, and no process every changes region.
Write = 12,where in 2, there is a nonempty xed group of processes continuing to take steps forever inT , and no region changes occur. Call these processes contenders.After at most a single step in 2, each contender i ensures that ag i] 1, and it remains 1 for the rest of 2 . So we can assume (without loss of generality) that this is the case forall contenders, throughout 2.Clearly, if turn changes during 2, it is changed to a contender's index. Moreover, wehave the following claim.Claim 4 In 2, eventually turn acquires a contender's index.Proof: Suppose not, i.e., the value of turn remains equal to the index of a non-contenderthroughout 2. Then when any contender pi checks, it nds that turn 6= i and ag turn ] = 0and hence would set turn to i. There must exist an i for which this will happen, because allcontenders are either in the while loop or in the second stage, destined to fail and return tothe while loop (because, by assumption, we know they don't reach C in 2).
Thus, eventuallyin 2, turn gets set to a contender's index.Once turn is set to a contender's index, it remains equal to a contender's index, althoughthe value may change to dierent contenders. Then, any later reads of turn and ag turn ]will yield ag turn ] 1 (since for all contenders i, ag i] 1), and turn will not be changed.Therefore, eventually turn stabilizes to a nal (contender's) index. Let 3 be a sux of 2in which the value of turn is stabilized at some contender's index, say i.Now we claim that in 3, any contender j 6= i eventually ends up in the rst while loop,looping forever. This is because if it is ever in the second stage, then since it doesn't succeedin entering C , it must eventually return to L.
But then it is stuck in stage 1, becauseturn = i 6= j and ag i] 6= 0, throughout 3 . So let 4 be a sux of 3 in which allcontenders other than i loop forever in the rst while loop. Note that this means that allcontenders other than i have their ag variables equal to 1, throughout 4.99We conclude the argument by claiming that in 4, process i has nothing to stand in itsway. This is true because when the while loop is completed, ag i] is set to 2, and no otherprocess has ag = 2, so pi succeeds in its second stage tests and enters C .To complete the proof we remark that the argument for the exit region is straightforward,since no one ever gets blocked there.1006.852J/18.437J Distributed AlgorithmsLecturer: Nancy LynchOctober 8, 1992Lecture 99.1 Dijkstra's Mutual Exclusion Algorithm (cont.)In this section we nish our discussion of Dijkstra's mutual exclusion algorithm with analternative proof of the mutual exclusion property of the algorithm.
Last time we saw anoperational argument. Today we'll sketch an assertional proof, using invariants, just as inthe synchronous case (See Goldman-Lynch LICS-90] for a more detailed proof).9.1.1 An Assertional ProofTo prove mutual exclusion, we must show that: 9(pi pj ) j(i 6= j ) ^ (pi in C) ^ (pj in C)]We would like to prove this proposition by induction on the number of steps in anexecution. But, as usual, the given statement is not strong enough to prove directly byinduction. We need to augment it with other conditions, which may involve all the statecomponents, namely shared variables, local variables, program counters, region designations,and temporary variables.We have to be a little more precise about the use of temporary variables. We dene, foreach process pi , a new local variable Si this variable is used by pi during execution of thefor loop, to keep track of the set of processes that it has already observed to have ag 6= 2.Initially Si = .
When the process nds ag j ] 6= 2 during an iteration of the for loop, itperforms the assignment Si Si fj g. When Si = f1 : : : ng ; fig, the program counterof pi moves to after the for loop. When ag i] is set to 0 or 1, pi assigns Si . Figure 9.1shows where these uses of S would appear in the code for pi. (Note that it becomes moreconvenient to rewrite the for loop as an explicit while loop.)For a given system state, we dene the following sets of processes.before-C: processes whose program counter is right after the nal loop.in-C: processes whose program counter is in region C .101Shared variables:ag : an array indexed by 1::n] of integers from f0,1,2g, initially all 0,written by pi and read by all processesturn : integer from f1,: : : ,ng, initially arbitrary,written and read by all processesCode for pi** Remainder Region **try iL: Si hag i] 1iwhile hturn 6= ii doif hag turn ] = 0i then hturn iiend ifend whilehag i] 2iSi =6 f1 : : : ng ; figchoose j 2 f1 : : : ng ; fig ; Sihag j ] = 2igoto Lwhiledoifend ifthenSi Si fj gend whilecrit i** Critical Region **exit iSi hag i] 0irem iFigure 9.1: Dijkstra's algorithm showing atomic actions and S .i102(The actual entrance to C is a separate step from the last test in the loop.)Put in the above terms, we need to prove that jin-Cj 1.
We actually prove a strongerstatement, namely that jin-Cj + jbefore-Cj 1. This is a consequence of the following twoclaims:1.: 9(pi pj ) j(i 6= j ) ^ (i 2 Sj ) ^ (j 2 Si)]2. pi 2 (before-C in-C) =) Si = f1 : : : ng ; figFirst a small lemma.Lemma 1 If Si 6= then ag i] = 2.Proof: From the denition of Si and the code for the algorithm.Now the main nonexistence claim.Lemma 2 : 9(pi pj ) j (i 6= j ) ^ (i 2 Sj ) ^ (j 2 Si)].Proof: By induction on the length of executions.
The basis case is easy since, in the initialstate, all sets Si are empty. Now consider the case where j gets added to Si (the reader canconvince him/herself that this is actually the only case of interest). This must occur when iis in its nal loop, testing ag j . Since j gets added to Si, it must be the case that ag j ] 6= 2because otherwise, i would exit the loop.
By the contrapositive of Lemma 1 then, Sj = ,and so i 62 Sj .Now the second claim.Lemma 3 pi 2 (before-C in-C ) =) Si = f1 : : : ng ; fig.Proof: By induction on the length of the execution. In the basis case, all processes arein region R, so the claim holds vacuously. For the inductive step, assume the claim holdsin any reachable state and consider the next step. The steps of interest are those where piexits the second loop normally (i.e., doesn't goto L), or enters C . Clearly, if pi exits theloop normally, Si contains all indices except i, since this is the termination condition for theloop (when rewritten explicitly in terms of the S sets).
Upon entry to the critical region, Sidoes not change. Thus the claim holds in the induction step.We can now prove the main result by contradiction.Lemma 4 jin-Cj + jbefore-Cj 1.Proof: Assume, for contradiction, that in some state reachable in an execution jin-C j +jbefore-C j > 1. Then there exist two processes, pi and pj , i 6= j , such that pi 2 (before-C in-C ) and pj 2 (before-C in-C ).
By Lemma 3, Si = f1 : : : ng;fig and Sj = f1 : : : ng ;fj g. But by Lemma 2, either i 62 Sj or j 62 Si , a contradiction.1039.1.2 Running TimeWe would like to bound the time from any state in which there is some process in T and noone in C , until someone enters C .
In the asynchronous setting, however, it is not clear what\time" should mean. For instance, unlike the synchronous case, there is no notion of roundsto count in this model. The way to measure time in this model is as follows. We assumethat each step occurs at some real time point, and that the algorithm begins at time 0.
Weimpose upper bounds on step time for individual processes, denoted by s, and on maximumtime anyone uses the critical region, denoted by c. Using these bounds, we can deduce timeupper bounds for the time required for interesting activity to occur.Theorem 5 In Dijkstra's algorithm, suppose that at a particular time there is some processin T and no process in C .
Then within time O(sn), some process enters C .We remark that the constant involved in the big-O is independent of s, c and n.Proof: We analyze the time along the same lines as we proved deadlock-freedom. Supposethe contrary, and consider an execution in which, at some point, process pi is in T and noprocess is in C , and in which no process enters C for time ksn, for some particular large k.First we claim that the time elapsed from the starting point of the analysis until pi teststurn is at most O(sn). (We will assume that k has been chosen to be considerably largerthan the constant hidden by this big-O.) This is because pi can at worst spend this muchtime before failing in the second stage and returning to L.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
