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

= receive pkt tr (m b)Since is enabled in s, (m b) appears in C sr in s.Since u 2 g(s), (m i) appears in the corresponding position inC sr in u,for some integer i with b = i mod 2.Let $ = receive pkt tr(m i) then $ is enabled in u.Let u0 be the state such that (u $ u0) is a step of389FIFO-Stenning, and such that the same number of packets is removedfrom the queue.We must show that u0 2 f (s0).It is easy to see that the third condition is preserved,since each of and$ removes the same number of packets from C sr.Suppose rst that b = s:ag r .Then the eects of imply that the receiver state in s0 is identicalto that in s.Now, since u 2 f (s), s:ag r = u:integer r mod 2since b = i mod 2, this case must havei 6= u:integer r + 1.Then the eects of $ imply that the receiver state in u0 isidentical to that in u.It is immediate that the rst and second conditions hold.So now suppose that b 6= s:ag r .The invariant above for FIFO-Stenning implies that either i = u:integer ror i = u:integer r + 1.Since b = i mod 2 and(since u 2 f (s)) s:ag r = u:integer r mod 2,this case must have i = u:integer r + 1.Then by the eect of the action, u0:integer r = u:integer r + 1and s0:ag r = 1 ; s:ag r ,preserving the second condition.Also, buer r is modied in both cases by adding the entry mat the end therefore, the rst condition is preserved.5.

= send pkt rt(b)Similar to send pkt tr (m b).6. = receive pkt rt(b)Since is enabled in s, b is in C rs in s.Since u 2 f (s), i is the corresponding position in C rs in u,for some integer i with b = i mod 2.390Let $ = receive pkt rt(i) then $ is enabled in u.Let u0 be the state such that (u $ u0) is a step ofFIFO-Stenning, and such that the same number of packets are removed.We must show that u0 2 f (s0).It is easy to see that the third condition is preserved,since each of and$ removes the same number of messages from C rs.Suppose rst that b 6= s:ag s.Then the eects of imply that the sender state in s0is identical to that in s.Now, since u 2 f (s), s:ag s = u:integer s mod 2since b = i mod 2, this case must havei 6= u:integer s.Then the eects of $ imply that the sender state in u0 isidentical to that in u.It is immediate that the rst and second conditions hold for this situation.So now suppose that b = s:ag s.The invariant above for FIFO-Stenning implies that either i = u:integer s ; 1or i = u:integer s.Since b = i mod 2 and(since u 2 f (s)) s:ag s = u:integer s mod 2,this case must have i = u:integer s.Then the eect of the action implies thatu0:integer s = u:integer s + 1and s0:ag s = 1 ; s:ag s, preserving the second condition.Also, buer s is modied in the same way in both cases,so the rst condition is preserved.Remark:Consider the structure of the forward simulation f of this example.In going from FIFO-Stenning to ABP ,integer tags are condensed to their low-order bits.The multiple values of the mapping f essentially \replace" thisinformation.391In this example, the correspondence between ABP and FIFO-Stenningcan be describedin terms of a mapping in the opposite direction - a (single-valued)projection from the state of FIFO-Stenning to that of ABP thatremoves information.Then f maps a state s of ABP tothe set of states of FIFO-Stenning whose projections are equal to s.While this formulation suces to describe many interesting examples,it does not always work.(Consider garbage collection examples.)Machine assistance should be useful in verifying (and maybe producing)such proofs.Liveness:As before, the forward simulation yields a close correspondencebetween executions of the two systems.Given any live execution of ABP , construct a \corresponding"execution 0 of FIFO-Stenning (needs formalizing).Show that 0 is a live execution of FIFO-Stenning:Includes conditions of IOA fairness for the sender and receiver.If not live in this sense, then some IOA class is enabled forever but noaction in that class occurs { easily yields the same situation in (if the correspondence is stated strongly enough), whichcontradicts the fairness of the sender and receiver in .Also includes the channel liveness conditions { innitely manysends imply innitely many receives.Again, this carries over from ABP.So far, we see that we can tolerate all types of channel faults usingStenning, with unbounded \headers" for messages.With \bounded headers" as in ABP, can tolerate loss and duplication,but not reordering.A.1.3 Bounded-Header Protocols Tolerating ReorderingThis leads us to the question of whether we can use bounded headers392and tolerate any reordering.Consider what goes wrong with the ABP, for example, if we attempt touse it with channels that reorder packets.The recipient can get fooled into accepting an old packet with thesame bit as the one expected.This could cause duplicate acceptance of the same message.Here we consider the question of whether there exists a protocol thatuses bounded headers, and tolerates reordering.Wang-Zuck 89 prove that there is no bounded-header protocol that toleratesduplication and reordering, and consequently none that tolerates allthree types of faulty behavior.In contrast, AAFFLMWZ produce a bounded-header protocol that toleratesloss and reordering, but not duplication.That paper also contains an impossibility result for \ecient"bounded-header protocols tolerating loss and reordering.Formalize the notion of bounded-header by assuming that the externalmessage alphabet is nite and requiring that the packet alphabetalso be nite.Wang-Zuck Reo-Dup ImpossibilitySuppose there is an implementation.Starting from an initial state, run the system to send,systematically, copies of as many dierent packets as possible,yielding execution .That is, there is no extension of in which any packet is sentthat isn't also sent in .Suppose there are n send-message events in .Let 0 be a live extension of that contains exactly oneadditional send-message event.By the correcteness condition, all messages in 0 get delivered.Now we construct a nite execution 00that looks like 0 to the receiver, just up to the pointwhere the n + 1st message delivery to the user occurs,393but in which the additional send-message event never occurs.Namely, delay the sender immediately after (also don't allowthe new send-message event).But let the receiver do the same thing that it does in 0 {receive the same packets, send the same packets, deliver the samemessages to the user.It can receive the same packets, even though the sender doesn't sendthem, because the earlier packets in can be duplicated {nothing new can be sent that doesn't appear already in .Then as in 0, it delivers n + 1 messages to the user,even though only n send-message events have occurred.To complete the contradiction, extend 00 to a live executionof the system, without any new send-message events.This has more receive-message events than send-message events, acontradiction.AAFFLMWZ Bounded-Header Protocol Tolerating Loss and ReorderingIt turns out that it is possible to tolerate reorderingand also loss of messages, with bounded headers.This assumes that duplication does not occur.It is not at all obvious how to do this, however it was a conjecturefor a while that this was impossible { that tolerating reorderingand loss would require unbounded headers.This algorithm is NOT a practical algorithm { just a counterexamplealgorithm to show that an impossibility result cannot be proved.The algorithm can most easily be presented in two pieces.The underlying channels are at least guaranteed not to duplicateanything.So rst, use the no-dup channels to implement channels that do notreorder messages (but can lose or duplicate them).Then, use the resulting FIFO channels to implement reliablecommunication.Note that pasting these two together requires each underlying channelto be used for two separate purposes { to simulate channels in two394dierent protocols, one yielding FIFO communication in eitherdirection.This means that the underlying channels need to be fair to eachprotocol separately { need the port structure mentioned earlier.The second task can easily be done using bounded headers - e.g., usethe ABP.The rst is much less obvious.The sender sends a value to the receiver only in response to anexplicit query packet from the receiver.The value that it sends is always the most recent message that wasgiven to it, saved in latest .To ensure that it answers each query exactly once, thesender keeps a variable unanswered which is incrementedwhenever a new query is received, and decremented whenever avalue is sent.The receiver continuously sends query s to the sender, keepingtrack, in pending , of the number of unanswered queries.The receiver counts, in count m], the number of copies of eachvalue m received since the last time it delivered a message(or since the beginning of the run if no message has yet been put onthat buer).At the beginning, and whenever a new message is delivered, the receiversets old to pending .When count m] > old , the receiver knows that m was thevalue of latest at some time after the receiverperformed its last receive event.It can therefore safely output m.The niteness of the message alphabet, the fact that the senderwill always respond to query messages, and the liveness of thechannels, together imply that the receiver will output innitelymany values (unless there is no send event at all).Code:Sender:395Variables:latest , an element of M or nil , initially nilunanswered , a nonnegative integer, initially 0send (m)Eect:latest := mrcv ; pkt (query )Eect:unanswered := unanswered + 1send ; pkt (m)Precondition:unanswered > 0m = latest 6= nilEect:unanswered := unanswered ; 1Receiver:Variables:pending , a nonnegative integer, initially 0,old , a nonnegative integer, initially 0,for each m 2 M , count m], a nonnegative integer,initially 0receive (m)Precondition:count m] > oldEect:count n] := 0 for all n 2 Mold := pendingsend ; pkt (query )Eect:pending := pending + 1rcv ; pkt (m)Eect:396pending := pending ; 1count m] := count m] + 13976.852J/18.437J Distributed AlgorithmsLecturer: Nancy LynchJanuary 19, 1993Lecture 27B.1 Reliable Communication Using Unreliable ChannelsB.1.1 Bounded-Header Protocols Tolerating ReorderingWe began considering bounded-header protocols tolerating reordering.We gave a simple impossibility result for reordering in combinationwith duplication, and then showed the AAFFLMWZ protocol thattolerates reordering in combination with loss (but no duplication).Today we start with an impossibility result saying that it's notpossible to tolerate reordering and loss with an ecient protocol.AAFFLMWZ Impossibility ResultAgain consider the case of channels C sr and C rsthat cannot duplicate messages but can lose and reorder them.Again, if innitely many packets are sent, innitely many of these packetsare required to be delivered.(The impossibility proof will still work if we generalize this condition to acorresponding port-based condition.)As above, we can get a protocol for this settingthat protocol was very inecient in the sense that more and morepackets are required to send individual messages.Now we will show that this is inherent: such a protocol cannot beecient in that it must send more and more messages.Again assume nite message alphabet and nite packet alphabet.398To capture the ineciency, need a denition to capture the numberof packets needed to send a message.First, a nite execution is validif the number of send-msgactions is equal to the number of rec-msg actions.(This means that the datalink protocol succeeded in sending all themessages m provided by the user i.e.,all the messages m for whichan action send-msg(m) occurred.)The following denition expresses the notion that, in order to successfullydeliver any message the datalink protocol only needs (in the best case)to send a bounded number of packets over the channels.De nition 1 If is a valid execution, an extension is ak-extension if:1.

In , the user actions are exactly the two actionssend-msg(m)and rec-msg(m) for some given message m.(This means that exactly one message has been sent successfullyby the protocol.)2. All packets received in are sent in (i.e.,no oldpackets are received).3. The number of rec-pktsr actions in is less than or equal to k.A protocol is k-bounded if there is a k-extension of forevery message m and every valid execution .Theorem 1 There is no k-bounded datalink protocol.Assume there is such a protocol and look for a contradiction.Suppose that there is a multiset T of packets, a nite execution, and a k-extension such that:399 every packet in T is in transit from the s to rafter the execution (i.e.,T is a multiset of \old" packets). the multiset of packets received by the receiver in is asubmultiset of T .We could then derive a contradiction:Consider an alternative execution that begins similarly with ,but that contains no send-msg event.All the packets in T cause the receiver to behave as in thek-extension and hence to generate an incorrectrec-msg action.In other words, the receiver is confused by the presence of oldpackets in the channel, which were left in transit in the channel in and are equivalent to those sent in .At the end of the alternative execution, a message has been receivedwithout its being sent, and the algorithm fails.(Note that we are here assuming a universal channel { one thatcan actually exhibit all the behavior that is theoretically allowedby the channel spec.