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

Used in practice.For each message that the sender wishes to send,there is an initial exchange of packets between thesender and receiver to establish a commonly-agreed-upon messageidentier.That is, the sender sends a new unique identier (called jd ) to thereceiver, which the receiver then pairs with another new uniqueidentier (called id ).It sends this pair back to the sender, who knows that the newid is recent because it was paired with its current jd .The identier jd isn't needed any longer, but id isused for the actual message communication.The sender then associates this identier id with the message.The receiver uses the associated identier to decide whether or notto accept a received message { it will accept amessage provided the associated identier id is equal to thereceiver's current id .The receiver also sends an acknowledgement.Additional packets are required in order to tell the receiver when itcan throw away a current identier.408VariableTypeInitiallyackedneedidsend, recackedSender's mode.M listJD or nilemptyjd ; used sS JD setid sD or nilcurrent ; msg sM or nilcurrent ; ack sBooleanacked ; buf sD listemptySender's list of messages to send.jd chosen for current message bysender.Includes all jd s ever used by sender.id received from receiver.Message about to be sent to receiver.Ack from receiver.List of id s for which the sender will issue acked message.mode ridleReceiver's mode.emptyReceiver's list of messages to deliver.jd received from sender.id chosen for received jd by receiver.Last id the receiver remembersaccepting.Includes all id s ever issued by receiver.List of id s for which receiver will issuenegative acks.mode sbuf sjd sidleacceptrcvd, ackrecM listJD or nilD or nilD or nilbuf rjd rid rlast rissued rnack ; buf rS D setD listnilnilnilfalseemptynilnilnilemptyemptySender Actions:Input:send msg (m), m 2 Mreceive pktrs (p), p 2 Pcrash sOutput:Ack(b), b a Booleansend pktsr (p), p 2 Precover sInternal:choose jdgrow ; jd ; used s409DescriptionInput:receive pktsr (p), p 2 Pcrash rOutput:receive msg (m), m 2 Msend pktrs (p), p 2 Precover rInternal:grow ; issued rsend msg (m)Eect:if mode s 6= rec thenadd m to buf schoose jdPrecondition:mode s = ackedbuf s nonemptyjd 2= jd ; used sEect:mode s := needidcurrent ; msg s := head (buf s )remove head (buf s )jd s := jdadd jd to jd ; used ssend pktsr (needid jd )receive pktsr (needid jd )receive pktrs (accept jd id )send pktrs (accept jd id )Precondition:mode s = needidjd s = jdEect:noneEect:if mode s = idle thenmode r := acceptchoose an id not in issued rjd r := jdid r := idadd id to issued rEect:if mode s 6= rec thenif mode s = needidand jd s = jd thenmode s := sendid s := idelse if id s 6= id thenadd id to acked ; buf sPrecondition:mode r = acceptjd r = jd ,id r = idEect:none410send pktsr (send m id )receive pktsr (send m id )Precondition:mode s = sendEect:if mode r 6= rec thenif mode r = acceptand id = id r thenmode r := rcvdadd m to buf rlast r := idelse if id 6= last r thenadd id to nack ; buf rcurrent ; msg s = mid s = idEect:nonereceive msg (m)Precondition:mode r = rcvd,m rst on buf rEect:remove head (buf r )if buf r is empty thenmode r := ackreceive pktrs (ack id b)send pktrs (ack id true )send pktsr (acked id nil)receive pktsr (acked id nil)Eect:if mode s 6= rec thenif mode s = send andid = id s thenmode s := ackedcurrent ; ack s := bjd s := nilid s := nilcurrent ; msg s := nilif b = true thenadd id to acked ; buf sPrecondition:mode r = acklast r = idEect:nonesend pktrs (ack id false )Precondition:mode r 6= recid rst on nack ; buf rEect:remove head (nack ; buf r )Precondition:mode s 6= rec,id rst on acked ; buf sEect:remove head (acked ; buf s )Eect:if (mode r = acceptand id = id r ) or(mode r = ackand id = last r ) thenmode r := idlejd r := nilid r := nillast r := nil411Ack(b)Precondition:mode s = ackedbuf s is emptyb = current ; ack sEect:nonecrash scrash rmode s := recrecover smode r := recrecover rgrow ; jd ; used sgrow ; issued rEect:Eect:Precondition:mode r = recEect:mode r := idlejd r := nilid r := nillast r := nilempty buf rempty nack ; buf rPrecondition:mode s = recEect:mode s := ackedjd s := nilid s := nilempty buf scurrent ; msg s := nilcurrent ; ack s := falseempty acked ; buf sPrecondition:noneEect:add some JD s to jd ; used sPrecondition:noneEect:add some Ds to issued rExplain the algorithm from my talk { overview, discuss why it worksinformally,Note the two places where msgs get added to the acked-buer, oncenormally, once in reponse to information about an old message.The trickiest part of this code turns out to be the liveness argument{ how do we know that this algorithm does continue to make progress?There are some places where only single responses are sent, e.g., asingle nack, but that could get lost.However, in this case, the node at the other end is continuing toresend, so eventually another nack will be triggered.4126.852J/18.437J Distributed AlgorithmsLecturer: Nancy LynchJanuary 26, 1993Lecture 28This is the nal lecture!It's on timing-based computing.Recall that we started this course out studying synchronousdistributed algorithms, spent the rest of the time doingasynchronous algorithms.There is an interesting model that is in between these two { really,a class of models.Call these partially synchronous.The idea is that the processes can presume some information abouttime, though the information might not be exact.For example, we might have bounds on process step time, or messagedelivery time.Note that it doesn't change things much just to include upper bounds,because the same set of executions results.In fact, we have been associating upper bounds with events throughoutthe course, when we analyzed time complexity.Rather, we will consider both lower and upper bounds on the time forevents.Now we do get some extra power, in the sense that we are nowrestricting the possible interleavings.C.1 MMT Model DenitionA natural model to use is the one of Merritt, Modugno and Tuttle.Here I'm describing the version that's used in Lynch, Attiya paper.This is the same as I/O automata, but now each class doesn't just get413treated fairlyrather, have a boundmap , which associates lower and upperbounds with each class.The lower bound is any nonnegative real number, while the upper boundis either a positive real or 1.The intuition is that the successive actions in each class aren'tsupposed to occur any sooner (after the class is enabled or afterthe last action in that class) than indicated by the lower bound.Also, no later than the upper bound.Executions are described as sequences of alternating states and(action,time) pairs,Admissibility.I've edited the following from the Lynch, Attiya model paper, Section 2.C.1.1 Timed AutomataIn this subsection, we augment the I/O automaton model to allow discussion of timingproperties.

The treatment here is similar to the one described in AttiyaL89] and is a specialcase of the denitions proposed in MerrittMT90]. A boundmap for an I/O automaton A isa a mapping that associates a closed subinterval of 0 1] with each class in part (A), wherethe lower bound of each interval is not 1 and the upper bound is nonzero. Intuitively,the interval associated with a class C by the boundmap represents the range of possiblelengths of time between successive times when C \gets a chance" to perform an action.

Wesometimes use the notation b` (C ) to denote the lower bound assigned by boundmap b toclass C , and bu(C ) for the corresponding upper bound. A timed automaton is a pair (A b),where A is an I/O automaton and b is a boundmap for A.We require notions of \timed execution", \timed schedule" and \timed behavior" fortimed automata, corresponding to executions, schedules and behaviors for ordinary I/Oautomata. These will all include time information.

We begin by dening the basic type ofsequence that underlies the denition of a timed execution.16In MerrittMT90], the model is dened in a more general manner, to allow boundmaps to yield open orsemi-open intervals as well as closed intervals. This restriction is not crucial in this paper, but allows us toavoid considering extra cases in some of the technical arguments.16414De nition 1 A timed sequence (for an I/O automaton A) is a (nite or innite) sequenceof alternating states and (action,time) pairs,s ( t ) s ( t ) :::011122satisfying the following conditions.1. The states s0, s1, ... are in states (A).2.

The actions 1, 2,... are in acts (A).3. The times t1 , t2,... are successively nondecreasing nonnegative real numbers.4. If the sequence is nite, then it ends in a state si.5. If the sequence is innite then the times are unbounded.For a given timed sequence, we use the convention that t = 0. For any nite timedsequence , we dene tend () to be the time of the last event in , if contains any (action,time) pairs, or 0, if contains no such pairs. Also, we dene send () to be the last statein .

We denote by ord () (the \ordinary" part of ) the sequence0s s :::0112i.e., with time information removed.If i is a nonnegative integer and C 2 part (A), we say that i is an initial index for C in if si 2 enabled (A C ) and either i = 0 or si;1 2 disabled (A C ) or i 2 C . Thus, an initialindex for class C is the index of an event at which C becomes enabled it indicates a pointin from which we will begin measuring upper and lower time bounds.De nition 2 Suppose (A b) is a timed automaton. Then a timed sequence is a timedexecution of (A b) provided that ord() is an execution of A and satises the followingconditions, for each class C 2 part (A) and every initial index i for C in .1.