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

However, at a later pointin the course (when we consider \wait-free objects" and other fault-tolerance issues), we willwant to prove things about executions that are not necessarily fair.8.2 Mutual Exclusion ProblemThe problem of Mutual Exclusion involves allocating a single indivisible resource among nprocesses p1 : : : pn. Having the access to the resource is modeled by the process reachinga critical region, which is simply a designated subset of its states. Normally, that is, whenit doesn't want access to the resource, the process is said to be in the remainder region.In order to gain access to the critical region, a process executes a trying protocol, while for91symmetry, after the process is done with the resource, it executes an (often trivial) exitprotocol. This procedure can be repeated, and the behavior of each process is thus cyclic,moving from the remainder region (R) to the trying region (T), then to the critical region(C), and nally to the exit region (E).

The cycle of regions that a process visits is shown inFigure 8.2. In the diagram, self-loops indicate that a process can remain in these regionsafter it performs a step. In contrast, we will abstract away steps done within the critical andremainder regions, and not consider them here.RETCFigure 8.2: the cycle of regions of a single processWe will consider here only algorithms in which communication among processes is donethrough shared memory. For starters, we will suppose that the memory is read-write only,that is, in one step, a process can either read or write a single word of shared memory.

Tomatch this up with the shared memory model discussed above, we have n process automataaccessing read-write shared memory. The two basic actions involving process pi and a sharedvariable x are:pi reads x and uses the value read to modify the state of pi, andpi writes a value determined from pi 's state to x.The inputs to processes are try i actions, modeling the rest of the program requestingaccess to the resource, and exit i, modeling the rest of the program announcing it is donewith the resource. The output actions are crit i, which is interpreted as granting the resource,and rem i, which tells the rest of the program that it can continue. The processes inside thediagram, then, are responsible for performing the trying and exit protocols.It is sometimes useful to view the outside world as consisting of n users, which we modelas other state machines that communicate with their respective processes via the designatedactions.

These users are assumed to execute some application programs. In between thecrit i and exit i action, user i is free to use the resource (see Figure 8.3).We will assume that each user obeys the cyclic behavior, that is, that each user is notthe rst to violate the cyclic order of actions between itself and its process.92try icrit iUser iexit irem iFigure 8.3: interface specication for the userA global picture of the system architecture appears in Figure 8.4.Within this setting, the protocol is itself supposed to preserve the cyclic behavior, andmoreover, to satisfy the following basic properties.Mutual exclusion: There is no reachable state in which more than one process is in regionC.Deadlock-Freedom: If at any point in a fair execution, at least one process is in the tryingregion and no process is in the critical region, then at some later point some processenters the critical region.

Similarly, if at any point in a fair execution, at least oneprocess is in the exit region (with no other condition here), then at some later pointsome process enters the critical region.Note that deadlock-freedom presupposes fairness to all the processes, whereas we don'tneed to assume this for the other conditions. In the ensuing discussions of mutual exclusion,we might sometimes neglect to specify that an execution is fair, but it should be clear thatwe assume it throughout | until otherwise specied (namely, when we consider faults).Note that responsibility for the entire system continuing to make progress depends notonly on the protocol, but on the users as well. If a user gets the resource but never returns it(via an exit i), then the entire system will grind to a halt.

But if the user returns the resourceevery time, then the deadlock-freedom condition implies that the system continues to makeprogress (unless everyone remains in its remainder region).Note that the deadlock-freedom property does not imply that any particular process eversucceeds in reaching its critical region. Rather, it is a global notion of progress, saying thatsome process reaches the critical region.

For instance, the following scenario does not violatethe deadlock-freedom condition: p1 enters T , while p2 cycles repeatedly through the regions(the rest of the processes are in R). The deadlock-freedom condition does not guaranteethat p1 will ever enter C .93EXTERNALENVIRONMENTSYSTEMProcessesVariablesP1try iUser icrit iPiexit irem iPnFigure 8.4: Architecture for the mutual exclusion problemThere is one other constraint: a process can have a locally controlled action enabled onlywhen it is in T E . This implies that the processes can actively execute the protocol onlywhen there are active requests.

The motivation for this constraint is as follows. In the originalsetting where this problem was studied, the processes did not have dedicated processors: theywere logically independent processes executed on a single time-shared processor. In thissetting, having special processes managing the mutual exclusion algorithm would involveextra context-switching, i.e., between the manager process and the active processes.

In atrue multiprocessor environment, it is possible to avoid the context-switching by using adedicated processor to manage each resource however, such processors would be constantlymonitoring the shared memory, causing memory contention. Moreover, a processor dedicatedto managing a particular resource is unavailable for participation in other computationaltasks.948.3 Dijkstra's Mutual Exclusion AlgorithmThe rst mutual exclusion algorithm for this setting was developed in 1965 by Edsger Dijkstra.

It was based on a prior two-process solution by Dekker. Until then, it was not evenclear if the problem is solvable.We begin by looking at the code, though it will not be completely clear at rst how thiscode maps to the state-machine model. The code is given in Figure 8.3.The shared variables are ag i] 1 i n, one per process, each taking on values fromf0 1 2g, initially 0, and turn , an integer in f1 : : :ng. Each ag i] is a single-writer multireader variable, writable only by process i but readable by everyone. The turn variable ismulti-writer multi-reader, both writable and readable by everyone.We translate the code to our model as follows. The state of each process consists of thevalues of its local variables, as usual, plus some other information that is not representedexplicitly in the code, including:Temporary variables needed to remember values of variables read.A program counter, to say where in the code the process is up to.Temporary variables introduced by the ow of control of the program (e.g., the forloop introduces a set to keep track of the indices already processed).A region designation, T , C , E or R.The state of the entire system consists of process states plus values for all the sharedvariables.The initial state of the system consists of initial values for all local and shared variables,and program counters in the remainder region.

(Temporary variables can be undened.) Theactions are try i crit i exit i rem i, local computation steps, and the read-write accesses to theshared variables. The steps just follow the code in the natural way. The code describes thechanges to the local and shared variables explicitly, but the implicit variables also need tobe changed by the steps. For example, when a try i action occurs, the region designation fori becomes T .

The program counter changes as it should, e.g., when try i occurs, it becomesa pointer to the beginning of the trying region code.This code is adapted from Dijkstra's paper. Note that the code does not specify explicitlyexactly which portions of the code comprise indivisible steps. However, since the processesare asynchronous, it is important to do this. For this algorithm, atomic actions are thetry i , etc., plus the single reads from and writes to the shared variables, plus some localcomputation steps. The code is rewritten in Figure 8.6 to make the indivisible steps more95Shared variables:ag : an array indexed by 1::n] of integers from f0,1,2g, initially all 0,written by pi and read by all processes.turn : integer from f1,: : : ,ng, initially arbitrary,written and read by all processes.Code for pi :** Remainder Region **try i** begin rst stage, trying to obtain turn **L: ag i] 1while turn 6= i doif ag turn ] = 0 then turn iend ifend while** begin second stage, checking that no other processor has reached this stage **ag i] 2for j 6= i do ** Note: order of checks unimportant **if ag j ] = 2 then goto Lend ifend forcrit i** Critical Region **exit iag i] 0rem iFigure 8.5: Dijkstra's mutual exclusion algorithm96explicit.

The atomic actions are enclosed in pointy brackets. Note that the read of ag turn ]does not take two atomic actions because turn was just read in the line above, and so a localcopy of turn can be used. The atomicity of local computation steps is not specied | infact, it is unimportant, so any reasonable interpretation can be used.8.3.1 A Correctness ArgumentIn this section we sketch a correctness argument for Dijkstra's algorithm. Recall that forthe synchronous model, the nicest proofs resulted from invariants describing the state ofthe system after some number of rounds. In the asynchronous setting, there is no notion ofround, so it may not be readily clear how to use assertional methods. It turns out that theycan still be used, and indeed are extremely useful, but typically it is a little harder to obtainthe invariants.

The arguments must be applied at a ner level of granularity, to make claimsabout the system state after any number of individual process steps (rather than rounds).Before presenting an assertional proof, however, we will sketch a \traditional" operationalargument, i.e., an argument based directly on the executions of the algorithm.In the following series of lemmas we show that the algorithm satises the requirements.The rst lemma is very each to verify.Lemma 1 Dijkstra's algorithm preserves cyclic region behavior for each i.The second lemma is more interesting.Lemma 2 Dijkstra's algorithm satises mutual exclusion.Proof: By contradiction.

Assume pi and pj are both simultaneously in region C , in somereachable state, where i 6= j . Consider an execution that leads to this state. By the code,both pi and pj set their ag variables to 2 before entering their critical regions. Considerthe last such step in which each sets its ag variable. Assume, without loss of generality,that ag i] is set to 2 rst.

Then, ag i] remains 2 from that point until pi leaves C , whichmust be after pj enters C , by the assumption that they both end up in C simultaneously.So, ag i] has the value 2 throughout the time from when pj sets ag j ] to 2 until pj entersC (see Figure 8.7).But during this time, pj does a nal test of ag i] and nds it unequal to 2, a contradiction.We will redo this argument using an invariant assertion proof later.