Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 43
Текст из файла (страница 43)
However, the concurrent writer is choosingconcurrently, and the algorithm didn't need any particular relation between valueschosen concurrently. In L3, suppose someone reads a number while it's being written. If the test succeeds,the writer is back at the point of choosing its value, and everything is ne. (That is,it must be that the reader at L2 saw the writer before it begin choosing its number,so the writer is guaranteed to choose a larger number.) The problem is if the writer'svalue comes back as very small, which can delay the reader. However, it cannot delaythe reader forever.17.3 Asynchronous Network AlgorithmsNow we make another major switch in the model we consider. Namely, we switch from asynchronous shared memory to asynchronous networks.
As in synchronous networks, we assumea graph (or a digraph) G, with processes at the nodes, and communication over (directed)edges. But now, instead of synchronous rounds of communication, we have asynchrony inthe communication as well as the process steps.We model each process as an IOA, generally with some inputs and outputs connecting itwith the outside world. (This is the boundary where the problems will usually be stated.) Inaddition, process i has outputs of the form send i j (m), where j is an outgoing neighbor, andm is a message (element of some message alphabet M ), and inputs of the form receive j i(m),for j an incoming neighbor.
Except for these interface restrictions, the process can be anarbitrary IOA. (We sometimes restrict the number of classes, or the number of states, etc.,215to obtain complexity results).To model communication, we give a behavior specication for the allowable sequences ofsend (i j ) and receive (i j ) actions, for each edge (i j ). This can be done in two ways: by alist of properties or axioms, or by giving an IOA whose fair behaviors are exactly the desiredsequences. The advantage of giving an explicit IOA is that in this case, the entire systemis described simply as a composition, and we have information about the state of the entiresystem to use in invariants and simulation proofs.
But sometimes it's necessary to do someunnatural programming to specify the desired behavior as an IOA , especially when we wantto describe liveness constraints. Let us now make a short digression to dene the importantnotions of safety and liveness.Let S and L be properties (i.e., sets) of sequences over a given action alphabet. S is asafety property if the following conditions hold.1.
S is nonempty (i.e., there is some sequence that satises S ),2. S is prex-closed (i.e., if a sequence satises S , then all its prexes satisfy S ), and3. S is limit-closed (i.e., if every nite prex of an innite sequence satises S , then theinnite sequence satises S ).L is a liveness property if for every nite sequence, there is some extension that satisesL. Informally, safety properties are appropriate for expressing the idea that \nothing badever happens" | if nothing bad has happened in a nite sequence, then nothing bad hashappened in any prex either moreover, if something bad happens, it happens at a nitepoint in time.
Liveness, on the other hand, is most often used to express the idea that\something good eventually happens".We now return to the asynchronous message passing model. The most common communication channel studied in the research literature is a reliable FIFO channel. Formally, thisis an IOA with the appropriate interface, whose state is a queue of messages. The send (i j )action puts its argument at the end of the queue. The receive i j (m) action is enabled if m isat the head of the queue, and its eect is to remove the message from the queue. Of course,it also delivers the message to the recipient process (which should handle it somehow).
Butthat is a part of the process' job, not of the channel's. The right division of responsibilitiesis obtained by the IOA composition denition. The fairness partition here can put all thelocally controlled actions in a single class.To gain some experience with asynchronous network algorithms (within this model), wego back to the beginning of the course and reconsider some of the examples we previouslyconsidered in synchronous networks.21617.3.1 Leader ElectionRecall the algorithms we considered earlier. First, the graph is a ring, with UIDs built intothe initial states of the processors as before. In the action signature there are no inputs fromthe outside world, and the only output actions are leader i, one for each process i.LeLann-Chang AlgorithmIn this algorithm, each process sends its ID around the (unidirectional) ring.
When a nodereceives an incoming identier, it compares that identier to its own if the incoming identieris greater than its own, it keeps passing the identier if it is less than its own, then theidentier is discarded and if it is equal, it outputs the leader action. This idea still worksin an asynchronous system: Figure 17.9 gives the code for the algorithm.Essentially, the behavior of the algorithm is the same as in the synchronous, but \skewed"in time. We might prove it correct by relating it to the synchronous algorithm, but therelationship would not be a forward simulation, since things happen here in dierent orders.We need a more complex correspondence. Instead of pursuing that idea, we'll discuss a morecommon style of verifying such algorithms, namely, direct use of invariants and induction.Invariant proofs for asynchronous systems work ne.
The induction is now on individualprocesses steps, whereas the induction in the synchronous model was on global system steps.Here, as in the synchronous case, we must show two things:1. that no one except the maximum ever outputs leader , and2. that a leader output eventually occurs.Note that (1) is a safety property (asserting the fact that no violation ever occurs), and (2)is a liveness property.Safety properties can be proved using invariants. Here, we use a similar invariant to theone we stated for the synchronous case:Invariant 7 If i 6= imax and j 2 imax i) then own (i) 2= send (j ).We want to prove this invariant by induction again, similar to the synchronous case.(Recall a homework problem about this.) But now, due to the introduction of the messagechannels with their own states, we need to add another property to make the induction gothrough:Invariant 8 If i 6= imax and j 2 imax i) then own (i) 2= queue (j j + 1).With these two statements together, the induction works much as before.
More specifically, we proceed by case analysis based on one process at a time performing an action.217The key step, as before, is where i gets pruned out by process imax . This proves the safetyproperty.We now turn to the liveness property, namely that a leader i action eventually occurs.For this property, things are quite dierent from the synchronous case. Recall that in thesynchronous case, we used a very strong invariant, which characterized exactly where themaximum value had reached after k rounds. Now there is no notion of round, so the proofmust be dierent.
We can't give such a precise characterization of what happens in thecomputation, since there is now so much more uncertainty. So we need to use a dierentmethod, based on making progress toward a goal. Here, we show inductively on k, for0 k n ; 1, that eventually, imax winds up in send imax +k . We then apply this to n ; 1,and show that imax eventually gets put into the (imax ; 1 imax ) channel, and then that imaxmessage eventually is received at imax , and therefore eventually leader imax action gets done.All these \eventually" arguments depend on using the IOA fairness denition.For example, suppose that there is a state s appearing in some fair execution , wherea message m appears at the head of a send queue in s. We want to show that eventuallysend (m) must occur.
Suppose not. By examination of the allowable transitions, we concludethat m remains at the head of the send queue forever. This means that the send class staysenabled forever. By the IOA fairness, some send must eventually occur. But m is the onlyone at the head of the queue, so the only one for which an action can be enabled, so send (m)must eventually occur.Likewise, if m appears in the kth position in the send queue, we can prove that eventuallysend (m) occurs. This is proven by induction on k , with the base case above. The inductivestep says that something in position k eventually gets to position k ; 1, and this is based onthe head eventually getting removed.We remark that this type of argument can be formalized within temporal logic, usingstatements of the form P ) 3Q (see Manna and Pnueli).218State of process i: own : type UID, initially i's UID send : type queue of UID's, initially containing only i's UID status : takes values from funknown chosen reported g, initially unknown.Actions of process i:send i i+1 (m)Precondition: m is rst on sendEect: Remove rst element of sendreceive i;1 i (m)Eect: casem > own : add m to end of sendm = own : status chosenotherwise: do nothingendcaseleader iPrecondition: status = chosenEect: status reportedFairness partition classes: For any process, all send actions are in one class, and theleader action in another (singleton) class.Figure 17.9: LeLann-Chang algorithm for leader election in asynchronous rings2196.852J/18.437J Distributed AlgorithmsLecturer: Nancy LynchNovember 12, 1992Lecture 1818.1 Leader Election in Asynchronous Rings (cont.)18.1.1 The LeLann-Chang Algorithm (cont.)We conclude our discussion of this algorithm with time analysis.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
