ࡱ>  |yz{~wgY CzbjbjWW 3==U]   2 J J J ^ ^ ^ ^ 8 l,^ IfffffHT,AAAAKAPICPD$KMD1J ffD:J J ff:::J fJ fA^ ^ J J J J A::AJ J Af.hm.^ ^ 3AChapter 10 Reliable Messages  XE "Reliable Messages " and Connection Establishment  XE "Connection Establishment "  Butler W. Lampson This chapter appeared in Distributed Systems, ed. S. Mullender, Addison-Wesley, 1993, pp 251-281. It is the result of joint work with Nancy Lynch and Jrgen Sgaard-Andersen. 10.1 Introduction Given an unreliable network, we would like to reliably deliver messages from a sender to a receiver. This is the function of the transport  XE "transport " layer of the ISO seven-layer cake. It uses the network  XE "network " layer, which provides unreliable message delivery, as a channel for communication between the sender and the receiver. Ideally we would like to ensure that messages are delivered in the order they are sent, every message sent is delivered exactly once XE "exactly once" , and an acknowledgement  XE "acknowledgement " is returned for each delivered message. Unfortunately, its expensive to achieve the second and third goals in spite of crashes and an unreliable network. In particular, its not possible to achieve them without making some change to stable state  XE "stable state " (state that survives a crash) every time a message is received. Why? When we receive a message after a crash, we have to be able to tell whether it has already been delivered. But if delivering the message doesnt change any state that survives the crash, then we cant tell. So if we want a cheap deliver operation which doesnt require writing stable state, we have to choose between delivering some messages more than once and losing some messages entirely when the receiver crashes. If the effect of a message is idempotent XE "idempotent" , of course, then duplications are harmless and we will choose the first alternative. But this is rare, and the latter choice is usually the lesser of two evils. It is called at-most-once XE "at-most-once"  message delivery. Usually the sender also wants an acknowledgement that the message has been delivered, or in case the receiver crashes, an indication that it might have been lost. At-most-once messages with acknowledgements are called reliable messages. There are various ways to implement reliable messages. An implementation is called a protocol XE "protocol" , and we will look at several of them. All are based on the idea of tagging a message with an identifier and transmitting it repeatedly to overcome the unreliability of the channel. The receiver keeps a stock of good identifiers that it has never accepted before; when it sees a message tagged with a good identifier, it accepts it, delivers it, and removes that identifier from the good set. Otherwise, the receiver just discards the message, perhaps after acknowledging it. In order for the sender to be sure that its message will be delivered rather than discarded, it must tag the message with a good identifier. What makes the implementations tricky is that we expect to lose some state when there is a crash. In particular, the receiver will be keeping track of at least some of its good identifiers in volatile variables, so these identifiers will become bad at the crash. But the sender doesnt know about the crash, so it will go on using the bad identifiers and thus send messages that the receiver will reject. Different protocols use different methods to keep the sender and the receiver more or less in sync about what identifiers to use. In practice reliable messages are most often implemented in the form of connections. The idea is that a connection is established, any amount of information is sent on the connection, and then the connection is closed. You can think of this as the sending of a single large message, or as sending the first message using one of the protocols we discuss, and then sending later messages with increasing sequence numbers. Usually connections are full-duplex, so that either end can send independently, and it is often cheaper to establish both directions at the same time. We ignore all these complications in order to concentrate on the essential logic of the protocols. What we mean by a crash is not simply a failure and restart of a node. In practice, protocols for reliable messages have limits, called timeouts XE "timeouts" , on the length of time for which they will wait to deliver a message or get an ack. We model the expiration of a timeout as a crash: the protocol abandons its normal operation and reports failure, even though in general its possible that the message in fact has been or will be delivered. We begin by writing a careful specification S for reliable messages. Then we present a lower-level spec D  XE "D " in which the non-determinism  XE "non-determinism "  XE ".i.non-determinism " ;associated with losing messages when there is a crash  XE "crash " is moved to a place that is more convenient for implementations. We explain why D implements S but dont give a proof, since that requires techniques beyond the scope of this chapter. With this groundwork, we present a generic protocol G and a proof that it implements D. Then we describe two protocols that are used in practice, the handshake protocol H and the clock-based protocol C, and show how both implement G. Finally, we explain how to modify our protocols to work with finite sets of message identifiers, and summarize our results. The goals of this chapter are to: Give a simple, clear, and precise specification of reliable message delivery in the presence of crashes. Explain the standard handshake protocol for reliable messages that is used in TCP, ISO TP4, and many other widespread communication systems, as well as a newer clock-based protocol. Show that both protocols can be best understood as special cases of a simpler, more general protocol for using identifiers to tag messages and acknowledgements for reliable delivery. Use the method of abstraction functions and invariants to help in understanding these three subtle concurrent and fault-tolerant algorithms, and in the process present all the hard parts of correctness proofs for all of them. Take advantage of the generic protocol to simplify the analysis and the arguments. 10.1.1 Methods We use the definition of implements and the abstraction function  XE "abstraction function " proof method explained in Chapter 3. Here is a brief summary of this material. Suppose that X and Y are state machines  XE "state machines " with named transitions called actions; think of X as a specification and Y as an implementation. We partition the actions  XE "actions " of X and Y into external and internal actions. A behavior of a machine M is a sequence of actions that M can take starting in an initial state, and an external behavior of M is the subsequence of a behavior  XE "behavior " that contains only the external actions. We say Y implements X iff every external behavior  XE "external behavior " of Y is an external behavior of X. This expresses the idea that what it means for Y to implement X is that from the outside you dont see Y doing anything that X couldnt do. The set of all external behaviors is a rather complicated object and difficult to reason about. Fortunately, there is a general method for proving that Y implements X without reasoning explicitly about behaviors in each case. It works as follows. First, define an abstraction function f from the state of Y to the state of X. Then show that Y simulates X: 1. f maps an initial state of Y to an initial state of X. 2. For each Y-action and each reachable state y there is a sequence of X-actions (perhaps empty) that is the same externally, such that the following diagram commutes.  EMBED Word.Picture.8  A sequence of X-actions is the same externally as a Y-action if they are the same after all internal actions are discarded. So if the Y-action is internal, all the X-actions must be internal (perhaps none at all). If the Y-action is external, all the X-actions must be internal except one, which must be the same as the Y-action. A straightforward induction shows that Y implements X: For any Y-behavior we can construct an X-behavior that is the same externally, by using (2) to map each Y-action into a sequence of X-actions that is the same externally. Then the sequence of X-actions will be the same externally as the original sequence of Y-actions. In order to prove that Y simulates X we usually need to know what the reachable states  XE "reachable states " of Y are, because it wont be true that every action of Y from an arbitrary state of Y simulates a sequence of X-actions; in fact, the abstraction function  XE "abstraction function " might not even be defined on an arbitrary state of Y. The most convenient way to characterize the reachable states of Y is by an invariant, a predicate that is true of every reachable state. Often its helpful to write the invariant  XE "invariant " as a conjunction, and to call each conjunct an invariant. Its common to need a stronger invariant than the simulation requires; the extra strength is a stronger induction hypothesis that makes it possible to establish what the simulation does require. So the structure of a proof goes like this: Establish invariants to characterize the reachable states, by showing that each action maintains the invariants. Define an abstraction function. Establish the simulation XE "simulation" , by showing that each Y-action simulates a sequence of X-actions that is the same externally. This method works only with actions and does not require any reasoning about behaviors. Furthermore, it deals with each action independently. Only the invariants connect the actions. So if we change (or add) an action of Y, we only need to verify that the new action maintains the invariants and simulates a sequence of X-actions that is the same externally. We exploit this remarkable fact in Section 10.9 to extend our protocols so that they use finite, rather than infinite, sets of identifiers. In what follows we give abstraction functions and invariants for each protocol. The actual proofs  XE "proofs " that the invariants hold and that each Y-action simulates a suitable sequence of X-actions are routine, so we give proofs only for a few sample actions. 10.1.2 Types and NNotation We use a type  XE "type " M  XE "M " for the messages being delivered. We assume nothing about M. All the protocols except S and D use a type I  XE "I " of identifier XE "identifier"  XE ".i.identifier" ;s for messages. In general we assume only that Is can be compared for equality; C assumes a total ordering XE "total ordering" . If x is a multiset  XE "set " whose elements have a first I component, we write ids(x)  XE "ids(x) "  XE ".i.ids(x) " ;for the multiset of Is that appear first in the elements of x. We write ... for a sequence with the indicated elements and + for concatenation of sequences. We view a sequence as a multiset in the obvious way. We write x = (y, *) to mean that x is a pair whose first component is y and whose second component can be anything, and similarly for x = (*, y).  XE "... for a sequence with the indicated elements and + for concatenation of sequences. We view a sequence as a multiset in the obvious way. We write x = (y, *) to mean that x is a pair whose first component is y and whose second component can be anyt"  We define an action by giving its name, a guard that must be true for the action to occur, and an effect described by a set of assignments to state variables. We encode parameters by defining a whole family of actions with related names; for instance, get(m) is a different action for each possible m. Actions are atomic XE "atomic" ; each action completes before the next one is started. To express concurrency we introduce more actions. Some of these actions may be internal, that is, they may not involve any interaction with the client of the protocol. Internal actions usually make the state machine non-deterministic XE "non-deterministic" , since they can happen whenever their guards are satisfied, not just when there is an interaction with the environment. We mark external actions with *s, two for an input action and one for an output action. Actions without *s are internal. Its convenient to present the sender actions on the left and the receiver actions on the right. Some actions are not so easy to categorize, and we usually put them on the left. 10.2 The Specification  XE "Specification " S XE "S"  The specification S for reliable messages is a slight extension of the spec for a fifo queue XE "fifo queue" . Figure 10.1 shows the external actions and some examples of its transitions. The basic state of S is the fifo queue q of messages, with put(m) and get(m) actions. In addition, the status variable records whether the most recently sent message has been delivered. The sender can use getAck(a) to get this information; after that it may be forgotten by setting status to lost, so that the sender doesnt have to remember it forever. Both sender and receiver can crash and recover. In the absence of crashes, every message put is delivered by get in the same order and is positively acknowledged. If there is a crash XE "crash" , any message still in the queue may be lost at any time between the crash and the recovery, and its ack may be lost as well. The getAck XE "getAck" (a) action reports on the message most recently put, as follows. If there has been no crash since it was put there are two possibilities: the message is still in q and getAck cannot occur; the message was delivered by get XE "get" (m) and getAck(OK) occurs. If there have been crashes, there are two additional possibilities: the message was lost and getAck(lost) occurs; the message was delivered or is still in q but getAck(lost) occurs anyway. The ack makes the most sense when the sender alternates put(m) and getAck(a) actions. Note that what is being acknowledged is delivery of the message to the client XE "client" , not its receipt by some part of the implementation XE "implementation" , so this is an end-to-end  XE "end-to-end "  XE ".i.end-to-end " ;ack. In other words, the get should be thought of as including client processing of the message, and the ack might include some result returned by the client such as the result of a remote procedure call XE "remote procedure call" . This could be expressed precisely by adding an ack action for the client. We wont do that because it would clutter up the presentation without improving our understanding of how reliable messages work.  EMBED Word.Picture.8  XE ""  Figure 10.1. Some states and transitions for S To define S we introduce the types A (for acknowledgement) with values in {OK, lost} and Status  XE "Status " with values in {OK, lost, ?}. Table 10.1 gives the state and actions of S. Note that it says nothing about channels; they are part of the implementation and have nothing to do with the spec. Why do we have both crash and recover actions, as opposed to just a crash action? A spec which only allows  XE "lost message" messages to be lost at the time of a crash  XE "crash " is not implemented by a protocol like C  XE "C " in which the sender accepts a message with put and sends it without verifying that the receiver is running normally. In this case the message is lost even though it wasnt in the system at the time of the crash. This is why we have a separate recoverr action which allows the receiver to declare the point after a crash when messages are again guaranteed not to be lost. There seems to be no need for a recovers action, but we have one for symmetry. A spec which only allows messages to be lost at the time of a recover XE "recover"  is not implemented by any protocol that can have two messages in the network at the same time, because after a crashs and before the following recovers its possible for the second message in the network to be delivered, which means that the first one must be lost to preserve the fifo property. SenderReceiverNameGuardEffectNameGuardEffect**put(m)recs = falseappend m to q, status := ?*get(m)recr = false, m is first on qremove head of q, if q = empty and status = ? then status := OK*getAck(a)recs = false, status = aoptionally status := lost**crashsrecs := true**crashrrecr := true*recoversrecsrecs := false*recoverrrecrrecr := falseloserecs or recr delete some element from q; if it s the last then status := lost, or status := lostq : sequence[M] :=  XE ".i.q : sequence[M] := "  XE "q : sequence[M] :=  XE \".i.q : sequence[M] := \" "  status : Status := lost XE "status : Status := lost"  recs XE "recs"  : Boolean := false (rec is short for recovering) recr XE "recr"  : Boolean := false Table 10.1. State and actions of S The simplest spec which covers both these cases can lose a message at any time between a crash and its following recover, and we have adopted this alternative. 10.3 The Delayed-Decision Specification D Next we introduce an implementation of S, called the delayed-decision  XE "delayed-decision "  XE ".i.delayed-decision " specification ;D, XE "D,"  that is more non-deterministic about when messages are lost. The reason for D is to simplify the proofs of the protocols: with more freedom in D, its easier to prove that a protocol simulates D than to prove that it simulates S. A typical protocol transmits messages from the sender to the receiver over some kind of channel which can lose messages; to compensate for these losses, the sender retransmits XE "retransmits" . If the sender crashes with a message in the channel it stops retransmitting, but whether the receiver gets the message depends on whether the channel loses it. This may not be decided until after the sender has recovered. So the protocol doesnt decide whether the message is lost until after the sender has recovered. D has this freedom, but S does not. D is the same as S except that the decisions about which messages to lose at recovery, and whether to lose the ack, are made by asynchronous drop actions that can occur after recovery. Each message in q, as well as the status variable, is augmented by an extra component ;of type Mark which is normally +  XE "+ " but may become #  XE "" \t " " between crash and recovery because of a mark action. At any time an unmark action can change a mark from # back to +, a message marked # can be lost by drop, or a status marked # can be set to lost by drop. Figure 10.2 gives an example of the transitions of D; the + marks are omitted.  EMBED Word.Picture.8  Figure 10.2. Some states and transitions of D SenderReceiverNameGuardEffectNameGuardEffect**put(m)recs = falseappend (m, +) to q, status := (?, +)*get(m)recr = false, (m, *) first on qremove head of q, if q = empty and status = (?, x) then status:=(OK,x)*getAck(a)recs = false, status = (a, *) status := (a, +) or status := (lost, +)**crashsrecs := true**crashrrecr := true*recoversrecsrecs := false*recoverrrecrrecr := falsemarkrecs or recrfor some element of q or for status, mark := #unmarkfor some element of q or for status, mark := +drop delete an element of q with mark = #; if it was the last element, status := (lost, +) or if status = (*, #), status := (lost, +) XE ""  q : sequence[(M, Mark)] := status : (Status, Mark) := (lost, +) XE "status : (Status, Mark) := (lost, +)"  recs XE "recs"  : Boolean := false recr XE "recr"  : Boolean := false Table 10.2. State and actions of D To define D we introduce the type Mark  XE "Mark " which has values in the set {+ XE "+" , # XE "" \t "" }. Table 10.2 gives the state and actions of D. 10.3.1 Proof that D Implements S We do not give this proof, since to do it using abstraction functions we would have to introduce prophecy variables, also known as multi-valued mappings or backward simulations (Abadi and Lamport [1991], Lynch and Vaandrager [1993]). If you work out some examples, however, you will probably see why the two specs S and D have the same external behavior. 10.4 Channels XE "Channels"  NameGuardEffectNameGuardEffect**sendsr(p)add some number of copies of p to sr**sendrs(p)add some number of copies of p to rs*rcvsr(p) p srremove one p from srrcvrs(p) p rsremove one p from rslosesr(p) p srremove one p from srlosers(p) p rsremove one p from rsTable 10.3. Actions of the channels All our protocols use the same channel abstraction to transfer information between the sender and the receiver. We use the name packet XE "packet"  for the messages sent over a channel XE "channel" , to distinguish them from reliable messages. A channel can freely drop and reorder packets, and it can duplicate a packet any finite number of times when its sent; the only thing it isnt allowed to do is deliver a packet that wasnt sent. The reason for using such a weak specification is to ensure that the reliable message protocol will work over any bit-moving mechanism that happens to be available. With a stronger channel spec, for instance one that doesnt reorder packets, its possible to have somewhat simpler or more efficient implementations. There are two channels sr  XE "sr " and rs XE "rs" , one from sender  XE "sender " to receiver  XE "receiver " and one from receiver to sender, each a multiset of packets initially empty. The nature of a packet  XE "packet " varies from one protocol to another. Table 10.3 gives the channel actions. Protocols interact with the channels through the external actions send(...) and rcv(...) which have the same names in the channel and in the protocol. One of these actions occurs if both its pre-conditions are true, and the effect is both the effects. This always makes sense because the states are disjoint. 10.5 The Generic Protocol G The generic protocol  XE "generic protocol "  XE ".i.generic protocol " ;G  XE "G " generalizes two practical protocols described later, H  XE "H " and C; in other words, both of them implement G XE "C\; in other words, both of them implement G" . This protocol cant be implemented directly because it has some magic XE "magic"  actions that use state from both sender and receiver. But both real protocols implement these actions, each in its own way. The basic idea is derived from the simplest possible distributed implementation of S, which we call the stable protocol  XE "stable protocol "  XE ".i.stable protocol " ;SB XE "SB" . In SB all the state is stable (that is, nothing is lost when there is a crash) XE "stable (that is, nothing is lost when there is a crash)" , and each end keeps a set gs or gr  XE "gs or gr " of good identifiers XE "good identifiers" , that is, identifiers that have not yet been used. Initially gs gr, and the protocol maintains this as an invariant. To send a message the sender  XE "sender " chooses a good identifier i from gs, attaches i to the message, moves i from gs to a lasts  XE "lasts " variable, and repeatedly sends the message. When the receiver  XE "receiver " gets a message with a good identifier it accepts the message, moves the identifier from gr to a lastr variable, and returns an ack packet for the identifier after the message has been delivered by get. When the receiver gets a message with an identifier that isnt good, it returns a positive ack  XE "ack " if the identifier equals lastr and the message has been delivered. The sender waits to receive an ack for lasts before doing getAck(OK). There are never any negative acks, since nothing is ever lost. This protocol satisfies the requirements of S; indeed, it does better since it never loses anything. 1. It provides at-most-once delivery  XE "at-most-once delivery " because the sender never uses the same identifier for more than one message, and the receiver accepts an identifier and its message only once. 2. It provides fifo ordering  XE "fifo ordering " because at most one message is in transit at a time. 3. It delivers all the messages because the senders good set is a subset of the receivers. 4. It acks every message because the sender keeps retransmit XE "retransmit" ting until it gets the ack. The SB protocol is widely used in practice, under names that resemble queuing system XE "queuing system" . It isnt used to establish connections because the cost of a stable storage write for each message is too great. In G we have the same structure of good sets and last variables. However, they are not stable in G because we have to update them for every message, and we don t want to do a stable write for every message. Instead, there are operations to grow  XE "grow " and shrink  XE "shrink " the good sets; these operations maintain the invariant gs gr as long as there is no receiver crash. When there is a crash, messages and acks can be lost, but S and D allow this. Figure 10.3 shows the state and some possible transitions of G in simplified form. The names in outline font are state variables of D, and the corresponding values are the values of the abstraction function in that state.  EMBED Word.Picture.8  Figure 10.3. Some states and transitions of G Figure 10.4 shows the state of G, the most important actions, and the S-shaped flow of information. The new variables in the figure are the complement of the used variables in the code. The heavy lines show the flow of a new identifier from the receiver to the sender, back to the receiver along with the message, and then back again to the sender along with the acknowledgement. G also satisfies the requirements of S, but not quite in the same way as SB. 1. At-most-once delivery is the same as in SB. 2. The sender may send a message after a crash without checking that a previous outstanding message has actually been received. Thus more than one message can be in transit at a time, so there must be a total ordering  XE "ordering " on the identifiers in transit to maintain fifo ordering  XE "fifo ordering " of the messages. In G this ordering is defined by the order in which the sender chooses identifiers. 3. Complete delivery is the same as in SB as long as there is no receiver crash. When the receiver crashes gs gr may cease to hold, with the effect that messages that the sender handles during the receiver crash may be assigned identifiers that are not in gr and hence may be lost. The protocol ensures that this can t happen to messages whose put happens after the receiver has recovered. When the sender crashes, it stops retransmitting the current message, which may be lost as a result. 4. As in SB, the sender keeps retransmit XE "retransmit" ting until it gets an ack XE "ack" , but since messages can be lost, there must be negative  XE "negative " as well as positive  XE "positive " acks. When the receiver sees a message with an identifier that is not in gr and not equal to lastr it optionally returns a negative ack. There is no point in doing this  XE "point in doing this " for a message with i < lastr because the sender only cares about the ack for lasts, and the protocol maintains the invariant lastr lasts. If i > lastr, however, the receiver must sometimes send a negative ack in response so that the sender can find out that the message may have been lost.  EMBED Word.Picture.8  Figure 10.4. State, main actions, and information flow of G G is organized into a set of implementable actions that also appear, with very minor variations, in both H and C, plus the magic grow, shrink, and cleanup actions that are simulated quite differently in H and in C. When there are no crashes, the sender and receiver each go through a cycle of modes XE "cycle of modes" , the sender perhaps one mode ahead. In one cycle one message is sent and acknowledged. For the sender, the modes  XE "modes " are idle, [needI XE "needI" ], send XE ""  XE "send.i." ; for the receiver, they are idle XE "idle"  and ack XE "ack" . An agent that is not idle is busy XE "busy" . The bracketed mode is internal: its possible to advance to the next mode without receiving another message. The modes are not explicit state variables, but instead are derived from the values of the msg and last variables, as follows: XE "bracketed mode is internal: its possible to advance to the next mode without receiving another message. The modes are not explicit state variables, but instead are derived from the values of the msg and last variables, as follows:"  modes = idle iff msg = nil moder = idle iff lastr = nil modes = needI iff msg nil and lasts = nil modes = send iff msg nil and lasts nil moder = ack iff lastr nil To define G we introduce the types: I XE " I" , an infinite set of identifiers. P  XE " P " (packet), a pair (I, M or A). The sender sends (I, M) packets to the receiver, which sends (I, A) packets back. The I is there to identify the packet for the destination. We define a partial order on I by the rule that i < i' iff i precedes i' in the sequence useds. XE "We define a partial order on I by the rule that i < i' iff i precedes i' in the sequence useds."   EMBED Word.Picture.8  Figure 10.5. Details of actions and information flow in G The G we give is a somewhat simplified version, because the actions are not as atomic as they should be. In particular, some actions have two external interactions, sometimes one with a channel and one with the client, sometimes two with channels. However, the simplified version differs from one with the proper atomicity only in unimportant details. The appendix gives a version of G with all the fussy details in place. We dont give these details for the C and H protocols that follow, but content ourselves with the simplified versions in order to emphasize the important features of the protocols. Figure 10.5 is a more detailed version of Figure 10.4, which shows all the actions and the flow of information between the sender and the receiver. State variables are given in bold, and the black guards on the transitions give the pre-conditions. The mark variable can be # when the receiver has recovered since a message was put; it reflects the fact that the message may be dropped. Table 10.4 gives the state and actions of G. The magic parts, that is, those that touch non-local state, are boxed. The conjunct recs has been omitted from the guards of all the sender actions except recovers, and likewise for recr and the receiver actions. NameGuardEffectNameGuardEffect**put(m)msg = nil,  EQ \x(gs gr or recr) msg := m,  EQ \x(mark := +) choose(i)msg nil, lasts = nil, i gsgs  :={j | j i}, lasts := i, useds +:= i*get(m)exists i such that rcvsr(i,m), i grgr  :={j | j i}, lastr := i, sendrs(i, OK)sendlasts nilsendsr(lasts, msg)*getAck(a)rcvrs(lasts, a)lasts := nil, msg := nilsendAckexists i such that rcvsr(i, *), i groptionally sendrs (i, if i = lastr then OK else lost)**crashsrecs := true**crashrrecr := true*recoversrecslasts := nil, msg := nil, recs := false*recoverrrecr, usedr gs usedslastr := nil, mark := #, recr := falseshrinks(i)gs  := {i}shrinkr(i)i gs, i lasts or mark = #gr  := {i}grows(i)i useds, i gr or recr gs +:= {i}growr(i)i usedrgr +:= {i}, usedr +:= {i}grow-useds(i)i useds gs, i usedr or recruseds +:= {i}cleanuplastr lastslastr := nilunmarkgs gr, lasts gr {lastr,nil}mark := + useds : sequence[I] := (stable) usedr : set[I] := { } (stable) gs : set[I] := { } gr : set[I] := { } lasts : I or nil := nil lastr : I or nil := nil msg : M or nil := nil mark : Mark := # recs : Boolean := false recr : Boolean := false Table 10.4. State and actions of G In addition to meeting the spec S XE "S" , this protocol has some other important properties: It makes progress XE "progress"  XE ".i.progress" ;: regardless of prior crashes XE "crashes" , provided both ends stay up and the channels dont always lose messages, then if theres a message to send it is eventually sent, and otherwise both parties eventually become idle, the sender because it gets an ack, the receiver because eventually cleanup makes mode = idle XE "idle, the sender because it gets an ack, the receiver because eventually cleanup makes mode = idle" . Progress depends on doing enough grow actions, and in particular on completing the sequence growr(i), grows(i), choose(i). Its not necessary to do a stable  XE "stable "  XE ".i.stable " storage operation ;for each message. Instead, the cost of a stable storage operation can be amortized over as many messages as you like. G has only two stable variables: useds and usedr. Different implementations of G handle useds differently. To reduce the number of stable updates to usedr, refine G to divide usedr into the union of a stable usedr-s and a volatile usedr-v. Move a set of Is from usedr-s to usedr-v with a single stable update. The usedr-v becomes empty in recoverr; simulate this with growr(i) followed immediately by shrinkr(i) for every i in usedr-v. The only state required for an idle agent is the stable variable used XE "used" . All the other (volatile) state is the same at the end of a message transmission as at the beginning. The sender forgets its state in getAck, the receiver in cleanup, and both in recover. The shrink actions make it possible for both parties to forget the good sets. This is important because agents may need to communicate with many other agents between crashes, and it isnt practical to require that an agent maintain some state for everyone with whom it has ever communicated. An idle sender doesnt send any packets. An idle receiver doesnt send any packets unless it receives one, because it sends an acknowledgement only in response to a packet. This is important because the channel resources shouldnt be wasted. We have constructed G with as much non-determinism as possible in order to make it easy to prove that different practical protocols implement G. We could have simplified it, for instance by eliminating unmark, but then it would be more difficult to construct an abstraction function from some other protocol to G, since the abstraction function would have to account for the fact that after a recoverr the mark variable is # until the next put. With unmark, an implementation of G is free to set mark back to + whenever the guard is true. 10.5.1 Abstraction Function to D XE "D"  The abstraction function is an essential tool for proving that the protocol implements the spec. But it is also an important aid to understanding what is going on. By studying what happens to the value of the abstraction function during each action of G, we can learn what the actions are doing and why they work. Definitions XE "Definitions"  cur-q = {(msg, mark)} if msg nil and (lasts = nil or lasts gr) { } otherwise inflightsr = {(i, m) ids(sr) | i gr and i lasts}, sorted by i to make a sequence old-q = the sequence of (M, Mark) s gotten by turning each (i, m) in inflightsr into (m, #) inflightrs = {lasts} if (lasts, OK) rs and lasts lastr { } otherwise. Note that the inflights exclude elements that might still be retransmitted as well as elements that are not of interest to the destination. This is so the abstraction function can pair them with the # mark. Abstraction function qold-q + cur-qstatus(?, mark) if cur-q { } (a) (OK, +) if modes = send and lasts = lastr (b) (OK, #) if modes = send and lasts inflightrs (c) (lost, +) if modes = send (d) and lasts (gr {lastr} inflightrs) (lost, +) if modes = idle (e)recs/rrecs/rThe cases of status are exhaustive. Note that we do not want (msg, +) in q if modes = send and lastss gr, because in this case msg has been delivered or lost. We see that G simulates the q of D using old-q + cur-q, and that old-q is the leftover messages in the channel that are still good but havent been delivered, while cur-q is the message the sender is currently working on, as long as its identifier is not yet assigned or still good. Similarly, status has a different value for each step in the delivery process: still sending the message (a), normal ack (b), ack after a receiver crash (c), lost ack (d), or delivered ack (e). 10.5.2 Invariants Like the abstraction function, the invariants are both essential to the proof and an important aid to understanding. They express a great deal of information about how the protocol is supposed to work. Its especially instructive to see how the parts of the state that have to do with crashes (recs/r and mark) affect them. The first few invariants establish some simple facts about the used sets and their relation to other variables. (G2) reflects that fact that identifers move from gs to useds one by one, (G3) the fact that unless the receiver is recovering, identifiers must enter usedr before they can appear anywhere else (G4) the fact that they must enter useds before they can appear in last variables or channels. If msg = nil then lasts = nil (G1) gs useds = { } (G2a) All elements of useds are distinct. (G2b) usedr gr (G3a) If recr then usedr gs useds (G3b) useds {lasts, lastr}  {nil} ids(sr) ids(rs) (G4) The next invariants deal with the flow of identifiers during delivery. (G5) says that each identifier tags at most one message. (G6) says that if all is well, gs and lasts are such that a message will be delivered and acknowledged properly. (G7) says that an identifier for a message being acknowledged can t be good. {m | (i = lasts and m = msg) or (i, m) sr} has 0 or 1 elements (G5) If mark = + and recs and recr then gs gr and lasts gr {lastr, nil} (G6) gr ({lastr} ids(rs)) = { } (G7) Finally, some facts about the identifier lasts for the message the sender is trying to deliver. It comes later in the identifier ordering than any other identifier in sr (G8a). If it s been delivered and is getting a positive ack, then neither it nor any other identifier in sr is in gr, but they are all in usedr (G8b). If it s getting a negative ack then it won t get a later positive one (G8c). If lasts nil then ids(sr) lasts (G8a) and if lasts = lastr or (lasts,OK) rs then ({lasts} ids(sr)) gr = { } (G8b) and ({lasts} ids(sr)) usedr and if (lasts, lost) ids(rs) then lasts lastr (G8c) 10.5.3 Proof that G Implements D XE "Proof that G Implements D"  This requires showing that every action of G simulates some sequence of actions of D which is the same externally. Since G has quite a few actions, the proof is somewhat tedious. A few examples give the flavor. recovers XE "recovers" : Mark msg and drop it unless it moves to old-q; mark and drop status. get(m): For the change to q, first drop everything in old-q less than i. Then m is first on q since either i is the smallest I in old-q, or i = lasts and old-q is empty by (G8a). So Ds get(m) does the rest of what Gs does. Everything in old-q + cur-q that was i is gone, so the corresponding M s are gone from q as required. XE " get(m): .i.For the change to q, first drop everything in old-q less than i. Then m is first on q since either i is the smallest I in old-q, or i = lasts and old-q is empty by (G8a). So Ds get(m) does the rest of what Gs does. Everything in old-q + "  XE "For the change to q, first drop everything in old-q less than i. Then m is first on q since either i is the smallest I in old-q, or i = lasts and old-q is empty by (G8a). So Ds get(m) does the rest of what Gs does. Everything in old-q + cur-q that w"  We do status  XE "status " by the abstraction functions cases on its old value. D says it should change to (OK, x) iff q becomes empty and it was (?, x). In cases (c-e) status isn t (?, x) and it doesn t change. In case (b) the guard i gr of get is false by (G8b). In case (a) either i = lasts or not. If not, then cur-q remains unchanged by (G8a), so status does also and q remains non-empty. If so, then cur-q and q both become empty and status changes to case (b). Simulate this by umarking status if necessary; then D s get(m) does the rest.  getAck(a) XE " getAck(a)" : The q is unchanged because lasts = i ids(rs), so lasts gr by (G7) and hence cur-q is empty, so changing msg to nil keeps it empty. Because old-q doesnt change, q doesnt either. We end up with status = (lost, +) according to case (e), as required by D. Finally, we must show that a agrees with the old value of status. We do this by the cases of status as we did for get: (a) Impossible, because it requires lasts gr, but we know lasts ids(rs), which excludes lasts gr by (G7). (b) In this case lasts = lastr, so (G8c) ensures a lost, so a = OK. (c) If a = OK we are fine. If a = lost drop status first. (d) Since lasts inflightrs, only (lasts, lost) rs is possible, so a = lost. (e) Impossible because lasts nil.  shrinkr XE " shrinkr" : If recr then msg may be lost from q; simulate this by marking and dropping it, and likewise for status. If mark = # then msg may be lost from q, but it is marked, so simulate this by dropping it, and likewise for status. Otherwise the precondition ensures that lasts gr doesn t change, so cur-q and status don t. Inflightsr, and hence old-q, can lose an element; simulate this by dropping the corresponding element of q, which is possible since it is marked #. 10.6 How C and H Implement G We now proceed to give two practical protocols, the clock-based protocol C and the handshake protocol H. Each implements G, but they handle the good sets quite differently. In C the good sets are maintained using time; to make this possible the sender and receiver clocks must be roughly synchronized, and there must be an upper bound on the time required to transmit a packet. The senders current time times is the only member of gs; if the sender has already used times then gs is empty. The receiver accepts any message with an identifier in the range (timer  2e  d, timer + 2e), where e is the maximum clock skew from real time and d the maximum packet transmission time, as long as it hasnt already accepted a message with a later identifier. In H the sender asks the receiver for a good identifier; the receivers obligation is to keep the identifier good until it crashes or receives the message, or learns from the sender that the identifier will never be equal to lasts. We begin by giving the abstraction functions from C and H to G, and a sketch of how each implements the magic actions of G, to help the reader in comparing the protocols. Careful study of these should make it clear exactly how each protocol implements Gs magic actions in a properly distributed fashion. Then for each protocol we give a figure that shows the flow of packets, followed by a formal description of the state and the actions. The portion of the figures that shows messages being sent and acks returned is exactly the same as the bottom half of Figure 10.4 for G; all three protocols handle messages and acks identically. They differ in how the sender obtains good identifiers, shown in the top of the figures, and in how the receiver cleans up its state. In the figures for C and H we show the abstraction function to G in outline font. Note that G allows either good set to grow or shrink by any number of Is through repeated grow or shrink actions as long as the invariants gs gr and lasts gr {lastr} are maintained in the absence of crashes. For C the increase actions  XE "increase actions " simulate occurrences of several growr and shrinkr actions, one for each i in the set defined in the table. Likewise rcvrs(js, i) in H may simulate several shrinks actions. Abstraction functions to G G CHuseds{i | 0 i < times} {sent}  {nil}useds (history)usedr{i | 0 i < low}usedrgs XE "gs" {times}  {sent}{i | (js, i) rs}gr  XE "gr " {i | low < i and i < high}{ir}  {nil}mark# if lasts gr and deadline = nil + otherwise# if modes = needI and gs gr + otherwisemsg, lasts/r, and recs/r are the same in G, C, and Hsrsrthe (I, M) messages in srrsrsthe (I, A) messages in rsSketch of implementations G C XE "C" H XE "H" grow XE "grow" s(i)tick(i) sendrs XE "sendrs" (js, i)shrink XE "shrink" s(i)tick XE "tick" (i'), i {times}  {sent}losers;(js, i) if the last copy is lost XE "js, i) if the last copy is lost"  or rcvrs XE "rcvrs" (js XE "js" , i'), for each i gs  {i'}growr(i)increase-high XE "increase-high" (i'), for each i {i | high  XE "high " < i < i'}mode = idle  XE "idle " and rcvsr(needI, *)shrinkr(i)increase-low XE "increase-low" (i'), for each i {i | low  XE "low " < i i'}rcvsr(ir, done)cleanup XE "cleanup" cleanuprcvsr XE "rcvsr" (lastr, done) XE "lastr, done)" 10.7 The Clock-Based Protocol C This protocol is due to Liskov, Shrira, and Wroclawski [1991]. Figure 10.6 shows the state and the flow of information. Compare it with Figure 10.4 for G, and note that there is no flow of new identifiers from receiver to sender. In C the passage of time supplies the sender with new identifiers, and is also allows the receiver to clean up its state. The idea behind C is to use loosely synchronized clocks  XE "synchronized clocks " to provide the identifiers for messages. The sender uses its current time for the next identifier. The receiver keeps track of low, the biggest clock value for which it has accepted a message: bigger values than this are good. The receiver also keeps a stable bound high on the biggest value it will accept, chosen to be larger than the receivers clock plus the maximum clock skew XE "clock skew" . After a crash the receiver sets low := high; this ensures that no messages are accepted twice.  EMBED Word.Picture.8  Figure 10.6. The flow of information in C The senders clock advances, which ensures that it will get new identifiers and also ensures that it will eventually get past low and start sending messages that will be accepted after a receiver crash. Its also possible for the receiver to advance low spontaneously (by increase-low) if it hasnt received a message for a long time, as long as low stays smaller than the current time 2e  d, where e is the maximum clock skew from real time and d is the maximum packet transmission time XE "maximum packet transmission time" . This is good because it gives the receiver a chance to run several copies of the protocol (one for each of several senders), and make the values of low the same for all the idle senders. Then the receiver only needs to keep track of a single low for all the idle senders, plus one for each active sender. Together with Cs cleanup action this ensures that the receiver needs no storage for idle senders. If the assumptions about clock skew and maximum packet transmission time are violated, C still provides at-most-once delivery, but it may lose messages (because low is advanced too soon or the senders clock is later than high) or acknowledgements (because cleanup happens too soon). Modes, types, packets, and the pattern of messages are the same as in G, except that the I set has a total ordering. The deadline variable expresses the assumption about maximum packet delivery time: real time doesnt advance (by progress) past the deadline for delivering a packet. In a real implementation, of course, there will be some other properties of the channel from which the constraint imposed by deadline can be deduced. These are usually probabilistic; we deal with this by declaring a crash whenever the channel fails to meet its deadline. NameGuardEffectNameGuardEffect**put(m)msg = nilmsg := mchoose(i)msg nil, lasts = nil, i=times, isentsent := i, lasts := i, deadline := now+d*get(m)exists i such that rcvsr(i, m), i (low..high)low := i, lastr := i, deadline := nil, sendrs(i, OK)sendlasts nilsendsr(lasts, msg)*getAck(a)rcvrs(lasts, a)lasts := nil, msg := nilsendAckexists i such that rcvsr(i, *), i (low..high)low := max(low, i), sendrs(i, if i = lastr then OK else lost ) if i = lasts then deadline := nil**crashsrecs := true, deadline:= nil**crashrrecr := true, deadline:= nil*recoversrecslasts := nil, msg := nil, recs := false*recoverrrecr, high < timer  2elastr := nil, low := high, high := timer + 2e + b, recr := falseincrease-low(i)low < i timer  2e  dlow := iincrease-high(i)high < i timer + 2e + bhigh := icleanupsent timessent := nilcleanuplastr < timer  2e  2dlastr := niltick(i)times < i, |now  i| < etimes := itick(i)timer < i, |now  i| < e, i + 2e < high or recrtimer := iprogress(i)now < i, |i  times/r| < e, i < deadline or deadline=nilnow := i times : I := 0 (stable) timer : I := 0 (stable) sent : I or nil := nil low : I := 0 high : I := b (stable) lasts : I or nil := nil lastr : I or nil := nil msg : M or nil := nil recs : Boolean := false recr : Boolean:= false deadline : I or nil := nil now : I := 0 Table 10.5. State and actions of C. Actions below the thick line handle the passage of time. Table 10.5 gives the state and actions of C. The conjunct recs has been omitted from the guards of all the sender actions except recovers, and likewise for recr and the receiver actions. Note that like G, this version of C sends an ack only in response to a message. This is unlike H, which has continuous transmission of the ack and pays the price of a done message to stop it. Another possibility is to make timing assumptions about rs and time out the ack; some assumptions are needed anyway to make cleanup possible. This would be less practical but more like H. Note that times and timer differ from real time (now) by at most e, and hence times and timer can differ from each other by as much as 2e. Note also that the deadline is enforced by the progress action, which doesn't allow real time to advance past the deadline unless someone is recovering. Both crashs and crashr cancel the deadline. About the parameters of C The protocol is parameterized by three constants: " d = maximum time to deliver a packet " b = amount beyond timer + 2e to increase high " e = maximum of |now  timer/s| These parameters must satisfy two constraints: " d > e so that modes = send implies lasts < deadline. " b > 0 so increase-high can be enabled. Aside from this constraint the choice of b is just a tradeoff between the frequency of stable storage writes (at least one every b, so a bigger b means fewer writes) and the delay imposed on recoverr to ensure that messages put after recoverr don t get dropped (as much as 4e + b, because high can be as big as timer + 2e + b at the time of the crash because of (e), and timer  2e has to get past this via tickr before recoverr can happen, so a bigger b means a longer delay). 10.7.1 Invariants Mostly these are facts about the ordering of various time variables; a lot of x nil conjuncts have been omitted. Nothing being sent is later than times (C1). Nothing being acknowledged is later than low, which is no later than high, which in turn is big enough (C2). Nothing being sent or acknowledged is later than lasts (C3). The senders time is later than low, hence good unless equal to sent (C4). lasts ( times (C1) lastr ( low high (C2a) ids(rs) low (C2b) If recr then timer + 2e high (C2c) ids(sr) lasts (C3a) lastr lasts (C3b) {i | (i, OK) rs} lasts (C3c) low times (C4) low < times if lasts times If a message is being sent but hasn t been delivered, and there hasnt been a crash, then deadline gives the deadline  XE "deadline " for delivering the packet containing the message (based on the maximum time for a packet that is being retransmitted to get through sr), and it isnt too late for it to be accepted (C5). If deadline nil then now < lasts + e + d (C5a) low < lasts (C5b) An identifier getting a positive ack is no later than low, hence no longer good (C6). If it s getting a negative ack, it must be later than the last one accepted (C7). If (lasts, OK) rs then lasts low (C6) If (lasts, lost) rs then lastr < lasts (C7) 10.8 The Handshake Protocol  XE "Handshake Protocol " H XE "H"  This is the standard protocol for setting up network connections XE "network connections" , used in TCP XE "TCP" , ISO TP-4 XE "ISO TP-4" , and many other transport protocols XE "transport protocols" . It is usually called three-way handshake XE "three-way handshake" , because only three packets are needed to get the data delivered, but five packets are required to get it acknowledged and all the state cleaned up (Belsnes [1976]). As in the generic protocol XE "generic protocol" , when there are no crashes the sender  XE "sender " and receiver  XE "receiver " each go through a cycle of modes XE "cycle of modes" , the sender perhaps one ahead. For the sender, the modes are idle, needI XE "idle, needI" , send XE ""  XE "send.i." ; for the receiver, they are idle XE "idle" , accept XE "accept" , and ack XE "ack" . In one cycle one message is sent and acknowledged by sending three packets from sender to receiver and two from receiver to sender, for a total of five packets. Table 10.6 summarizes the modes and the packets that are sent. The modes are derived from the values of the state variables j and last: modes = idle iff js = lasts = nil moder = idle iff jr = lastr = nil modes = needI iff js nil moder = accept iff jr nil modes = send iff lasts nil moder = ack iff lastr nil Figure 10.7 shows the state, the flow of identifiers from the receiver to the sender at the top, and the flow of done information back to the receiver at the bottom so that it can clean up. These are sandwiched between the standard exchange of message and ack, which is the same as in G (see Figure 10.4). Intuitively, the reason there are five packets is that: One round-trip  XE "round-trip " (two packets) is needed for the sender to get from the receiver an I (namely ir) that both know has not been used. One round-trip (two packets) is then needed to send and ack the message. SenderReceivermodesendadvance onpacketadvance onsendmodeidle XE "idle" see idle belowput, to needI(i, lost) when (i, m) arrivesidle XE "idle" needI XE "needI" (needI, js) repeatedly(needI, j) (needI, j) arrives, to accept(js, i) arrives, to send(j, i) (jr, ir) repeatedlyaccept XE "accept" send XE "send" (lasts, m) repeatedly(i, m) (ir, m) arrives, to ack (ir, done) arrives, to idle(lasts, a ) arrives, to idle(i, a) (lastr, OK) repeatedlyack XE "ack" idle(i, done) when (i, a) arrives(i, done) (lastr, done) arrives, to idleneedI or send(i, done) when (j js, i) or (i, OK) arrives, to force receiver to idleTable 10.6. Exchange of messages in H A final done  XE "done " packet from the sender informs the receiver that the sender has gotten the ack. The receiver needs this information in order to stop retransmit XE "retransmit" ting the ack and discard its state. If the receiver discards its I got the message state before it knows that the sender got the ack, then if the channel loses the ack the sender wont be able to find out that the message was actually received, even though there was no crash. This is contrary to the spec S. The done packet itself needs no ack, because the sender will also send it when idle and hence can become idle as soon as it sees the ack. We introduce a new type: J XE " J"  XE ".i. J" , an infinite set of identifiers that can be compared for equality. The sender and receiver send packets to each other. An I or J in the first component is there to identify the packet for the destination. Some packets also have an I or J as the second component, but it does not identify anything; rather it is being communicated to the destination for later use. The (i, a) and (i, done) packets are both often called close XE "close"  XE ".i.close"  ;packets in the literature. The H protocol has the same progress and efficiency properties as G, and in addition, although the protocol as given does assume an infinite  XE "infinite " supply of Is, it does not assume anything about clocks XE "clocks" .  EMBED Word.Picture.8  Figure 10.7. The flow of information in H Its necessary for a busy agent  XE "busy agent " to send something repeatedly, because the other end might be idle and therefore not sending anything that would get the busy agent back to idle. An agent also has a set of expected packets XE "expected packets" , and it wants to receive one of these in order to advance normally to the next mode. To ensure that the protocol is self-stabilizing  XE "self-stabilizing "  XE ".i.self-stabilizing " ;after a crash, both ends respond to an unexpected packet  XE "unexpected packet " containing the identifier i by sending an acknowledgement XE "acknowledgement" : (i, lost) or (i, done). Whenever the receiver gets done for its current I, it becomes idle. Once the receiver is idle, the sender advances normally until it too becomes idle. Table 10.7 gives the state and actions of H. The conjunct recs has been omitted from the guards of all the sender actions except recovers, and likewise for recr and the receiver actions. 10.8.1 Invariants Recall that ids(c) is {i | (i, *) c}. We also define jds(c) = {j | (j, *) c or (*, j) c}. Most of H s invariants are boring facts about the progress of I s and J s from used sets through i/js/r to lasts/r. We need the history variables useds and seen to express some of them. (H6) says that theres at most one J (from a needI packet) that gets assigned a given I. (H8) says that as long as the sender is still in mode needI, nothing involving ir has made it into the channels. NameGuardEffectNameGuardEffect**put(m)msg = nil, msg := m, exists j such that j j-usedjs := j, j-used +:= {j}requestIjs ( nil, lasts = nilsendsr(needI, js)assignI(j,i)rcvsr(needI, j), ir = lastr = nil, i usedrjr := j, ir := i, usedr +:= i, seen +:= {(j, i)}choose(i)lasts = nil, rcvrs(js, i)js := nil, lasts := i, useds +:= isendIjr nilsendrs(jr, ir)sendlasts nilsendsr(lasts, msg)*get(m)exists i such that rcvsr(i, m), i = irjr := ir := nil, lastr := i, sendrs(i, OK)sendAcklastr nilsendrs(lastr, OK)*getAck(a)rcvrs(lasts, a)if a = OK then sendsr(lasts, done) msg := lasts := nilbounceexists i such that rcvsr(i, *), i ir, i lastrsendrs(i, lost )bounce (j, i) rcvrs(j, i), j js, i lasts or rcvrs(i, OK)sendsr(i, done)cleanup(i)rcvsr(i, done), i = ir or i = lastrjr := ir := nil, lastr := nil**crashsrecs := true**crashrrecr := true*recoversrecsmsg := nil, js := lasts := nil, recs := false*recoverrrecrjr := ir := nil, lastr := nil, recr := falsegrow- j-used(j)j-used +:= {j}grow- used(i)usedr +:= {i}useds : sequence[I] := (history) usedr : set[I] := { } (stable) j-used : set[J] := { } (stable) seen : set[(J, I)] := { } (history) js : J or nil := nil jr : J or nil := nil msg : M or nil := nil ir : I or nil := nil lasts : I or nil := nil lastr : I or nil := nil recs : Boolean := false recr : Boolean := false Table 10.7. State and actions of H. Heavy black lines outline additions to G j-used {js, jr}  {nil} jds(sr) jds(rs) (H1) usedr {ir, lastr}  {nil} useds {i | (*, i) rs} ids(sr) ids(rs) (H2) useds {lasts, lastr}  {nil} ids(sr) ids(rs) (H3) If (i, done) sr then i lasts (H4) If ir nil then (jr, ir) seen (H5) If (j, i) seen and (j , i) seen then j = j (H6) If (j, i) rs then (j, i) seen (H7) If js = jr nil then (ir, *) sr and (ir, done) rs (H8) 10.8.2 Progress XE "Progress"  We consider first what happens without failures, and then how the protocol recovers from failures. If neither partner fails, then both advance in sync through the cycle of modes XE "cycle of modes" . The only thing that derails progress is for some party to change mode without advancing through the full cycle of modes that transmits a message. This can only happen when the receiver is in accept  XE "accept " mode and gets (ir, done), as you can see from Table 10.6. This can only happen if the sender got a packet containing ir. But if the receiver is in accept, the sender must be in needI or send, and the only thing thats been sent with ir is (js, ir) XE "(js, ir)"  XE "ir, done), as you can see from Table 10.6. This can only happen if the sender got a packet containing ir. But if the receiver is in accept, the sender must be in needI or send, and the only thing thats been sent with ir is .i.(js, ir)" . The sender goes to or stays in send and doesnt make done when it gets (js, ir); in either of these modes, so the cycling through the modes is never disrupted as long as theres no crash. If either partner fails and then recovers XE "recovers" , the other becomes idle  XE "idle " rather than getting stuck; in other words, the protocol is self-stabilizing XE "self-stabilizing" . Why? When the receiver isnt idle it always sends something, and if that isnt what the sender wants, the sender responds done, which forces the receiver to become idle. When the sender isnt idle its either in needI, in which case it will eventually get what it wants, or its in send and will get a negative ack and become idle. In more detail: The receiver bails out when the sender crashes because the sender forgets is and js when it crashes, if the receiver isnt idle, it keeps sending (jr, ir) XE "(jr, ir)"  or (lastr, OK) XE "(lastr, OK)" , the sender responds with (ir/lastr, done) XE "(ir/lastr, done)"  when it sees either of these, and the receiver ends up in idle whenever it receives this. The sender bails out or makes progress when the receiver crashes because If the sender is in needI XE "needI" , either it gets (js, i ir) from the pre-crash receiver, advances to send, and bails out as below, or  it gets (js, ir) from the post-crash receiver and proceeds normally. " If the sender is in send  XE "send " it keeps sending (lasts, msg),  the receiver has lastr = nil lasts, so it responds (lasts, lost), and  when the sender gets this it becomes idle. An idle receiver might see an old (needI, j) XE "(needI, j)"  with j js and go into accept with jr js, but the sender will respond to the resulting (jr, ir) packets with (ir, done), which will force the receiver back to idle. Eventually all the old needI packets will drain out. This is the reason that its necessary to prevent a channel from delivering an unbounded number of copies of a packet. 10.9 Finite Identifiers XE "Finite Identifiers"  NameGuardEffectrecycle(i) for Gi gs gr {lasts, lastr} ids(sr) ids(rs)useds  := {i}, usedr  := {i}recycle(i) for Hi {lasts, ir, lastr} {i | (*, i) rs} ids(sr) ids(rs)useds  := {i}, usedr  := {i}, seen  := {j | (j, i) seen | (j, i)}recycle-j(j) for Hj {js, jr} jds(sr) jds(rs)used-j  := {j}, seen  := {i | (j, i) seen | (j, i)}Table 10.8. Actions to recycle identifiers So far we have assumed that the identifier sets I and J are infinite. Practical protocols use sets that are finite and often quite small. We can easily extend G to use finite sets by adding a new action recycle(i) that removes an identifier from useds and usedr so that it can be added to gr again. As we saw in Section 10.1, when we add a new action the only change we need in the proof is to show that it maintains the invariants  XE "invariants " and simulates something in the spec. The latter is simple: recycle simulates no change in the spec. The former is also simple: we put a strong enough guard on recycle to ensure that all the invariants still hold. To find out what this guard is we need only find all the invariants that mention useds or usedr, since those are the only variables that recycle changes. Intuitively, the result is that an identifier can be recycled if it doesnt appear anywhere else in the variables or channels. Similar observations apply to H, with some minor complications to keep the history variable seen up to date, and a similar recycle-j action. Table 10.8 gives the recycle actions for G and H. How can we implement the guards on the recycle actions? The tricky part is ensuring that i is not still in a channel, since standard methods can ensure that it isnt in a variable at the other end. There are three schemes that are used in practice: Use a fifo channel XE "fifo channel" . Then a simple convention ensures that if you dont send any i1s after you send i2, then when you get back the ack for i2 there aren't any i1s left in either channel. Assume that packets in the channel have a maximum lifetime  XE "maximum lifetime " once they have been sent, and wait longer than that time after you stop sending packets containing i. Encrypt packets on the channel, and change the encryption  XE "encryption " key. Once the receiver acknowledges the change it will no longer accept packets encrypted with the old key, so these packets are in effect no longer in the channel. For C we can recycle identifiers by using time modulo some period as the identifier, rather than unadorned time. Similar ideas apply; we omit the details. 10.10 Conclusions We have given a precise specification S of reliable at-most-once message delivery with acknowledgements. We have also presented precise descriptions of two practical protocols (C and H) that implement S, and the essential elements of proofs that they do so; the handshake protocol H is used for connection establishment in most computer networking. Our proofs are organized into three levels: we refine S first into another specification D that delays some of the decisions of S and then into a generic implementation G, and finally we show that C and H both implement G. Most of the work is in the proof that G implements D. In addition to complete expositions of the protocols and their correctness, we have also given an extended example of how to use abstraction functions and invariants to understand and verify subtle distributed algorithms of some practical importance. The example shows that the proofs are not too difficult and that the invariants, and especially the abstraction functions, give a great deal of insight into how the implementations work and why they satisfy the specifications. It also illustrates how to divide a complicated problem into parts that make sense individually and can be attacked one at a time. References Abadi, M. and Lamport, L. (1991), The Existence of Refinement Mappings, Theoretical Computer Science 82 (2), 253-284. Belsnes, D. (1976), Single Message Communication, ieee Trans. Communications com-24, 2. Lampson, B., Lynch, N., and Sgaard-Andersen, J. (1993), Reliable At-Most-Once Message Delivery Protocols, Technical Report, mit Laboratory for Computer Science, to appear. Liskov, B., Shrira, L., and Wroclawski, J. (1991), Efficient At-Most-Once Messages Based on Synchronized Clocks, acm Trans. Computer Systems 9 (2), 125-142. Lynch, N. and Vaandrager, F. (1993), Forward and Backward Simulations, Part I: Untimed Systems, Technical Report, mit Laboratory for Computer Science, to appear. Appendix For reference we give the complete protocol for G, with every action as atomic as it should be. This requires separating the getting and putting of messages, the sending and receiving of packets, the sending and receiving of acks, and the getting of acks. As a result, we have to add buffer queues bufs/r for messages at both ends, a buffer variable ack for the ack at the sender, and a send-ack flag for positive acks and a buffer nack-buf for negative acks at the receiver. The state of the full G is: useds : sequence[I] := (stable) usedr : set[I] := { } (stable) gs : set[I] := { } gr : set[I] := { } lasts : I or nil := nil lastr : I or nil := nil bufs : sequence[M] := bufr : sequence[M] := msg : M or nil := nil mark : + or # := + ack : A := lost send-ack : Boolean := false nack-buf : sequence[I] := recs : Boolean := false recr : Boolean := false The abstraction function to D is: q XE "q"  the elements of bufr  XE "bufr " paired with + XE "+" + old-q + cur-q XE "cur-q" + the elements of bufs  XE "bufs " paired with +status XE "status"  (?, +) if bufs  XE "bufs "  empty else (?, mark) if cur-q { } (a) (?, +) if modes = send, lasts = lastr, bufr  XE "bufr "  { } (b) (OK, +) if modes = send, lasts = lastr, bufr = { } (c) (OK, #) if modes = send and lasts inflightrs (d) (lost, +) if modes = send (e) and lasts (gr {lastr} inflightrs) (ack, +) if modes = idle XE "idle"  (f)recs/rrecs/r NameGuard EffectName GuardEffect**put(m)append m to bufs prepare(m)msg = nil, m first on bufs, gs gr or recrbufs:=tail (bufs), msg := m, mark := +choose(i)msg nil, lasts = nil, i gsgs  := {j | j i}, lasts := i, useds +:= isendsr(i, m)i = lasts nil m = msgrcvsr(i, m)if i gr then append m to bufr, sendAck := false, gr  := {j | j i}, lastr := i, else if i gr {lastr} then optionally nack-buf +:= i else if i = lastr then sendAck :=true*get(m)m first on bufr if bufr = m then sendAck := true, bufr :=tail (bufr)rcvrs(i, a)if i = lasts then ack := a, msg := nil, lasts := nilsendrs (i, OK) sendrs (i, lost)i = lastr, sendAck i first on nack-bufoptionally sendAck := false nack-buf := tail (nack-buf)*getAck(a)msg = nil, bufs = empty, ack = aack := lost**crashsrecs := true**crashrrecr := true*recoversrecslasts := nil, msg := nil, bufs := , ack := lost, recs := false*recoverrrecr, usedr gs usedslastr := nil, mark := #, bufr:= , nack-buf:= , recr:=falseshrinks(i)gs  := {i}shrinkr(i)i gs, i lasts or mark = #gr  := {i}grows(i)i used, i gr or recrgs +:= {i}growr(i)i usedrgr +:= {i}, used +:= {i}grow-useds(i)i used gs, i usedr or recr used +:= {i}cleanuplastr lastslastr := nilunmarkgs gr, lasts gr {lastr, nil}mark := +Table 10.9. G with honest atomic actions  Actually this definition only deals with the implementation of safety properties. Roughly speaking, a safety property is an assertion that nothing bad happens; it is a generalization of the notion of partial correctness for sequential programs. A system that does nothing implements any safety property. Specifications may also include liveness properties, which roughly assert that something good eventually happens; these generalize the notion of termination for sequential programs. A full treatment of liveness is beyond the scope of this chapter, but we do explain informally why the protocols make progress.  You might think it would be more natural and closer to the actual implementation of a channel to allow a packet already in the channel to be duplicated. Unfortunately, if a packet can be duplicated any number of times its possible that a protocol like H (see section 10.8) will not make any progress.  (i, lost) XE "(i, lost)"  is a negative  XE "negative " acknowledgement; it means that one of two things has happened: The receiver has forgotten about i because it has learned that the sender has gotten a positive ack for i, but then the receiver has gotten a duplicate (i, m), to which it responds with the negative ack, which the sender will ignore. The receiver has crashed since it assigned i, and is message may have been delivered to get or may have been lost.  (i, OK) XE "(i, OK)"  is a positive  XE "positive " acknowledgement; it means is message was delivered to get. Butler W. Lampson Reliable Messages and Connection Establishment  "89WXyz{>&'+78:;?OPklp}~ t u y `aekl6<j<U6CJCJjCJ0OJQJUCJ0OJQJ<CJ0OJQJj<CJ0OJQJU CJ0OJQJ CJ(OJQJD {>P V k+'Il$1$ 1$&1$.1$1$1$d$d/.1$$1$H $1$d $1$d @ {>P V k+'Il& `o _!!B"^"#$(C(((f)Z+h,{vqnk+&&Is*&&g@. &3&&&&J &&2&h.(lHIM`a & ,-1GHjk!!!!R![!b!c!!!B"C"Z"["]"E%F%J%`%a%%%&&&&&''jȦ8 CJOJQJUVmH jU j0JU6<<j<URl& `o _!!B"^"#$(C(((f)Z+h,,,D/3Z5R78+1$ */.1$.1$1$&1$' '''((())+++++y,z,,,,,,,,,,,,,,,,-----$-%-2-3-7-E-G-K-\-]-^-------------..>.@.r.t.x.z........../V/X/^/`/0000000EHOJQJ665CJ0<j<U<Xh,,,D/3Z5R78A8;J<<<=>==@@@BDLFMFTFUFVF_F`FaFfFlFsFxF~FFF~wpib^ 6  6  6  6  6  6  6  6  6  6  6  6 9 ,P*wz+&;+&_.}. #00|1~111111333324844444445555 5D6E6I6^6_688!838485868?8@888888889!9(9)9<9?9@9A9B9C9G9J9K9L9M9N9h9n99999:!:%:):::;;;';(;;;;;;;6::<j<U OJQJ jU6U8A8;J<<<=>==@@@BDLFMFTFUFVF_F`F 6$1$Ld$ 6$1$d$,1$*1$+1$&1$1$.1$1$X;;;d<e<j<p<<<<<<<<<<<<<)=/=0=4=i=j=o=u=v=z=========.>/>3>=>>>s>t>x>>>>>>>>>>>>>>???????@@@@@@@@@@A A0A8A>ADAEA j Uj$8 CJOJQJUVmH jU<6<j<U6QEAFAJAUAVAfApA+B0B5B 6 D 6 IJ 6 K 6 T 6 U 6 V 6 ] 6 ^/_,*(./A6 6 % 6 2 6 7!|H~HHHHHHHHHHHHHHHHIIIIIIIIIIIIIIIJJ J JJ J#J&JBJEJFJGJKJSJTJbJgJhJrJJJJKKKKKKKKKKKKKKKKMMMMMOO<<j<U 6CJEHj6U6 OJQJjOJQJUOJQJCJ6LHHhJJ-KWKOQQQQQQQQQ 6$1$d$,1$ *1$.1$1$X1$/1$ A1$   M$$P4ֈp4 !OOOOOPPP!P6P7P;PAPBPTPUPYPdPePPPPPPQQQ&Q*Q.Q2QQQQQQQQQQQQR R RRRRRRRRR'R*R1R2R4R:RFRIRJRKRMRPRQRTRYR]R^RlRmRnR}R~RRRRROJQJ6EHCJ5 jUjI8 CJOJQJUVmH jU<j<U<6NQQQQQQQRR RRRERniii61$$M$$P4ֈ$ 0,!9$$P4`$ 0,! 6$1$d$ ERMRnRRRRRSSSSSSS+S4S5SBSCSMSRS`SjSoS}S~SSSSĽ}voha]VOH 6  6  6  6  6  6  6  6  6  6  6  6  6  6  6  6  6  6  6 J 6 h 6 st 6  6  6 ERMRnRRRRRSSSSh61$d$M$$P4ֈ$ 0P,!61$$ RRRRRRRRRRRRRRRRRRRRRRRRRRRRRRRSS SSSSSSS!S"S&S*S+S-S2S3S5S8S9S=SASBSCSDSKSLSMSPSQSRSUSVSZS_S`SaShSiSjSmSnSoSrSsSwS|S}S~SSSSSSSSSSSSSSSSSCJOJQJ6EH6_SSSS+S4S5SBSCSMSVM$$P4ֈ$ 0,!61$$61$d$M$$P4ֈ$ 0,! MSRS`SjSoS}S~SSSSSSTTrDM$$P4ֈ$ 0,!9$$P4`$ 0,!61$$ SSSTTTT"U$U&U(U*U^VV%WFWXXXXXXXXXYY&Y2Y3YYYZYdYeYgY Z6ZHZJZXZZZ~zsljj 6 K 6 UV 6 | 6 } 6  6  6  6  6  6  6  6  6  6 ./A6  6 _ 6 ` 6 g)SSSSTT@TBTNTXTTTTTTTTUUU"U$U&U(U*U,U4UU@UBU\U^UbUjUvUxUzU|U~UUUUUUUUUUUVVVVVVV#V$V2V7V8V;V{@{B{D{L{N{X{Z{`{h{j{B|C|Z|[|\|]|^|i|} }"}(}.}5}}}}}}P~Q~U~_~`~d~h~ jJUj$8 CJOJQJUVmH j'UOJQJ 6CJEH<j<U6Ph~k~p~q~u~~~~~~~~~~~~~~~~~~~~~~~~~   #(,-.089<BGJ  $*,46<FPVXZ\bOJQJ 6CJEH jU6<j<U6Vbltvxz| $&nprt|ƒă#';<˄τЄф҄9:;<STUVWbx jjUj$8 CJOJQJUVmH j3U jU<j<UOJQJ 6CJEH6M8:>DFJLRXdfvxz|~ȋԋ֋؋܋ދ,.0248:DFLNPRTV\hjrΌԌ،ڌOJQJ 6CJEH j6UCJ5 6CJEH6X*8:Lڋ܋ދP61$d$M$$P4ֈ( hp! 6$1$d$ 6RT^vj`Y61$P$ 61$dP$9$$P4`( hp!61$$61$d$M$$P4ֈ( hp! ڌ܌ތ $&(.24>BDNRTfhjln~čƍ΍Ѝ֍؍ ,.FLPRTVX`bdfhjlnCJ 6CJEHOJQJ6^vڍn܎t61$($61$$61$d$9$$P4`( hp!61$P$ ĎЎ؎  &(08:<>LNPVXZbdlrtȏʏΏ֏؏ڏ܏  ,46>HJLXZ\^`bdfhtvCJOJQJ 6CJEH6^܎ގ  :<PV M$$P4ֈ( hp!61$$61$d$M$$P4ֈ( hp! :<PZΏ.JLbdz̐.DVj 0Lfhjln|Ēؒڒ`IљC>J¤פ٤p֦h§ħƿ5  5  5  5  ???.+&/A6 IPZΏ.JLbdz̐061$d$61$d$$d%d&d'd61$$9$$P4`( hp!61$d($$d%d&d'd61$$vx̐ΐАܐސ"(*.02>@BLNPRTXZ\^fhjlnz|‘đƑΑБґԑ֑ؑڑOJQJ 6CJEH6`̐.DVj|61$d$$d%d&d'd61$d$61$$M$$P4ֈ( hp!61$$  0Lfhjln|ĒؒŌ61$$61$d$$d%d&d'd61$d$$d%d&d'd61$d$61$$9$$P4`( hp! 8:<>@HJLTV^fh~Ē̒֒ؒڒ $,.<>`dftvȓΓ֓ 6CJEH 6CJEHOJQJ6]ؒڒ`IљC>J¤פ 1$?1$1$.1$1$+1$&1$1$/1$A1$9$$P4`( ! "%)034BGHKLZ_`j  =>BMNGNUY\`ae˖̖*./01489:;>DEFmnr}=ABGKLtxy˘ϘИ<<j<U 6CJEH6[И "&')-124VZ[]ovw™ÙǙ˙̙Ι%&Ś̚ښƝ̝Ğ78<AB:<>JLNRdhjnx jU6<j<U 6CJEH6Wxz¡ġʡ̡ޡ  &(,.06<>HJfh¢Т ,0>@HZ^`bdfnprv~£ȣ̣ޣ 6CJEH6OJQJ`פޤ*24:BLTV\dfrvȦ̦ئ (*,.2468:>FHLNP`djr§ާ,2@FVX`hjpx6< 6CJEH 6CJEHOJQJ6\פ٤p֦h§ħbtخZ|<@1$.1$1$1$ 1$ $$P4! 51$$ Xld $$P4!51$$xƨ̨>@Xbhr).Z[\`deíĭ"$ZbƮ̮خڮܮޮ&.0Zbdfhjln̯ԯ֯دگޯCJEHOJQJ 6CJEH6^ħbtخZ|̯>F2PzN9,t'D8!TxTBNPn     5      5    2  2  2 5..B@. 8|̯>F2PzN,t'1$ 1$HP 1$H1$P.1$1$@1$ 1$B1$@1$  *.|~²IJƲʲֲ̲زڲ LTjpr³ijȳгҳܳX\jlnOJQJ6 6CJEH`nX`bdfhnƷηзڷ $*,.02\dfjlvzƸʸظ@Bݺ<j<U jUOJQJ 6CJEH6Wݺ16ABIJWXfgxy}FHjlGILMTZ[\`klÿɿʿxz|~(h6<j<U jUOJQJ 6CJEH6Vht$ &(46bjlrtvx %*;<\bfl 378$,.02<@dlnprtvxCJEHOJQJ 6CJEH<j<U6Xx &(.2TV\dp| (ZbdfhjpvnzXd<j<UOJQJ 6CJEH6Z$48PZ08:FHJ,. "$&(*.68<DFP\^26<j<UOJQJ 6CJEH6Y'D8!TxTBNPn|51$$ $1$$51$$$1$$$$P4 <<<#21$x$1$1$.1$1$2>@ ",.028>BJLPRTV^jlnpxzCJjCJUCJ66CJEHj6CJEHUOJQJ565 6CJEH6Mn,.8XZ\^dj6PR`X~RT+uA&C $&8L^`bdfz6 ,*.2  5 5 =  NO 5 b 5 sL,.8XZ\^dj1$$$$P4 |0<# $1$$51$$51$$$1$$$$P4 <<<#51$$"(.6BJLNPRTV`pv|^jt| 248:LNPRZ\dtvxz6<j<U5j5U565 >*OJQJ 6CJEHOJQJ6P6PR`X~xX5$1$$ 2$1$d$5$1$$2$1$$2$1$$1$$$P4 <<<#z|(*,068:<@HJT\`hlnprtz.02468@LNVnprtvxz jU<CJOJQJ<j<U6 <CJj<CJU 6CJEH6N $&(0BDHJPTX`fnprz468:>@FLNPXhjnprtvz~OJQJ6<j<U 6CJEH6VRT+u&C $h6$1$d$6$1$$,1$*1$1$.1$1$51$$21$$$$P4 <<<# $&.NPcdh58<@uv:= xzOJQJ j0Uj$8 CJOJQJUVmH jFU<j<U jU <CJj<CJU 6CJEH66j6UB&)(/)1nx$*0268>DJLRZ\`bfrtvx $*,.@BZ`dfhjntvxz~ 6CJEHOJQJ56j<U[$&8L^`bdfz^8M$$P4ֈ8 0L"61$$M$$P4ֈ8 0L" "2 $JLNPRh0 DVX`$l~2JZ&.@BDFHJYv3 Tj |&9+[&&./A6 T"2 $JLNPRh0H61$$61$P$9$$P4`8 0L"61$$~,02:<FHJLNT`bdhnrt|~ $,.06FRX`dflrtz 6CJEHOJQJ6` "&6<BDHRTX^`hpt "&.4<>\^`hjrxzOJQJ CJOJQJ 6CJEH6] DVX<^M$$P4ֈ8 0L"61$$M$$P4ֈ8 0L" `$l~rM$$P4ֈ8 0L"9$$P4`8 0L"61$$  "*02468@B`bhjlrz~ "$&.02:Bbdjrt CJ 6CJEH 6CJEHOJQJ6\2JZ&h9$$P4`8 0L"61$$ "$.068>@FLNPVX\^fhnv $&,.4<>@BHTX\^| ,46< 6CJEHOJQJCJ 6CJEH6\.@BDFHJYv TH1$1$$$$1$/$1$A1$$$P488L"61$$M$$P4ֈ8 0L"      <>FLTdfhlnv|  !%(,2;>GHXc:ABWZ[!np #&"$.68 2:<DF`OJQJ 6CJEH6`Tj |  B    &   Lpp@1$B1$@1$1$1$+1$&1$.1$`hnr.68>FX`bhx"$N\^>FHPRXZ&(Z\LPRZ"%>B j 6OJQJ 6CJEHCJOJQJ6Z   B    &    Lpp@/&>@BDVXZ\fp "$d>@BDFH|<>LPDfhr &..B@.X           " & * , . 4 L R T ` h j r t v x z                                & , . 0 2 : < H N T \ ^ f n p r t v ~   # 7 8 < I J <j<UOJQJ j 6CJEH6XJ      $,.46<>LRX`d$&*268:>JRTZbd|~56:QR|} jU<j<U 6CJEHOJQJ6WZ[_stBFHMNRabdhimqsw  &0:<>DLNTZ\dflv~ 6CJEH66<j<UZ@/&>@BDVXZ$$1$$/.$1$$/.$$1$$/.&1$$1$d<P LP0 1$ $.8@BDFHNPXZ`hpxz|~59@AETU&<DT\ &(,4FHL 6CJj6CJU6CJCJ5CJ<j<UOJQJ 6CJEH6OZ\fpp\$$1$$/.$$1$$/.$1$$/.$1$$/.X$$P4֞`"`"`" "$dlX$$1$L$/.$$1$$/.$$1$$/.$$1$$/.X$$P4֞L"LN`bdln0<@BJLNRTrz~   @HLNRTVZ\z CJOJQJ 6CJEH 6CJj6CJU j0JUCJ6CJTd>@Bp~llXll$$1$$/.$$1$$/.$$1$$/.X$$P4֞L"$$1$$/. BDFH|Hl$$1$$/.$$1$$/.$$1$$/.$$1$$/.D$$P4vL"<>LPllX$$1$$/.$$1$$/.$$1$$/.$$1$$/.X$$P4֞L" DfLl$$1$$/.$$1$$/.$$1$$/.$$1$$/.D$$P4vL"   $(@BDJLbdhptv   (,.LNPRTVX\^jv    ! * +       ""p"t"6<j<U6 6CJj6CJU j0JU 6CJEH CJOJQJCJ6CJLfhr L~lXll$$1$$/.$$1$$/.$$1$$/.$$1$$/.X$$P4֞L"   * ""#$%%% ))))|*,,,,,,,,,,-- - - - -"-.F.H.J.L.N.`....(/////"0.0@0^0`0j00001`1b1d1f1h1x111111Z2h2222333346 ,*+/ \   *|~~~llXll$$1$$/.$$1$$/.$$1$$/.X$$P4֞\ L"$$1$$/.  ""#$%%% )))|*|y.1$1$,1$*1$1$+1$/1$X$$P4֞\ L"$$1$$/.t""""""""""""E#F#J#K#####=$A$H$K$X$Y$u$v$z$$$$$$$$B%C%G%T%U%_%`%%%%%%%%%%%%%%&& &&&&&&&&u'v'z''''''''''(( (!(?(@( jUj%8 CJOJQJUVmH jBTU<<j<U6S@(D(W(X([(b(h(k(((((E)H)I)))))))))))))****2*4*>*@*H*J*T*V*X*Z*j*l*p*r*t*v***+ ++"+>+D+J+R+Z+`++++++,,N,O,,,,,,,,,,,,,,,,,,--- - -5OJQJ 6CJEH6j<U<Y|*,,,,,,,,,,-- - -61$d$61$$M$$P4ֈ 0h" 6$1$dd$ 6$1$d$1$ - - -.F.H.J.L.N.`....(/r|9$$P4` 0h"     61$$M$$P4ֈ 0h" - - --- -!-...... .&.2.@.B.D.L.N.b.d.f.h.j.p.v.~......................../////////$/&/(/*/,/4/6/://F/H/L/T/V/`/b/f/n/|/////////////67 j 6CJEHOJQJ6CJ$\(/////"0.0@0^0`0j0^W61$P$M$$P4ֈ 0h"      M$$P4ֈ 0h"           61$$ //////////////0000000 0"0,0.00020406080>0@0H0L0N0P0R0V0X0Z0\0^0`0r0t0v0x0z0000000000000000000000001111 1 1111 1&1*1214161<1>1D1L1P1R1\1b1f167OJQJ 6CJEH6^j00001`1b1d1f1h1x111111Z2h22223x9$$P4` 0h"61$$61$P$f1h1v1x11111111111111111111111111111111 2222 2"2&2.20282@2H2J2R2X2Z2f2v2x222222222222222222222222222223 33 3$3&3.3@3B3D3F3H3J3L3P3 6CJEH6OJQJ`P3R3T3V3X3`3b3j3p3t3v3333333333333333333333333444444 4 44444444 4"4'4(4*4-4.424647494>4?4A4D4E4I4M4N4O4P4W4X4Y4\4]4^4a4e4h4i4m4n4r4v4w4{4~444444 CJOJQJCJ$ 6CJEHOJQJ6\333344 4)4*474@4A4N4M$$P4ֈ 0h"              61$$61$$ 44 4)4*474@4A4N4O4Y4^444444444445 5 58P88X99j::;l;;2<v<>=ACC(DDD9EEEEF.GGRHHJ K%K+K2K3KDKFKnLLLLZMMM NNNNNO@SST. 6  6  6  6 +&z.@/6 KN4O4Y4^44444444444r9$$P4` 0h"61$$M$$P4ֈ 0h"       44444444444444444444444444444444444444444455555 5 555566666$6&64666Z6f6t6v66666666666777777$7*72787:7@7F7H7P7V7OJQJ 6CJEHCJ$ 6CJEH6 CJOJQJZ45 5P88X99j::;l;;2<v<>=A1$.1$1$@1$/$1$A1$ 4pM$$P4ֈ 0h"61$$V7^7h7j7p7r7z77777777777777777777777788 8&8(8D8N8P8d88889999999 9$9&9094989:9D9H9X9`9b9d9f9j9l9n9z9|999999999999999999999999999:::OJQJ 6CJEH6`:: :::":$:.:4:8:::D:H:L:N:X:\:r:::::::::::::::::::::::::::::;; ;;;;;";.;8;<;>;@;H;T;b;t;|;;;;;;;;;;;;;;;;;;;;;;;;;;;; < <<<<< 6CJEH6OJQJ`< <"<(<P<R<r<t<===>>H>L>>>>>>>>>>>S?T?U?q?w???????????????????@@@AAA&A'A*A+A,A-A.AAAAAAAAAAAHBIBMBaBbBBB8C=C~CC DDDD< 6CJEH6<j<U jU6OJQJUACC(DDD9EEEF.GGRHHJ K%K+K2K3K,$$P4Ft!61$$1$+1$\&1$\+1$&1$1$DDDXDYDZD]D^D_D`DdDpDqDvDzD{DDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEFFFFF^FfFFFFFFFZGbGdGfGnGGGGGGGGGGGGGGHH H.H6H8HDHHHHIIOJQJ6<j<U 6CJEH6XIII*I,I8I:II@IBIDI^IjIvIxIzI|I~IIIIIIIIIJ J J J9J=JVJ[JKKKK K2K3K:K;K=KDKEKLLLLL LLLLLLLL$L&L*L2L4LFLHLRLVLZL\LfLjLnLvLxLLLLLLLL 6CJEH5CJ5 jU 6CJEHOJQJ6<j<UR3KDKnLLLLZMMM NNNNtu61$d$$d%d&d'd61$$61$ddP$$d%d&d'd61$P$,$$P4Ft!61$dPP$$d%d&d'd61$PP$ LLLLLLLLLLLLLLLLLL M MMM M"M&M(M*M.M2M4M>MBMFMHMRMVMZMbMdMpMrMzMMMMMMMMMMMMMMMMMMMMMMM NNNNNNNN N"N&N(N2N6N:Nc@cXcZcdcfchcjclcrcxczccccccOJQJ 6CJEH:55:66:[cccccccccc ddd0dFdHdRdTdVdXdZd`dbd~dddddddeeeeeBeHeJeLeNeVehejeeeeeeeeeeeeeeeeeeef fffff,f.fHfJfLfXfZfvfxfzfffff jU<j<U 6CJEH6j6U 6CJEHOJQJ6PddeeeeeeeeeJfLfzffgg hthifihivi8< 51$$ XT 51$$ X $$P451$$1$$1$ffffffffffffff&g.g0g6g>gBgJgLgRgZg\g`gfghgjglgtgggggggggggggggggggggghh$h,h.h4hqTqxqqqqqqqrr(r\r^rzrrrrrs s"s$s&s(s6sssss`vwxxtyyyyyzz;zz    /6 \kll|m~mmmmmmnnXcXM$$P4ֈ8 "61$$61$d$9$$P4`8 "61$P$ lllllmm(m*m,m.m@mBmHmPmRm^mlmrmzm|m~mmmmmmmmmmmmmmmmmmmmmmmmmnnnnnnnnnnn%n&n)n-n.n7n:n>n?nDnGnKnNnPnTnUnYn\n]nangnhnmnonsnunzn{n}nnnnnnnnnnnCJ 6CJEH6OJQJ_n!n"n]nonnnnnnnno$o%o&o'o61$$61$d$9$$P4`8"61$$nnnnnnnnnnnnnnnnnnnnoooo oooooo#o&o'o(o*o/o0o2o5o6o:o>o?oAoFoGoIoLoMoQoUoVoWoXo_o`oaodoeofojokooorouoxo|ooooopppp ppp"p$p,p.p6p@pBpDpRpTpVp\p^pbpjplpnpCJ 6CJEHOJQJ6^'o(o1o2o?oHoIoVoWoaofoBpVpżjM$$P4ֈ8 "61$$61$d$9$$P4`8 " Vpbppqq&q(q>qTqxqqq0 61$d$61$dd$$d%d&d'd61$$9$$P4`8 "61$dP$$d%d&d'd61$$ npppvpxpzp|p~pppppppppppppppppppppppppppq qqqqq q"q$q&q(q*q,q8q:qs@sBsDsHsPsRsTsVs`sbsdsfshslstsvs6@CJEH6@@OJQJ 6CJEH6Z^rzrrrrrs s"s$s&s(s6ssss61$d$$d%d&d'd9$$P4`8 "61$d$$d%d&d'd61$d$61$$vszssssssssss8t>tJuRu`vavwwwwwwwwwwwwwwww4x5x{x|xxxxxx*y+y1y2yXy[ysytyuywyxyzy|y}y~yyyyyyyyyyyyyyyyzz5z9z:z;zz?zCJOJQJ B*OJQJjOJQJUCJ<j<U j0JU6Qss`vwxxtyyyzz;zz@zAzBzCz $1$ ! 1$ !$1$1$ 1$h1$/1$>z@zAzBzCz/  ?z@zCzOJQJ1 000+P9 J! " #$%\ F DdH 0 B  S A? 2l4{.1W(nHD2`!@4{.1W(n:H `xkUϝ;h-M(VQnf QH!ZԍBvM J|V ڧM yCP"SSKbU߽w;ә,3s3ssgQ?(EH}Oѳ)Ǫ33ji9qwƊy1!"k2u)s'*P(CI8T$a@*wU/<С33'fL:ǵ?On5/;nөTԃ9Lc8T,Cf\^.U/pYf[wKgv"v͔Løx8I;I (l -XAJ1'C]X?IO?]vUV" nYn"lr1]n0D6p\eo* As8aU5LؐyŠ7 b***VOUg *Y gY {GOw-,BǼdky_{\#ݩSSsӧʤ=7\wz^RF3c? gOb$VRju_J$<|9YpJ㎹т\i$)||/'*B4:Y|*yT!JC>C>"9?AcAN>hGosfL rr_y1 ȋZE@d+Umy>&יJ<+vG>_ž+4:= _<]3PY!JCn[EvT!JC>C><T !JCC`22Fy<-|Idq|[Oƿѝ 3hDl !)5~W~C>"?MG"!e^M8r È΂|0pgCC>G?2ȃw,4uىȻ _b-B[ i|ksmByӇK?XL;Q:DK݉/~nc މIg'Z"N$|qs]~~O?x5O_|6bdXqȗԄmπ`șƽ/{ _$-DdoKB  S A? 2 Hyj|X1rw#ĴF2`!Hyj|X1rw#Ĵ ?i(x]t}=ȎQ+m0b@(4{/yy).wNM> nI1d <Ą@AЙݑno}n>~A`m{^>ör: ?l?ԼԭYܴiUxOXğD=xAn|-[H=@P}'zV? 0uVӦ5`?>myOlOTg9Z=!Ҁ,uq*iDðF.#U3ytO9@ҁ!F/\HQs*W5 'I7(ǃRyNl{XW :r^!8N!V\/*:TWB- ~2\%넲qezJFdzJFdzJFdzJFdzJFdzJFdzJFdzJR) SH$:OI u@<%yJR) SH$:OI u@z df`iȞ"s)2W"s)2W"s)2W"s)2W"s)2W"s)2W"s) U¸O6_a6Hdh$pioHjF+1*<.MMk=pw7T| Vf|NėsU݌kP%‹|} W]v%t1:HtzAߴV |G1x K{n_ZS!}$u 3Lk="zi}QR7\Q+JsE[q\Q,WR7\Q+J݊R`?WR7\QVWn?WR>ԍNPZe%MQX::ˮD.VTÂy+X]19P7&dZq7\{l oj3:3-yeiL/@wEh6^%h1^^KѯOdZL4KdZlL봙iLk텿= o?ԫ`jZ;.zLx@oĔ1Z]yUR?2 p†u -klF6ʻ~v]T kUyz#0-9*?mb<(%Pvͮ|M˟|6=}Q2qW@ٕ6-Q~DCyw@˟--2OovQW|Sr7[yOd[vm?ц 8^q߁syvd>zP1 O?(#0P~&Gy#f6բ?f|++mvTO\ΚwPA s$XOw_Gy[1pE s{s7[y_2&}kn? 0GXou} ~^հW#wSXv1} )#M-SktE}/ʻ+*|wiOjOPݩ=Ofܣ; Xh[mk憍-]۪ |AVНFQ%0H 51(fQkXf iq#0bj fbrG3)PWo&5MHy-Sr P`M$1gM[(YcvT$S~=~ʱLu ^RR{?FPXT/({y[=z]Ly}B/^R>i~@2Ig򤧚' (O2)Ye|Gaz/PRS9o$+6766頋؃vi9Rvǡ׫Ep':6~ bRng`lP7ks|&=bߍwxαW&.nC^+:8mb+310Kl;dj_A^+Sx\X!qe?=  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnoprstuvwx}Root Entry= FpБ\sm.Data q WordDocument0Data<iles0My papers03+htObjectPooloherentMemorya8800?l.sm._940025544  Fl.}l.1Tablet(CompObjhObjectPool}l.}l. [4@4Normal,nOJQJkHmH >> Heading 1 $h< 5CJKH66 Heading 2 $<522 Heading 3 $6<A@<Default Paragraph Font b,bulletedl & Fh>Th(O(c,code OJQJkH(O( e,emphasis6,",i,indent h!2ib,indent bulletedh & F>Th!Biu. indent nUmberedh & F>Th.2OQ2 m,coMment6OJQJkH2>b2Title $< 5CJ$KHr u,nUmberedh & Fh>Th. !$'*-0369<?BEHKNQTWZ]    !"#$%&'() !$'*-0369<?BEHKNQTWZ]`  Sdl+*+,2$Lu}߷_g:@`)*( I <B @ # 1'  BCxDE0F: <<<(<dxx<<<@`&<B @ # 1%  BCwDE0F: ;;;;Oww;;;@`$<B  # 1#  BwCDE0F: ;;;;Oww;;;@`"<B   # 1!   BwCDE0F: <<<(<cww<<<@` r   6 r   6 r   6 r  6 r  6 r  6 r  6 r  6 r  6   r  6   r  6   r  6   r  6   r  6 r  6 r  6 r  6 r  6 r  6  r  6  r  6  r   6  r ! 6  r " 6 r # 6 r $ 6 r % 6 r & 6 r ' 6 r ( 6 r ) 6 HB * C DB S  ?  !"#$%&'*  4)f  _4(|_4'f4&fx4%f4$fa4#^f4"f4!f_4 4f4f4(4M((4(4a(4K(4(47(4(4 T 4| T 4 T 4 Th 4z T 4h   4   4k 4CT4 T4 |T/4 AT4 4 :4  4A B :4 x4k(R )4* 44)\]tu)*/05689>?DESTVWYZ\]_`bcklnoqrtuwxz{}~@oG@GTimes New Roman5Symbol3& Arial9Palatino3Times71Courier;" Helvetica"qhZ&Z&$20-Butler LampsonButler Lampson  "  FMicrosoft Word Picture MSWordDocWord.Picture.89q  FMicrosoft Word Picture MSWordDocWord.Picture.89q  FMicrosoft Word Picture MSWordDocWord.Picture.89q  FMicrosoft Word Picture MSWordDocWord.Picture.89qWordDocument SummaryInformation( DocumentSummaryInformation8_940057751  F#m. '%m.Y bjbjWW ==)^] P P P P P \ P $ ###K$M$M$M$M$M$M$$&(bq$ #i###q$K$  K$K$K$#(D K$4 B #K$K$K$K$D K$ x v]:P P E#K$ f ( y ) y y ' f ( y ' ) Y - a c t i o n X - a c t i o n s f f ()*,-/0235689;<>?ABDEGHJKMNPQSTVWYZ\]_`bcefhiklnoqrtuwxz{}~5B*CJOJQJhnH 6B*CJOJQJhnH  jUmH@)+,./124578:;=>@ACDFGIJLMOPRS      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcddSUVXY[\^_abdeghjkmnpqstvwyz|}defghijklmnopqrstuvwxyz{|}~#N N! " #!$!%Oh+'0d   , 8DLT\ssButler Lampsonutl Normal.dotsButler Lampson2tlMicrosoft Word 8.0@@D=:@D=:՜.+,D՜.+,0 hp  MSFTitlj  Title 6> _PID_GUIDAN{1FBE4029-542D-11D1-9194-00609797EA20}1TableHCompObj hObjectPool '%m. '%m.WordDocument [4@4Normal,nOJQJkHmH >> Heading 1 $h< 5CJKH66 Heading 2 $<522 Heading 3 $6<A@<Default Paragraph Font b,bulletedl & Fh>Th(O(c,code OJQJkH(O( e,emphasis6,",i,indent h!2ib,indent bulletedh & F>Th!Biu. indent nUmberedh & F>Th.2OQ2 m,coMment6OJQJkH2>b2Title $< 5CJ$KHr u,nUmberedh & Fh>Th. #&),/258?EHKNTWZ]fknqt|J      !"#*+,-./0123789:;<=ABCDEFGHIJKLPQRSTXYZ[\] #&),/258?EHKNTWZ]fknqt|  !"#$%&'()*+,-./0123456789:;<=>?@AJ  JJ x#J lI `_`/X2$CM3̾@9r$뭆  }Oi@V+^_*( h T"  c $GADH"  C G2 1Cr  6B r  6A x@ 1P3) @~  61P3! ~  6$2 P3" ~   62!F3# ~   6$2"P3$ ~   682.$(3+& ~   62Y%<3V' ~   6 $2p&P3m(  ~  6 $2'<3)  l@ \ ' ?~  6 \ Y"  ~  6 s!p#  ~  6 "$  ~  6#% ~  6$& ~  6%' V@ ?)&-'+ >  zBCDEFF((P @`-j*-'+HB  # |?)&/-*r  6= r  6< r  6; r  6: r  69 r  68 r   67 r ! 66 r " 65 r # 64 V@ \#!# &3 $ zBCPDEF(P(( @`!\#!#HB % # 1#!#V@ '}$!$ )2 ' zBCPDEF((P( @`'}$$HB (B # 1$!$r * 61 r + 60 r , 6/ r - 6. r . 6- r / 6 ,  r 0 6!+ !r 1 6"* "r 2 6#) #r 3 6$( $V@ ,p#*1# 6' 4 zBCPDEF(P(( @`0p#*1#HB 5 # 1,#0#r 7 6%& %r 8 6&% &r 9 6'$ 'r : 6(# (r ; 6)" )r < 6*! *r = 6+  +V@  &b%'+ @ > zBCDEF(P @` j*!'+HB ?B # |r!&b%*r A 6, ,r B 6- -r C 6. .r D 6/ /r E 60 0r F 61 1r G 62 2r H 63 3r I 64 4r J 65 5r K 66 6r L 67 7B M 3 1T" N c $GAH" O C G2 1r P 68 8r Q 69 9r R 6:  :r S 6;  ;r T 6<  <B U 3 1 T" V c $GA H" W C G2 1r X 6= =r Y 6> >r Z 6? ?r [ 6@ @r \ 6A Ar ] 6B BB ^ 3 1HB _ C DB S  ?  !"#$%&'()*+,-./0123456789:;<=>?@ABCDJ_f f4^ [74]! %4\ 4[s 4Zh4Y(h4Xsh4Wi 4Vi 4U P 74T 4Sh 4Reh4Qh4Phh4Oi 4Ni 4MU4L u  4K   4J g  4I  4H  4G~  4F.  4E  4D| 0  4C   4B J  4At   4@* 4=KE4< 4; " 4:(q49+(9q48(q47(Hq46L643  42m 41*404/l 4.4-&]4,hv]4+]4*h]4)C4&"r4#1  4" k 4!  4  ] 4B + 4w+ 4 4E 4* 4A4' 4":4@ZK 4  ]4m ]4 J4 J4F`aKFLORWXZ[]^`acdfgijoprsuvxy{|~$%+18<>?K@hGJ@GTimes New Roman5Symbol3& Arial9Palatino3Times71Courier;" Helvetica"qh&&$20-Butler LampsonButler LampsonY JbjbjWW ==F]   <<<<<P,<DBBBoDqDqDqDqDqDqD$BF6HbD B:BBBDoD+oDoDoDB( oD .BoDoDoDoDj  oD|0=<<BoD status = ? R e c e i v e r S e n d e r crash lose ( B ) lose ( D ) recover put ( m ) getAck ( a ) q = get ( m ) D C B get ( B ) get ( C ) get ( D ) status = OK q = status = lost q = C EFLNRTUWXZ[]^`acdfgijlmoprsuvxy{|~6B*CJ$OJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH  jUmHSFMNSTVWYZ\]_`bcefhiklnoqrtuwx      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFLMNRSTUVWXYZ[\]^_`abcdefghijkldlmnopqrstuvwxyz{|}~dxz{}~    "$&()+1368<>@BCEFJB*CJOJQJhnH 6B*CJOJQJhnH 3      "#$&'()*+123678<=>@ABCDEFGHIE     ##$'(*+2378=>ABDEGHIJN N!"#:$;%za뭆  }O( wwSummaryInformation(DocumentSummaryInformation8_940025417 FLKm.`Lm.1Table GOh+'0d   , 8DLT\ssButler Lampsonutl Normal.dotsButler Lampson2tlMicrosoft Word 8.0@@ۃ@ۃ՜.+,D՜.+,0 hp  MSFTitlj  Title 6> _PID_GUIDAN{1FBE4033-542D-11D1-9194-00609797EA20}     4 !"#$%&'()*+-./0123v6789:;<>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuyz{|}~ [4@4Normal,nOJQJkHmH >> Heading 1 $h< 5CJKH66 Heading 2 $<522 Heading 3 $6<A@<Default Paragraph Font b,bulletedl & Fh>Th(O(c,code OJQJkH(O( e,emphasis6,",i,indent h!2ib,indent bulletedh & F>Th!Biu. indent nUmberedh & F>Th.2OQ2 m,coMment6OJQJkH2>b2Title $< 5CJ$KHr u,nUmberedh & Fh>Th. &,/258;>EKNQTZ]`clqtwzF      !"#$%,-./0123459:;<=>?CDEFGKLMNPQRSTUVWXYZ[ &,/258;>EKNQTZ]`clqtwz  !"#$%&'()*+,-./0123456789:;<=>?F FF |1F rE ^]^/X2${Xl r   6= r   6< r   6; r   6: r  69 r  68 r  6 7  r  6 6  l@ m . ( 5~  6 m $h"  ~  6 !#  ~  6 "$$  ~  6#.% ~  6$& ~  6& ( V@ 5)&-+ 4  zBCDEFD''N @`,J*-+HB  # y5)&-q*r  63 r  62 r  61 r  60 r   6/ r ! 6. r " 6- r # 6, r $ 6+ r % 6* V@ e#!# () & zBCNDEF'N'' @`:!e#!#HB ' # 1#:!#V@ _$!$ +( ) zBCNDEF''N' @`_$$HB *B # 1$!$r , 6' r - 6& r . 6% r / 6$ r 0 6# r 1 6 "  r 2 6!! !r 3 6"  "r 4 6# #r 5 6$ $V@ ,y#0# 8 6 zBCNDEF'N'' @`O0y#0#HB 7 # 1,#O0#r 9 6% %r : 6& &r ; 6' 'r < 6( (r = 6) )r > 6* *r ? 6+ +B @ 3 1T" A c $GAH" B C G2 1r C 6, ,r D 6- -r E 6. .r F 6/ /r G 60 0B H 3 1 T" I c $GA H" J C G2 1 r K 61  1r L 62  2r M 63 3r N 64 4B O 3 1r P 65 5r Q 66 6r R 67 7r S 68 8x@ 1"3s) \~ T 691"3! 9~ U 6:1 3" :~ V 6;1!3# ;~ W 6<1"3$ <~ X 6=12$2-& =~ Y 6>1V%3Q' >~ Z 6?1g&3b( ?~ [ 6@1x'3s) @HB ] C DB S  ?  !"#$%&'()*+,-./0123456789:;<=>?@ABF] $ $4\jW 4S] 4R] 4Q] 4P_] 4O+j !4N 4M< W4L}84K<84J x4I x4Hj 4G 4F #4EG84DI84C84B|  x4A{  x4@4?4>|  4=  4<j4;ewj4:j49j48k45x 44 43r`42Er&41r40hrl4/bW4. W4-ZW4,hW4+$r4({ W4%q  4$m  4#  4"e  4!  4 5~ 4~ 4T~ 4u~ 4m4 g 44(  <4 <4]  4  4 U  4   4 6 4  4 U  4 4< 44[ 14[ 04D89GDHSWbhknstvwyz|} /0235689;<>?ABG@@`GF@GTimes New Roman5Symbol3& Arial9Palatino3Times71Courier;" Helvetica"qhX&X&$20-Butler LampsonButler LampsonCompObjhObjectPoolLKm.LKm.WordDocumentSummaryInformation(,Y FbjbjWW ==D]  , 2CPPPPP9A9A9ABBBBBBB$DFbC 9A[99A9A9ACBPP +PBBB9A(P PB  9ABBBB6  BP4=I: aAB drop ( B ) drop ( D ) status = ? S e n d e r crash mark ( B ) mark ( D ) recover put ( m ) getAck ( a ) q = get ( m ) D C B status = lost q = status = ? # q = D# C B# C R e c e i v e r CDHJKMNPQSWYZ\]_`bhjnpqstvwyz|}6B*CJ$OJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH  jUmHSDIJLMOPRSXY[\^_abijoprsuvxy{|      !"#$%&'()*+,-./0123456789:;<=>?@ABCDHIJKLMNOPQRSWXYZ[\]^_`abhijnopqrdrstuvwxyz{|}~d|~  "#%')*,-/0235689;<>?ABF6B*CJ$OJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH /!"$%()+,./1  !"#$%'()*+,-./0123456789:;<=>?@ABCDE=124578:;=>@ACDEFN N!E"F#\$\%za뭆  }O( wwOh+'0d   , 8DLT\ssButler Lampsonutl Normal.dotsButler Lampson2tlMicrosoft Word 8.0@@7:@7:DocumentSummaryInformation85_940057783' FZm.P]m.1Table=qCompObjh՜.+,D՜.+,0 hp  MSFTitlj  Title 6> _PID_GUIDAN{1FBE4024-542D-11D1-9194-00609797EA20} [4@4Normal,nOJQJkHmH >> Heading 1 $h< 5CJKH66 Heading 2 $<522 Heading 3 $6<A@<Default Paragraph Font b,bulletedl & Fh>Th(O(c,code OJQJkH(O( e,emphasis6,",i,indent h!2ib,indent bulletedh & F>Th!Biu. indent nUmberedh & F>Th.2OQ2 m,coMment6OJQJkH2>b2Title $< 5CJ$KHr u,nUmberedh & Fh>Th. !$'*-04:=AFJNRX[^adjmqy|  #&.27:=BEHKRU\_jou}\!"#$%&'()*+,-./0123456789:;<=?@ABCDEFGHIKLMNOPQRSTUVWYZ[\]^_`abcdefhistuvwxyz{|~ !$'*-04:=AFJNRX[^adjmqy|  #&.27:=BEHKRU\_jou}  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijkl\ ,  \ S\ (d(\ dS[ O2$FTÚXAݤ(yB r$뭆  }Oi,r$_fp<CPi,r$-8VX*0t%i,@JED(  T"  c $G0*AH"  C G0*1T"  c $G0*AH"  C G0*1T"  c $G0*AH"  C G0*1T   c $AT   c $AT   c $AT   c $A~T   c $A}T  c $A|T  c $A{T  c $Azx@ 3D5& y~  63D5 ~  6405 ~  64105.! ~  64I 05F" ~  6,4!5# ~  64"05$ ~  64#05% ~  64$5& l@ S%  x~  6 S P  ~  6    ~  6  !  ~  6  "  ~  6 "#  ~  6#% r ! 6w r " 6v r # 6u r $ 6t r % 6s r & 6r r ' 6q r ( 6p r ) 6o r * 6n r + 6m r , 6l r - 6k r . 6j r / 6i r 0 6h r 1 6g r 2 6 f  r 3 6!e !r 4 6"d "r 5 6#c #r 6 6$b $r 7 6%a %r 8 6&` &r 9 6'_ 'r : 6(^ (r ; 6)] )r < 6*\ *r = 6+[ +H" > C GZr ? 6,Y ,r @ 6-X -r A 6.W .r B 6/V /r C 60U 0r D 61T 1r E 62S 2r F 63R 3r G 64Q 4r H 65P 5r I 66O 6H" J C GNr K 67M 7r L 68L 8r M 69K 9r N 6:J :r O 6;I ;r P 6<H <r Q 6=G =r R 6>F >r S 6?E ?r T 6@D @r U 6AC Ar V 6BB Br W 6CA CH" X C G@r Y 6D? Dr Z 6E> Er [ 6F= Fr \ 6G< Gr ] 6H; Hr ^ 6I: Ir _ 6J9 Jr ` 6K8 Kr a 6L7 Lr b 6M6 Mr c 6N5 Nr d 6O4 Or e 6P3 Pr f 6Q2 QH" g C G1r h 6R0 Rr i 6S/ SV@ ",$0+) l. j zBCDEFF((P @`/m(0+)HB k # |",$0(V@ &$s') o- m zBwCDEF<<w< @`&(s')HB n # 8c8'$9'(V@ $"+) r, p zBCDEF(P @`m(+)HB qB # |$"(r s 6T+ Tr t 6U* Ur u 6V) Vr v 6W( Wr w 6X' Xr x 6Y& Yr y 6Z% Zr z 6[$ [r { 6\# \r | 6]" ]<B }@ # !r ~ 6^  ^r  6_ _r  6` `r  6a ar  6b br  6c cr  6d dB  3 1r  6e er  6f fr  6g gB  3 1B  3 1B  3 1<B @ # B2  3 jJB2  3 jJr  6h hB2  3 jJr  6i  iB2  3 jJ r  6j  jB2  3 jJ r  6k  kB2  3 jJT"  c $G0*AH"  C G0*1r  6l lB2  3 jJr  6m mB2  3 jJ<B @ # HB  C DB S  ?  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~\( _H _4|D4944V 4 444 K4%in41 K4%n4 K4%] n4s K4|%Xn4 q K4 K44&, 4 , r4, 4F  4  4 7 42]4L ; 4L ; 4mL ; 4tr  4.  4r  4~&4}U4| u1 4{  4zO 4yE 4xS aB 4w" Vk 4v " 7 k 4u " k 4t " G k 4sq "  k 4r>u 4o$u 4lJu 4i@4hP4g:  4fk4e4dJ4c4b}4ay4`*4_z4^u4] W4\fj4[iW4Z.2@4Y`<P4X J 4WJ4V4U]4T \4S  4R  4Q  4Puo4O[W4N 1 W4M%Jn4L!4K'4J4I< )4H4G84F4Eh4Du4C W4BTX4A|XW4@F4?W4> 4=64<n4;w4:49D 48  47UE/46}Y45  /44  43*/4241040F4/ 4.l4-:4,64+ /4*N z4) 4( /4'R1/4&4%4$*4# 4"4!4 =4Zlr 4 14 &14t 14 W74 4  &4 t4 W4r 44r 44#4#4*4*4]:;BH`ckly(.]@,G\@GTimes New Roman5Symbol3& Arial9Palatino3Times71Courier;" Helvetica"qh&&$20-Butler LampsonButler LampsonObjectPool<\m.<\m.WordDocumentxY-SummaryInformation(DocumentSummaryInformation86 Y \bjbjWW Y-==]HHHHH$lDHmkkkmmmmmmm$rofqbmk'[kkkmmKFmmmk@0 m,:kmmmmPm,P HH[kDm R e c e i v e r S e n d e r g s = last s = msg = sr = rs = g r = last r = mark = 3 C 2 + q = C status = ? 3 C 3 C 3 + q = status = OK 3 OK 3 4 5 nil 2 + q = C # status = lost 3 C 3 C nil # q = C # status = ? # 3 C get ( C ) crash s crash r ; recover nil lost shrink r (3) ( after strikeout ) ( before strikeout ) 4 4 5 3 4 5 4 4 3 4 5  B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH 6B*CJOJQJhnH 6B*CJ$OJQJhnH  jUmHI      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdddefghijklmnopqrstuvwxyz{|}~d      !#$%&'()*+,-./0123456789:;<=@ABHIJLMNPQRSd    !$%'(   !#%&()+,./124578:;=@BHJLNPRSUWY^`cefhiklnqstvwy6B*CJOJQJhnH 6B*CJOJQJhnH 5B*CJOJQJhnH 56B*CJOJQJhnH B*CJOJQJhnH K(*+-.0134679:<=ABIJMNQRTUXY_`dSTUWXY^_`cdefghijklmnqrstuvwxyddeghjkmnrsuvxy   "#%&(8:;=>@DFKMNPQSB*CJOJQJhnH 6B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH 5B*CJOJQJhnH 56B*CJOJQJhnH F  !"$%'(    !"#$%&'(89:;<=>?@DEFKLMNOPQRSXYZ[A(9:<=?@EFLMOPRSYZ[\SX\B*CJOJQJhnH N N!"#$%za뭆  }O( wwza_fp<CP( za-8VX*0t%( wwwwOh+'0d   , 8DLT\ssButler Lampsonutl Normal.dotsButler Lampson2tlMicrosoft Word 8.0@@ۃ@ۃ՜.+,D՜.+,0 hp  MSFTitlj  Title 6> _PID_GUIDAN{1FBE403C-542D-11D1-9194-00609797EA20}_940057799" F~km.mm.1Table`CompObj!$hObjectPoolmm.mm. [4@4Normal,nOJQJkHmH >> Heading 1 $h< 5CJKH66 Heading 2 $<522 Heading 3 $6<A@<Default Paragraph Font b,bulletedl & Fh>Th(O(c,code OJQJkH(O( e,emphasis6,",i,indent h!2ib,indent bulletedh & F>Th!Biu. indent nUmberedh & F>Th.2OQ2 m,coMment6OJQJkH2>b2Title $< 5CJ$KHr u,nUmberedh & Fh>Th. $),/258>AFILOUX^adgjpsvy| "%(-25:=@FIQZakr{.   %&()+,345678?@JKLMNOPQRSTUVWXYZ[\]^_`abcdefgijklmnvwxyz{|}~ $),/258>AFILOUX^adgjpsvy| "%(-25:=@FIQZakr{  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcd. *  .y. +W,. dN- _2$ dz/f\=X r$#+ 'w{i *r$P%Hsp羙Ьi*r$-8VX*0t%i*r$_fp<CPiY+@V>V( }0 N  S AB  3 jJN  S AB  3 8cN  S AT  c $Ar   6 H"   C G;r   6~ r   6} H"   C G;|r  6{ r  6z N  S AyN  S AxN  S AwB  3 jJvN  S AuB  3 jJtN  S AsB  3 jJrT  c $AqH"  C G(pr  6o r  6n r  6m H"  C G(lr  6 k  r  6 j  N   S AiB ! 3 8chN " S AgB # 3 8cfH" $ C Ger % 6 d  r & 6 c  H" ' C Gbr ( 6 a  r ) 6` H" * C G_r + 6^ r , 6] V@ -"." /\ - zBPCDEF((P( @`-"."HB . # -"-"V@ c,',c( 2[ 0 zBCxDEF<x<< @`c,',c(HB 1 # c,'(d,((r 3 6Z r 4 6Y r 5 6X r 6 6W r 7 6V r 8 6U V@  *h/*/ ;T 9 zBCFDEFF @` *h/*/HB : # */*/V@ *X0*0 >S < zBCPDEF((P( @`*X0*0HB = # *0*0r ? 6R r @ 6Q V@ !B'>"' CP A zBxCDEF<<x< @`!B'>"'HB B # "B'"C'V@ !h/g"/ FO D zBCFDEFF @`!h/f"/HB E # f"/g"/V@ X0P0 IN G zBCPDEF((P( @`X0F0HB HB # F0P0r J 6M r K 6L r L 6K r M 6J r N 6I r O 6H r P 6G r Q 6 F  r R 6!E !r S 6"D "r T 6#C #r U 6$B $r V 6%A %r W 6&@ &r X 6'? 'r Y 6(> (r Z 6)= )r [ 6*< *r \ 6+; +r ] 6,: ,r ^ 6-9 -r _ 6.8 .x@ 3<(>5U2 h7~ ` 6/3<(>59* /~ a 603{)*5x+ 0~ b 613**5, 1~ c 623+*5- 2~ d 63&4,5. 3~ e 643.*5/ 4~ f 653A/*5>1 5~ g 663X05U2 6l@ g)0 o6~ i 67g)+ 7~ j 68g*, 8~ k 69gZ+W- 9~ l 6:gr,o. :~ m 6;g-/ ;~ n 6<.0 <V@ &'G'c( r5 p zBCxDEF<x<< @`&'G'c(HB qB # &'(&((V@ j###o# u4 s zBCPDEF((P( @`j###o#HB t # #G##H#r v 6=3 =r w 6>2 >r x 6?1 ?r y 6@0 @r z 6A/ Ar { 6B. Br | 6C- Cr } 6D, Dr ~ 6E+ Er  6F* Fr  6G) Gr  6H( Hr  6I' Ir  6J& Jr  6K% Kr  6L$ Lr  6M# Mr  6N" Nr  6O! Or  6P  Pr  6Q Qr  6R Rr  6S Sr  6T TN  S AN  S Ar  6U UV@  (Y!q)   zBCxDEF<x<< @` (Y!q)HB B #  5) 6)V@ &(G'q)   zBCxDEF<x<< @`&(G'q)HB  # &5)&6)r  6V Vr  6W Wr  6X Xr  6Y YN  S AV@ 2(A3q)   zBCxDEF<x<< @`2(A3q)HB B # 25)26)N  S AB  3 jJF@ $!$#   zBPCxDEF(x(P(x @`$"$#HB  # jJ$!$!HB  # jJ$"$"HB  # jJ$:"$N"HB  # jJ$k"$"@ &!&    zBwCPDEFw(P(w( @` !&!&HB  # jJ&&HB  # jJ &- &HB  # jJK &_ &HB  # jJ} & &HB  # jJ & &HB  # jJ & &r  6Z  Zr  6[  [r  6\  \r  6]  ]r  6^ ^r  6_ _r  6` `r  6a ar  6b bV@ -#.s'   zBFCDEF((F( @`-&.s'HB  # -#-&V@ !) "/   zBFCDEF((F( @`!. "/HB  # ")".n@  " Z  S A ax Z  S A j6!~  6c  c~  6d e! d`  c $A !?"~  6e!" e`  c $A!?"HB  C DB S  ?  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~.[ B{ B4\4 ;X4+E 4)g\4(gk4P48g{ 4g4P4iY4QiY4iY4j  4  4 P4 U4 \C 4l4qim4<-4i! m4`-4 b C 4 tC 4g p 44p4k4b p48+  4+ t 4  4 ` 4 $ 4  4tp4$p4t^N4B^N4^N4^KN4  p46  p4r ^ N4~@ ^ N4} ^ N4| ^J N4{ +   4z +  4y^ 4x, 4w r 4v 5 4u  A4r b 5 4o p4h Y'4_H)4^&)4])4\90)4[ D 4Z  4Y 7 4X9  4W0 E 4V E 4U XE 4T9 :E 4S  4R h 4Qn " 4P(  4O?  4N24M4LP4KV4Jm4I*kz4F:4C Y 4@ q 4?Lc 4>1*z4;':48b  47  46T  453  44 a 43<E  42~ 5 4/5o4,?4+o4*`z4)O4(o4'` 4&k4%(4$z4#O 4"O 4! + 4  + 4#'4s44^4 4 &4 4g P64 &54 +:45g 40l 45&40+4/ C 4q C 4U  4_  4 (  4  n^4  4  tc4  - 4g 644 C 41 ~+ 41 ~+ 4D4I4#)@Aghsv{|/ #)./78:;=>@ACDFGIJOPRSUVXY[\^bghmnsv{| "*/@LG.@GTimes New Roman5Symbol3& Arial9Palatino3Times71Courier;" Helvetica"qh&&$20-Butler LampsonButler Lampson  FMicrosoft Word Picture MSWordDocWord.Picture.89q  FMicrosoft Word Picture MSWordDocWord.Picture.89q  FMicrosoft Word Picture MSWordDocWord.Picture.89q  FMicrosoft Word Picture MSWordDocWord.Picture.89qWordDocument#%+SummaryInformation(&DocumentSummaryInformation8_940057814 .) FUm.Pbm.Y .bjbjWW +==](((((DD(rW{W{W{7999999$ b]W{kW{W{W{]7W777W{` 7 W{77777,G((-| 7 sr 3 A 5 B 5 OK rs 4 lost new r g s g r last r get ( m ) last s grow r ( i ) grow s ( i ) choose ( i ) put ( m ) getAck ( a ) R e c e i v e r S e n d e r send ( i , m ) rcv ( i , a ) send ( i , a ) rcv ( i , m ) msg rec s rec r [ copy ] Sender actions state Receiver state actions messages / acks identifiers channels B*CJOJQJhnH 6B*CJOJQJhnH 56B*CJOJQJhnH 6B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH 56B*CJOJQJhnH  jUmH=      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdddefghijklmnopqrstuvwxyz{|}~d     !"#)*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNd   "#*+    !#)+,./124578:;=>@ACDFGIJLMOPRSUVXY[\^bdeghjkmnpqsvxyB*CJOJQJhnH 6B*CJ$OJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH L+-.0134679:<=?@BCEFHIKLNOQRTUWNOPQRSTUVWXYZ[\]^bcdefghijklmnopqrsvwxyz{|}~dWXZ[]^cdfgijlmoprswxz{}~y{|~ "*.5B*CJOJQJhnH 56B*CJOJQJhnH 56B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH C!"+, !"*+,-(,-.N N!"#.$/%za#+ 'w{( wwzaP%Hsp羙Ь( 33za-8VX*0t%( wwwwza_fp<CP(     !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Oh+'0d   , 8DLT\ssButler Lampsonutl Normal.dotsButler Lampson2tlMicrosoft Word 8.0@@ۃ@ۃ՜.+,D՜.+,0 hp  MSFTitlj  Title 6> _PID_GUIDAN{1FBE4041-542D-11D1-9194-00609797EA20}1Table CompObj(+ hObjectPoolۀm.ۀm.WordDocument*,A [4@4Normal,nOJQJkHmH >> Heading 1 $h< 5CJKH66 Heading 2 $<522 Heading 3 $6<A@<Default Paragraph Font b,bulletedl & Fh>Th(O(c,code OJQJkH(O( e,emphasis6,",i,indent h!2ib,indent bulletedh & F>Th!Biu. indent nUmberedh & F>Th.2OQ2 m,coMment6OJQJkH2>b2Title $< 5CJ$KHr u,nUmberedh & Fh>Th. "%(+147<?BEKNQWZ]`ciloru} #&),/28;>ADGLORUX[cfilorz}  &,037:>AEKNRX[^adgjmsx{~"#%&()19:<=>?@GHMXYZ[\]^_`abcdefghijklmoqstvwxyz{|}~0123456789:;<=>?@ABCDEFGHIJKLMNOPQ\]abcde "%(+147<?BEKNQWZ]`ciloru} #&),/28;>ADGLORUX[cfilorz}  &,037:>AEKNRX[^adgjmsx{~  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~@  mXZ^ 4kTp"  d6:  utu_2$ۓip}r$P%Hsp羙Ьi @r$#+ 'w{i @r$_fp<CPi@r$-8VX*0t%iYA@st@( 5% n@ Q'3' Z  S Aw(Q'3'Z  S As!Q''%'Z  S AQ':'V@ n(!* .q*    zBCPDEF(P(( @`-!* .q*HB  # n(I*-J*N   S AB   3 jJN   S AB   3 jJN  S AB  3 jJN  S AB  3 jJT  c $AH"  C G(r  6 r  6 r  6 H"  C G(r  6 r  6 <B  # N  S AB  3 8cN  S AB  3 8cN  S AB   3 8cH" ! C Gr " 6 r # 6 H" $ C Gr % 6 r & 6   H" ' C Gr ( 6   r ) 6   V@ ",T r,  , * zBPCDEF((P( @`",T r, HB + # J,T K,U V@ -/&.& / - zBCxDEF<x<< @`-/&.&HB . # -k&-l&B2 0 3 r 1 6   <B 2 # V@ /&/' 5 3 zBPCDEF((P( @`/&/'HB 4 # /&/&V@ ,(^,E) 8 6 zBPCDEF((P( @`,(^,E)HB 7 # 6,(7,(r 9 6   r : 6 B2 ; 3 r < 6 r = 6 r > 6 r ? 6 r @ 6 V@ n(.(. C A zBCPDEF((P( @`n(.(.HB B # (.(.V@ J,% .% F D zBCPDEF(P(( @`-% .%HB E # J,%-%r G 6 r H 6 V@  % & K I zBxCDEF<<x< @` % &HB J # [ %\ %B2 L 3 r M 6 V@ .. P N zBCPDEF((P( @`..HB OB # ..<B Q@ # V@ r-. T R zBPCDEF((P( @`-.HB S # r--V@  ,v"@- W U zBCPDEF((P( @` ,!@-HB VB # !-v"-r X 6 r Y 6 r Z 6 r [ 6 r \ 6 r ] 6 r ^ 6 r _ 6 r ` 6 r a 6   r b 6! !r c 6" "r d 6# #r e 6$ $r f 6% %r g 6& &r h 6' 'r i 6( (r j 6) )r k 6* *r l 6+ +r m 6, ,H" n C Gr o 6- -<B p # r q 6. .H r C r s 6/ /r t 60 0H" u C Gr v 61 1r w 62 2x@ 5&m60 ~ x 635&m6( 3~ y 6485'c6) 4~ z 6585(c6* 5~ { 6685)c6+ 6~ | 67858+(66- 7~ } 6885F,c6D. 8~ ~ 6985-c6/ 9~  6:85.O60 :l@ {'H/ ~  6;{') ;~  6<{(* <~  6={)+ =~  6>{+- >~  6?{2,0. ?~  6@{J-H/ @V@ '%/&%&   zBCxDEF<x<< @`'%/&%&HB B # '%k&1%l&T  c $Ar  6A AH"  C G;r  6B Br  6C C@ e'\&P(K( T"  C G;e'\&(<(~  6D'&2(' D~  6E'['P(K( E<B  # V@ w%%h    zBPCDEF((P( @`w%%h HB  # %%<B @ # H  C r  6F Fr  6G Gr  6H Hr  6I Ir  6J Jr  6K Kr  6L Lr  6M Mr  6N Nr  6O Or  6P Pr  6Q Qr  6R Rr  6S Sr  6T Tr  6U Ur  6V Vr  6W Wr  6X Xr  6Y Yr  6Z Zr  6[ [r  6\ \l@ (S%+' ~~  6](S%*C& ]~  6^)S%C*C& ^~  6_)S%*C& _~  6`/*S%*C& `~  6a)&*' a~  6b*&+' bV@ -m) .) }  zBCPDEF(P(( @`-m) .)HB  # -)-)N  S A|N  S A{H  C zH  C yN@  xHB B # @bL hd hd  zBPCDEF((P( @`hdHB  # @ADL d dHB  # deHB  # HB  # rV@ /"N0# w  zBPCDEF((P( @`/j#N0#HB  # &0"'0j#8@ r/#0n$ vHB  # r/#0#HB  # /1$02$HB  # /m$X0n$r  6cu cr  6dt dr  6es er  6fr fr  6gq g   BmCDEF;m;; @`pr  6ho h<B  # nr  6im ir  6jl jr  6kk kr  6lj lr  6mi mr  6nh nr  6og or  6pf pr  6qe qH  C dr  6rc rV@ ='' b  zBCxDEF<x<< @`=''HB B # y'&z'V@ %='%' a  zBCxDEF<x<< @`%='%'HB  # %y'%z'H  C `<B  # _V@ ,(/U( ^  zBCPDEF((P( @`,(-U(HB B # --(/.(r  6s] sr  6t\ tr  6u[ ur  6vZ vN  S AYB  3 jJXN  S AW<B  # VN  S AUV@ 3='f4' T  zBCxDEF<x<< @`3='f4'HB B # 3y'3z'N  S ASB  3 jJRH  C QN@ !# PHB B # @!"bL "hB# "hB#  zBPCDEF((P( @`"hB#HB  # @"A"DL B## B##HB  # B#C#HB  # ~##HB  # #r#F@ # R#X!  O  zBPCxDEF(x(P(x @`# R#X!HB  # jJ*# +#, HB  # jJ*#J +#^ HB  # jJ*#| +# HB   # jJ*# +# @ @$+% N   zBxCPDEFx(P(x( @`b$+%HB   # jJ@%T%HB   # jJr%%HB  # jJ%%HB  # jJ%%HB  # jJ%%HB  # jJ:%N%r  6wM wr  6xL xr  6yK yr  6zJ zr  6{I {r  6|H |r  6}G }r  6~F ~r  6E r  6D r  6C <B  # Bn@ .-0. !A  BCDEFA<2 @`.-/.Z   S A/-0&.<B " # @V@ 0l.D04/ %? # zB<CFDEFF<F @`0.D04/HB $ # &0l.'0.<B & # >V@ /)N0- )= ' zBPCDEF((P( @`/-N0-HB ( # &0)'0-<B * # <n@ ..0/ -; + BCDEFA2<2 @`..//Z , S A/R/0/H . C :H / C 9r 0 68 r 1 67 r 2 66 r 3 65 r 4 64 r 5 63 r 6 62 r 7 61 r 8 60 r 9 6/ r : 6. r ; 6- r < 6, r = 6+ r > 6* r ? 6) r @ 6( r A 6' r B 6& r C 6% r D 6$ r E 6# r F 6" r G 6! r H 6  r I 6 r J 6 r K 6 r L 6 r M 6 r N 6 r O 6 r P 6 r Q 6 B R 3 <B S # <B T # <B U # <B V # H W C H X C V@ W-1/+2 [ Y zBCPDEF((P( @`W-1-+2HB ZB # -2/2r \ 6 r ] 6  V@ /%3N04 `  ^ zBPCDEF(P(( @`/%3N03HB _ # &03'04r a 6  r b 6  r c 6  r d 6 r e 6 V@ /B0N01 h f zBPCDEF((P( @`/0N01HB g # &0B0'00<B i@ # <B j@ # V@ !N!O"! m k zBCxDEF<x<< @`!N!N"!HB l # N"!O"!V@  -t!. p n zBCxDEF<x<< @` -s!.HB o # s!-t!-V@ d(-(. s q zBCxDEF<x<< @`d(-(.HB r # (-(-HB t C DB S  ?  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~t 4sq4pq 4m\ % 4jX4i4h4e&,z4dx4cr:x4b6x4a=hx4`4]*v4\X4[4X94W4Ves4Ue&s'4Te4S&e4RaN4Qm !4P;'4Oi 4Nf 4M*'4L p4K  4J& 4I l4H'04Gi  4F) 4E[gK4DYy74CU[K4B[K4AfGLK4@ y74?[RK4>D[K4=GK4<i[K4;)[K4::#49i#w48#hV47hJ46P45hH 44h043P42+41 {40 (4/H4.4-uo4* 4){4&k4%C 4"}4!4oQ}R44qa4} #  4 #  4 # U  4 A  4#  4Y Q A 4 Q A 4 Q A 4Q A 4 s 4   /4& 4 G 4 4v4 /{4s  4g4  4V  4<47!4Q44N44) e,4eP f4 + 4  8 4 K 4K 4 4L  4A 4lA 4r&A 4,) 4A 4vY40Y46Y4Y4Je44ly4U A 4A 4sA 4z) 4A 4  sE 4e 4&4S4jH44C8 4D4t* Z 4S44S4"4h4+4f  4  4R  4  4 f 4 * 4z j Z 4 j Z 4> *  4 *  4 * R  4 *   4bR4bR4ZbR4tbR4 P 4z .'4qC4 y` ?4\ y8 z43 "4 n4 d4 J4 P 4= 4  L ~ 4x ]4` s4wH 4v-4ua 24t]O4ssHc4rX 4q M4p-4oM-4nJ24m&I4lI4khI4jI4i" < 4hd r< 4g < 4f d< 4e: v 4d: 0 4c6:  4b:  4a  54` I 54_O  54^  4] m 54\954[54ZW54Y] 4Xt54W 4TeIa4QIAJ4PuC4M4LF4K\ 0 4H f  4GA  ( 4Ff  4Cu4@_ < 4? < 4>R < 4=0 < 4<:4;4:Z49 4845=  42  e 41R  409  4/" ~ 4,+ 4) 4(o4'O4&04%4$a 4#64"-4!O24  &\ 4 &\ 4f  t 4f  t 4 "t 4 "t 4 B  44+WG4444 4 SxC4o &|4=  444 4~ 4  = 4  {B 4 4 {4 H4( } 4 ]^op!&';<GJOPij}~,-sv  "#%&+/127:?@EIKLQUWX]^cgijopu{  !&',-26;<ABGJOPUV[acdijrx}~  $,-78@4G(`@``GTimes New Roman5Symbol3& Arial9Palatino3Times71Courier;" Helvetica"qh&&$0-Butler LampsonButler Lampson=Y  bjbjWW A==]4dmmm$b-mmmmϠm<bmtD$;  5 OK rs 4 lost new r g s g r = last r = get ( m ) last s = grow r ( i ) grow s ( i ) choose ( i ) put ( m ) getAck ( a ) I rec r new s R e c e i v e r S e n d e r sr 3 A 5 B Y rcv ( i , *) send ( i , m ) rcv ( i , a ) send ( i , a ) rcv ( i , m ) shrink r ( i ) X choose ( i ) shrink s ( i ) msg rec s rec r msg nil , last s = nil OK lost [ copy ] Sender actions state Receiver state actions or mark X = i ( g s { last s }) Y = g s g r or rec r # + put ( m ) mark     "#%&()+/12457:<=?@BCEIKLNOQUWXZ[]^`acgijlm6B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH 56B*CJOJQJhnH 56B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH  jUmH=   !"$%'(*+0134      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdddefghijklmnopqrstuvwxyz{|}~d      !"#$%&'()*+/0123456d467;<>?ABDEJKMNPQVWYZ\]_`bchik67:;<=>?@ABCDEIJKLMNOPQUVWXYZ[\]^_`abcghijklmnopqrstu{|}~ dklnoqrtu|}moprsu{}~  "&(,.248:>@DFJLPRVX6B*CJ$OJQJhnH 56B*CJOJQJhnH 56B*CJOJQJhnH 6B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH : $&*,0268<>BDHJNPT "$&(*,.02468:<>@BDFHJLNPRTVXZ\^`bdfhjlnprtvxz~dTVZ\`bfhlnrtxzX\^bdhjnptvz~  "&(,.248:>DHJNPTVZB*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH 56B*CJOJQJhnH 6B*CJ$OJQJhnH K    "$&(*,.02468:<>DFHJLNPRTVXZ\^`bdfrtvxz|~d $&*,0268<>FHLNRTXZ^`dftvz|Z\`bfrvx|~"&(,48:>@DFJRVZ^6B*CJOJQJhnH 56B*CJOJQJhnH 56B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH @"$&(*,468:<>@BDFHJRTVZ\^fhjlnpxz|~           " $ ( * , . 0 2 6 8 : d$&*,68<>BDHJTV\^hjnp^fjlpx|~       $ ( , . 2 6 : B F H L P T \ ` b f h l n r t x z ~ B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH 5B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH Gpz|        " " $ * , 0 2 8 : D F J L R T ^ ` d f j l p r v x | ~ : B D F H J L P R T \ ^ ` b d f h j l n p r t v x z | ~ C  56B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH  N N!g"g#)$)%zaP%Hsp羙Ь( 33za#+ 'w{( wwza_fp<CP( za-8VX*0t%( wwwwSummaryInformation(-DocumentSummaryInformation8_94005783750 Fٝm.m.1TableOh+'0d   , 8DLT\ssButler Lampsonutl Normal.dotsButler Lampson2tlMicrosoft Word 8.0@F#@`@`՜.+,D՜.+,0 hp  MSFTitlj  Title 6> _PID_GUIDAN{1FBE4046-542D-11D1-9194-00609797EA20}ްA0>\~0ӟ(IgMA)TqQ^kbTHG$7sLU9rVRs %+/G>ZGγ=q"dVi4\'>qixC?01G`@ُof}cPG`SEoL#Ơj.SR[YPAks"-obk~3VK9o+qr@oar ^s%+4`w0Y{Tk qoW F86~b83yq)(la ٯ89Xg qʴq|pT`BIƹ8&o`f{;o4pd"^iP ȮNWl\WFAU!*\?VգBH2\ r]T5ISu\+GƕR))R))R))R))R))R))R))R)iV)iV)iV)iV)iV)iV)iV)=M*U4\O+\O+\O+\O+\O+\O+\OXU=cb6p;d6| w.9 Uwñt6,up"N զUZ%=MVFici*]`ѺHv3sAitim$ߊV(WrE(Wj\8(W +sE(WjqEZ\Q+sE(W++Ղr5\Q+sEZq\D6ԯ>VEAky~{=/Zw^j=l#a;y@V_՗<fje8Lt9a}MZ%=UՇ834]!%Z}(Rvҫ״6l2/m/w}e-6_t)fP}Ӊ&}eDqO2K@0ߦthr h/7Zy& ;!0_&cmҷU ۪f{.g@OHk;_rM9+O_7Vw +OKtU \ ~BXL )zF!A\P5M!*\?˞(WJzJJzJJzJJzJJzJJzJJzJJzJZzJZzJZzJZzJZzJZzJZC9 Sdp=E Sdp=E Sdp=E Sdp=E Sdp=E SrBp=%eOȃOP+OmNLѷ ܨ?Gwk]d`v*kFV}Sstj3ܘD_5&}F}K8=l\%G l;@]E0v}sUNvZyi]we\?Wr5\QVWj\?Wr⸢\-X(Wj\?WjrE(Wj\8O"W 婡[+OO[yZv2UV_X):_amZ}AgVS z^Ik*QE7*KFZn3SCAW`juHV%c;yh'OWn>L31^V=n TcWlb1B;=}]Ɩ2V~u&vY4C`?ݐMZ2t(gb?,SR^̬I:ʘ "JV"&rSsέy+g[ȩ_hODd5B  S A? 2nOx̟KJ2`!BOx̟K4  <'x]{՝>>oJ`` (Xkd4hX0ܡ(JP-[ & Ijٲ@Ɣq-S0D8^Lyܾ/=th{_;>ߜ#!:j!B o8,WoWϒ F7XX~yX >=Ļ>>b4;K [t@n浫D(#hFq{ GHn(B!3Lb;!T;XI D괱X㲝+=Eb|4>sq=Z.ed[SAEb,#B*Eoѯs}25 A\Y\A7 r j qMzc9u>g :3Xs|`9u>g :3Tjb+.3u^qLW\f2S:ye+.3u^qLW\fPIu^qlw{lv$DvI ˟N~?O$̏GoÍĕR!2JWJݽ\+us^<.ppL/h  `F\,bT;EzvG KR{gQu;~(Tn:^{g3wv~Ozg|r, H6IlWҋwwHl?*~/q_~'zyhEH߯`93jxCEY,`7NEXi&ֽ >a 0Pb$p,I-:{Tce:|-Z.#8T3-RE,T9޺գLŔX-YGXϴTsgo'?ԭ_%[ ˔JUdQ/m_5M@(l~?pLiۯ )MgW,kDYbWXkʠ|DdOKgl%dgLaΟ1T1VWWȘj]ebj=W2SЛڐ+Laum ʯe5 ) T=\aC%?T i^džeƄ缒?_|``% jLx+X9|? ?$&J]ļkM )U[C+Lo-|kY; V3)F)år嫛ꚲ'̀L?΂~nƄFyyXTURy_ xZ[Ţj\UL@5N 7,-4͇ ]e:|Dbϟw]q<= g/ Ϭy3{391q> J(H2tM"ʯ!Gr|9"1ʗbr*/@^G'C?O~'1OP~HRtC"//y$X%Ą+KEe z-DN W~cEfW:- =+mP vlo[}Xˆ7;>aw*P χ*9`ңl"]j?c5;;GGۥ#\tyn= (W(^BV2[CNbΔKYi2p՘߫QJ\l5ɲ%aOspS& ޲Rr~^qԫA|?9x݇^- C[|@ 꿖)A>(S/D}:LMד9qx<,:"/43jwf?jfJv<#4kLQ^7Aļnªlf$m  /0+,V+GoǗ Q>Jbd--P%SLPyr9)gJ(?QOИhW.y];5^r\YǏAP܏#PQ# b'[@Ք L)|JrZYE%/"e4&p-~UǻWfuW'4&|4(y8;'1&;?C+LQ+Q{;c*~Tbdg,b{@ %K(_\F#} {'FAc([yAsRGz EHW>'^W{UO'@]ux<]JsY e WAv\fkA3u ח2,dWcr y`w y`w y`w y`w y`w y`w yPzPW\f2S:ye+.3u^qLW\f2S:y7PE;Q9|gpٕx-׳xOV8s쁥wB`ʧagbo6N9E)cN{fh'{ò޷Bll{0st=EײmYVg)d}ݲrWJ\+s]|ԿϕwR.W%ÕwR.>WJ\O+fyv RZ ɂf cpM8UIwl3`x7s^X}'ĺ;V{ܱYͷiwYX wKwl?,ݱg;64ˊ lr߆P|>pFy5"bL4. aYS5Jc"ͪ=SS7cd?]a#Cvz^F%'3x2BY(ߗ2(RRE˜Gg!FbMF*u̧}O&'OWiw;~`YVe ׃~i\2渮3ȵ s: r]iK :::::::'3u^qLW\f2S:ye+.3u^qLW\f2S|$52fkW|=X?Nx+9;! z sl/m±y:ǜslv8=N7t9۞sֲ&pZinY;6s]|ԿϕwR.>WJ\+q]2\+s]|Կ%ķ}8O;βCv;YcucVp1rlAGs_^=tra wCll Qg={YV;.'|4~[9kLy76nb>4>/I5&|y'Xr{Z[1ʱ3V#kUYQ80$~\blU+Vlf-!ʑDRBy |3[WLd[ -8eoe5#x _b1J 9v3[Y%ј($bx>8΄(W(dY?fIJ[+c4&[} b^|ֽζ!i:gЧx Y홈y{ꥉOP}|FyX9~ 'Py'Pb•U.b^K>N3< WX9rAv,&PIĄ+U.b^+LDh|Ƅ+@E̫9}~rXc•LE FKu2e`Ӭ. W~+x٫ o6DdB  S A? 2zZzl5XߍPtI|+2`!tzZzl5XߍPtI0  M5Bx]{D$Juy9p}:#0*>QA`Ղ\ѽOtkÈ<} "**{EVǷ(=TIΤI~SNPH )! ڎt!_ڿpBmyuWO<)|_{DgoQ]QG=1+h?uL2jCl3 v&Xrˍ%T@V %Ӌ{TJҽrv6B~|;N;tKՎt+{7ԯjJߪ? `_׾j{R2-L: +m*| lwh0mͥ'O[DKӍ} . 0XpLmߙיd2eU8#Jgװ ;(:4J((֯1JBqD9V?C?ZXabPLHϞIN} 9I26ϓ-Vӕ&!f3-cp]D,f=dL۫۫Nr{Gvrcm/7J~^ n W*F{)ܟg#Q`? ~s~0fؙ̧6МˆsL+̉9 G}(~WW2ysBYR~b[uh,YsvӺy<Na ,y)=RǞ睂jVɮDĺ_2VfլV:Cl:^q@n{䶗Kn{eƷ|{9WK*vޏl}eT}(`"|&`\_=OŰ ׂm3{|N8s87>`l2`/yRb[uh,ךFyc!j>O j>oD|#5߈FD7"jQӫ Q@HXr5ƒy7\ͻjލ%WFAI|+P_Uwjn@n7{A;(EV!bEz kdUXgROK <͗x/54_ji>c!j>cO j>O j>5߈FD7"jQ󍈚oy*\ͻjލ%Wn,wcռK3+P_n5+P=L{Hp+PUA"b=DN h*54_ji|ROK <5C| Q1D5C| Q D'5@|Q D'5@|#5߈FD7"jQ5R#Vjj>kKXr5 T~jV}d>J+Po~ucU^?Vy|R~51#t_k:b|MG1 Z_Kk b|-A% 1v!.څ_kb|B]4cWg_}O?^|u>M4r\ƒ_n,ƒ_n,ƒ_n,|ٹ+Ћz=}dަ,.׋oo\/YnX?gc,.+sn^~˕B| Q)Dͧ5B| Q)D͗x,<͗x,<͗x,<͗xr5G|QqD5G|QID'5D|QID'5yKּKXr5ƒy7\ͻj[4 *Zk>y_# jgU?Vr*Yn#V`,r5B| Q)Dͧ5B| Qe>; Oe>; Oe>; Oe>;\qD5G|QqD5G|QID'5D|QID'%k޽ Wn,wcռKXr5ƒyK|+P Ӛ(>Vo\/YnX?gc,7b@,r5B| Q)Dͧ5B| Qe>; Oe>; Oe>; Oe>;\qD5G|QqD5G|QID'5D|QID'%k>kFj{e b|J "\ͻj5 Ԭ_}^(!WlxHi4 >X>Y>^"*QF& 9n䔺&ݜw-_p-l.}MOJaj7q+4QG_Gۅ'W's%Ҹ Z3aj}ݨzrm3\ɔ[+rMMPF琗'?#99בa~7:['?:6'@ ͛QB+Z.snC30>3 b~G b^_4e#_pj4 W._ |B,9K6 MW(a|<(5UÕWw>UrsuuZ״|M{jCߩ̻`Sss ܯyżeoaZ |=9];p6{9`?/sJ<@\Ybnsx4o(*"C*J] 9%.,19K<ƫj=K^Ivi:KgJik%n+ڸVS%.P2D(yAdGd>Mes/3Ǎ<(rNӕ˵qv.A޺/8)z{@y굿'e'ynL |qO>u3Ox[ܹMsp?y!`z7[̳{ u?Ox9[d^C퓿/wOwr\j>&!w|~.Ky{ B4{ #{\^k>8e5dZ>(rg#+*dl|Å;b^_L/" X9pe}󨗜Y5*9%&W7k<} -foְ<7B`oe7[XWeg n>7sr\ʯ*m8,SO!Rt~ Wv}}SH_o{;iPg~3!rN@%Q y9:TH^NpS=n WJ<>@Isns2YPw7#ʺwWX>Թua'.|e'§xysns2`tTsA3O(>s~fmS3KmOyz %u3=K|9pInuxgJܶ598kT^e>m%ZkbTݖSmm9L2r|4)G[vjZ>U 厗NLpJPYVsO~j܇ۜϚRlg@ l 99YRߎɹyv^C&d4K.zC#􏰵WΡG*1Mӓ hr)=SMkI&:PYlcϧssw5võkڟGwkry;[dI#\3 cDlOnse6=]|K;<_|cl^NH0M_G#^ur26uX]hcᓿ· /RmRXbR#rַMFo2j 5ַO~F,9ɀfze?Z^N I0Y UTO˄OQRx9;n53M;Pk)m/gmsIy9]ƞ| i;&#Gz76&v哿jS=TO|02Y҇p_!7`d͒Pm}TS?(6RJC9خ}!ؖfYgl24]8BqlW`n2nRfNu_BnqNv$+0jp pp &K2*<6n|rjd3U'aOlSbO׳4T'"l,QKdodI}sq|V syۜxW^E?-/xBSH􂑭}ns9uf oo B2\ʜÿ fzjf)d 0gՖ\S]Pmd9[7:3!9:ޏ]VY&c]{2_%|Yɜۜ̏ hifkXS+rV #[بbWz5˄O!26:v=Vx2_˦-~yPruow)G[5_as֣ _}S7gN7zY'SXG/T]鍴Nٴ'}LJ$OB:6<[>pZ8w\c\k-\u̧{.ph.WV}gd>GS&#g}jޓkt?c'̹M*"z睿>FSHtMΝ?n:|1ܓB-]Ü"I>§zIt~;_M@$ꝥ>d;K-fvy7S=5]f2v969Ym*V|/yh},T /wpcf? §!3ʗ̳Y['j/^|9jʉ7#btȗGwL9Or|}= W B3_u7gkXeg˷v+ҚlyAo2֟07B`~6?g{>}it94gCG5O&s!]a6ѽ4yyṿ"#鉑iȍ}~|d-%~x==٬fprV}g\>dszn-<&| ɖW0enJ 2^7a0҉?GZm-ebs>d:3;|ߩ*}G8$a7`1/^bps" v6ݣfME=25_<8, [3~췋:NɕIs:oy:DghWX[> UYe\g_l:Pߨ~@ej'eIu6;Ogw3tEUS{աBgxl|vUs6(7z_ufᓿ?^^ۜbQA1 fanRZ`>QW{GfgN6HM45RDL? BKJ*$\+~(ϗ4$P?TӪE%+b!Fj= 6ٝ]~H±~;ޛo޼]JWJLĤLGg42qi#Kzr$c&Gi#i2?וR1D3Z% %(c}DD!'= 8ǻSy̰(}b8=[ي-Nɽb~1A -'.%O\.8ƭϑ^Yq4,jh-ʱu 㟝(YҌUҟ% K {0-Qb~\Ȧ~J߆Ȼd(?yL-7LD7|8?(fsF8J3 ,>,>,>*>*>*>%Їp@]}K)CJRq>T)CJ0Ws0Ws0Wsp@N }8A'ᄐ}H!W`\\zW>LfĞ3Ru?Do5yaeW"y-2,/0dϤk̤-Bw?_^4E3)ai&%~!g䙭RNǰQiwGJPwxL߳V$\L.?o CJM69W;_i3X]P"ɛd?y$=$zRCnHi &CrLFҝd<#ESHa ~Yb:z#7݄-,p\?a>-"ߖKgǿMǟDWXXo:m&텸]wB <& uu|K<J#ӏ]K<$.$\iTb(q,wsy\⛠Jvn_8I"G:?I1zJ)g"hT%h+2^L,HA560I)]IC21=ff`g>s`߹Qwg]ZF,}(Q/&(C7LL0֚ਁ2O3>9xYLH5fCӉ1Y9e7Ӊ>r n>d9:$q\rMx;9.Rkh\5:6~Ə Q5T rY ןr2bp]\_\?0Ld&yA[I:UBJҹrȵV q\]C~R6Z=sY!|A2IYS̔b6jvOq򤯚RqεV q\]H\ @ O.K -ua!sW[8WؽUe"~{!D)/ % A@9 :/'U rm *UW@ֆş3@k:WgG " <;7Iov~vdAg1t]:W3pRJ~N\I'p%?'rÝ}Sw N>)Ї!a|H8&·!a|W a_>+Ї}@ a@ a@ a@9}8G>#Ї[p@ní}UCrr.ϝB+\Z+\ZaWO އ}s*xORyQdG`~'t>8 Y]FzoU|M~P?'Gu䘺R"a6ɥ&G $[Jg+,6礊}Md a*Yu06׏|} ME%jn~'ᶫJtM&& uh@Y{iYwwI@ ;.ez$Qmio MCY>KG;:M 3!lI}DJ#Sy4=ba؅bw Z y.58g4(hl2z?+q=R:0~enhny\:\́1Q!eGuLr#{Y4j.VXo*wzr؏4tJ|fGuݣ8ZOBwTeFݕxu3f}@Os3s[4V!e'-_nm{Ңߋq3qj&4,]3i%k 37f_? ?'U35CFyu޸ 0l@φ;(]K00}6oen\ߓGwN[>z5s=ɰĹۓUgexq5P쨖iXZ\LjY@zB|@E\{ =Y+p Uy35PfPc8g[Oa/P ο{̀|}1s?[PfsNШ7c oG,/ < z(1~@8ʻZU篃u:GpktRl"/ HLd4J>4qOl&$~RE֛شp1r7k.4&c<ڵģiK Y9~(P\l Ѐ@TG=Eݕ߫ioSS9Qi UV ṡSʬ,Rte FMR&a?:ʧQ(?|#(XprCdD8殼V>9uQ >G ODl P׹h.ٽ$šJc ht|V%-6A EݕwSk4aԩ'Tsյh9 |cm\Tw_Tcae[7*j4ʬǂ{xğg5e㳾Y2##!j\;u׳$|6ec{֗ql= TvLl{/خ~k|( %z5s :X6$[3^'/(%w30v;LPg+3ܛ^V8y%qJQk 8~~@+Y/H<>2g8ǫ }~ |(|(/(kw(*L}+(A ]1Y9Ys^$jr]m Y9Yt։W\[h|K @sY@=L:?K305|c TuPc|r00T]A ίSZ{`zilڻ*j`<2+1ق`+OcŠ*Cʬ,=L`>C6J30~|˥(&uS]5Ou+0F1l'3 :XtvT-Pc8uD c3 |*9cf: PP}ʽΧ5>Y<(^TJ \gcb((+/5_3fy cS,RnIjze%(}P>WOS0F1Z y+ F1sƨgSn|jUW@YK I\I%Թ@ ""kD\%R?Ŀ>"WjF4P; Rv}qa|nvw r?du}:#?>bՕ|Wq^kGk>bV])~>b-3eXXks*c7I.ӻvgBk0d4QLNj_^ayߦ&xAp' e pe\ L&:dV:ȭ(u Wg A`a b4b007{▾B!kK"˴ƍ2~e(@x.W:{= Due"]g2F'9Fhc!'7)`t+,c5'9`t} ac#'y`-02c/'_/O`t~z]T=>&s#މ4띨&"fqtXpa>eȸzJY#1c:t+͂vyKnqz!EE1ͪ':~HqRx6]3Gf{ B[#4ydjzvsbΜT:A"'Ehd kL,G(,P=N=m'x~{ѱO /eU,+KGt,GĴHf;SLƽL,FֲRG:uoIQ'q dHF:j Au F&HOLd2 pq/IE;oc}ߟ1vOod3J͈gV+]m Fvd>ժsJBB|++r9̂u+{NAYC5n> 6M9cmC8VakFKCYH ]0Q~8z, +dfƟżpnɸ^RV̍tZmҵג UТE^bi̮_G#5?'>*i@V{ C4d5` Z5'TJNjC3uV6>fI[<ǸG ' 5:f -’V *+uw^rDfX1_F ' GY#= Quɸui5R]u#ǡ7A^s?Z؏4"EJn83,Zlߏj+QV~TrQ `/~ۨ1z!7./0DdnB  S A? 2/D4q u/Ej2`!m/D4q ܖYz  PGJ0A;/x] tEꪮ *GhaוJeEBvݨ,!,GYsUaGW pyI`•! %RPD_=~M̤)뫿k:$_Pԉn~?lbͥ>V6qQ>,ď[+j-Ui }jryĸ,Ia[- $?CYq֯FQOz"lqdZPew+-I{y -svvyIȴI bX*XO z[ X-8& zK !X8~L ~X8,@#@2 k$p,6~~{XXbʒ^Xvw`^zq;rK*F Ě/+*\T`My(1V׏ ĺNU k@wba 5EV>`-+8J HJHvSc 4 Pb^JwZHknH<_N31~ ua%*6X$9m͸g_ӀuÂN<9͐@ }?1)ϛu@gb+@kR7K + Xw~3C"X Qr{cg9R#=Rz D )ڝ3^:jбIX@b}-sϓaVz8pLG{,ҎF\o߿4F%f Ѽ7k@%dϖʴʛчm$%.+TWyʃֺRCC %X]UqX#bX2Hܤ#E9X F!Z )C=m̴fciXb YZk*XӅ: P@^ u0a&N9Ls8au8L 0:&Psp@ùu8W f:,Pp@nu P u P u P !_rCա+:beVVЊYƱ+x6굶I=TIc+*eU+I QSqGrENW#?I:iF:%$ҳ"-`#kv}@ֳv=oFK/}R>lwPw dK"oᕘO+(9A4$Æ#Q5u.;VCJ&}rD[0ue\?+^Y濌v;,ԿXKYFvS,L`?NuxF뺧keWs[BS;:Vyac?׌sBsw9sfsdn>g^f>ɝ)=NtϏa&CD5ND)F lStCc=|v]PFC}h)TJ;B*P<Խ6`*]m,BB`=8.8ʼnpq4{S G"i>Ͱ2w^fT5|Cɼacgu<[c^g>aϤk<zC^&V}-pҖ+D}w䫤UA$*Y%l-J j%lJ @W V$XwcbXo6 (=;!G=h;mYcfVǺ_ ֳ:%D뎝J!U)^_FGk@ ꠈzP cڕ\ic2)(ˤ#?Igi.6+PɇGQT>Du}%G6Th ފ6Dp-*(?G#ETbĻp\øÃ)q>ǝ ]Eyt ףcpauhA[.Z7,{,NN ~tcu{_u?y?GCTB[ ɼؙ;aef'K훨D;yR3vD']Zj:CEգhZ֫:*Nx7pTwV u$R-+Y1^F(wx?+ć |Y>>:AGQ}v:e5hۅVKVs~3l\G e"vd^d$,w;tˀ:ZVD~Qo>c"ߊ(`{eTiﵨknn0x 0 dh|ЇBo.ꑩ>9ϰPsD~?#{cڒd=.ȆbWDnS.zhBCsbf%C#?Y$z'2|Q cn0Z7@^f~s*߇7J4tIqo.ݡ|QF}GCȻ$ NG%зΠvoNogjN37A+*I@^^ C!9qgfMCz@ |?3w0}]Ngkhq|ցy>Tyae~^k=>&L.o/`g4+rJװ2 ^ִ+{ԍQ}=jY# ;Ꞥ4Ws8uFO^ִ|uEb>h6̿3ۼ=;|ϟ vه@doiy;l~zrޗeRgs}6nee~}kfG0ma5euxBG=2s^xlS-xE[Et6$/g|`䯲DWx]>ѰVEp ZѿwRqV'F}rQBuJ ; O3Vџ7>LxL_I3jJ(6Z`X Z뙻֗/J*=`2BS<^ye&6=Xߣ'U9܆!j7i>@a}|$J[Hɪ.(.q4-Tdl@eo]feک:NrYif];g~񧙈c#//<>'곖yfL1y9L 9쯨~S]a$O]ja>Vmé0l9r2sX`>߮4Cw}&:#Zh=uT:R({겠F*"zOM2Y`,#,(06Tsȅ! eA;EM2>y׀|O@%*y1߫HV:k5漌?6fɥ]0Vp0 T̢1A@.ć99`']0;&S}6WW,̻Yd|G38YTMJ?N}M_ <=?,l=ae-}JP?V|6x~ qOL jV+&f70dU{@>_ȮaWr%vƜ1c DG= ؄ƿae^wA ك$T ++K%A|0A'u++컠sD_zЎώVvr;MnM%+ _&פHHJ ͅPVM%ncب܍V˟C?@S7-J:uV]*ߨ.۩s!vB <8a_ݬq&B{/ó,[=n1==Ws=`_%\ ؼUCϠy,)w߆l߆FʝRO= w|?>iݫuWIH=6g<ۃyDԢp{-xNX>_6O1+/3;>&1nE5;ȷ;/クOњ7X,]@r=&Ey򇨗\;y*"y *4BR[6`cT-w*oJ^!Kx\B*"(+`l{1ypl7hњ8>V|y-Xsn9i@v2oN sr ozΊ3l~;/ v~C$u"42$%Hb*yNGq^̑ϰln/3{@ΈNP'6t2Ͱ23efR@_V7K?ɜ? H`8).+hf|~Niz3?lQyeG lFdƟ._1to Ol3iŒa͜yY&R|a| Y6e)3_'u0 ,u.+91ɰI&j2~f|fCvl3:KjEaMyY&4A] U06b^¼ɀ|~\}YR3lU's^ffx@a6[|83΅sjfԲM.0eH& 6M=C;x=EzH2sD~f'eߵDp;wl^A ;~G+_:ۄ4ʗ      !"#$%&'()*+,-./0123456789:;<^?@ABCDEFGHIJKLMNOPQRSTUWXYZ[\]`abcdefijklmnopqrstuvwxyz{|}~ [4@4Normal,nOJQJkHmH >> Heading 1 $h< 5CJKH66 Heading 2 $<522 Heading 3 $6<A@<Default Paragraph Font b,bulletedl & Fh>Th(O(c,code OJQJkH(O( e,emphasis6,",i,indent h!2ib,indent bulletedh & F>Th!Biu. indent nUmberedh & F>Th.2OQ2 m,coMment6OJQJkH2>b2Title $< 5CJ$KHr u,nUmberedh & Fh>Th.  #&)/=CINQTWZ]`florvz} "%+.147:?BEHKNSX[`ckt{.  UVWXY\]^_`ef !  #&)/=CINQTWZ]`florvz} "%+.147:?BEHKNSX[`ckt{   !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefg., .f. 9e. d- H$#$o2$+^fMn?Z]\cV r$#+ 'w{i,r$뭆  }Oi,r$_fp<CPi,r$P%Hsp羙ЬiY-r$-8VX*0t%i-@v"#u(  T  c $A~<B  # }r  6| r  6{ r  6z r  6y r   6x r   6w  @ r$H"0I" /vHB   # r$H"$I"HB   # $H"$I"HB   # &%H"N%I"HB  # %H"%I"HB  # %H"&I"HB  # 4&H"\&I"HB  # &H"&I"HB  # &H"'I"HB  # B'H"i'I"HB  # 'H"'I"HB  # 'H"(I"HB  # O(H"w(I"HB  # (H"(I"HB  # )H"+)I"HB  # ])H")I"HB  # )H")I"HB  # *H"9*I"HB  # k*H"*I"HB  # *H"*I"HB  # +H"F+I"HB  # x+H"+I"HB   # +H"+I"HB ! # ,,H"T,I"HB " # ,H",I"HB # # ,H"-I"HB $ # :-H"b-I"HB % # -H"-I"HB & # -H".I"HB ' # G.H"o.I"HB ( # .H".I"HB ) # .H"#/I"HB * # U/H"}/I"HB + # /H"/I"HB , #  0H"10I"HB - # c0H"0I"HB . # 0H"0I" @ r$&0& TuHB 0 # r$&$&HB 1 # $&$&HB 2 # &%&N%&HB 3 # %&%&HB 4 # %&&&HB 5 # 4&&\&&HB 6 # &&&&HB 7 # &&'&HB 8 # B'&i'&HB 9 # '&'&HB : # '&(&HB ; # O(&w(&HB < # (&(&HB = # )&+)&HB > # ])&)&HB ? # )&)&HB @ # *&9*&HB A # k*&*&HB B # *&*&HB C # +&F+&HB D # x+&+&HB E # +&+&HB F # ,,&T,&HB G # ,&,&HB H # ,&-&HB I # :-&b-&HB J # -&-&HB K # -&.&HB L # G.&o.&HB M # .&.&HB N # .&#/&HB O # U/&}/&HB P # /&/&HB Q #  0&10&HB R # c0&0&HB S # 0&0&r U 6t r V 6s r W 6 r  r X 6 q  r Y 6 p   Z  BCuDEFAu @`o [  BCDEFAu @`nx \ <S m  r ] 6 l  r ^ 6k r _ 6j r ` 6i @ -/}/H" dh a zBPCDEF(P(( @`-/}/^  b zBPCDEF((P( @`-/!}/H"HB c # U/^ V/!r e 6g r f 6f @ .3 seHB g # .#/HB h # U/}/HB i # //HB j #  010HB k # c00HB l # 00HB m # 1>1HB n # p11HB o # 11HB p # $2L2HB q # ~22HB r # 23X@ .'3' dHB t # .'.'HB u # .'#/'HB v # U/'}/'HB w # /'/'HB x #  0'10'HB y # c0'0'HB z # 0'0'HB { # 1'>1'HB | # p1'1'HB } # 1'1'HB ~ # $2'L2'HB  # ~2'2'HB  # 2'3'B"  3 G#cN"  S G$Ԕbr  6a r  6` r  6_ r  6^ <B @ # ]@ -/H"}/& \  zBPCDEF(P(( @`-/H"}/"  zBPCDEF((P( @`-/M&}/&HB  # U/"V/M&   BCDEFA @`[x  <Z N  S AYB  3 8cXV@ g!}(! ) W  zBxCDEF<<x< @`g!}(! )HB  # !}(!~(r  6V r  6U N"  S G0*ԔTT  c $AST  c $ARN  S AQN  S APN  S AOT  c $ANH"  C G(Mr  6L r  6K r  6J H"  C G(Ir  6H r  6G N  S AFB  3 1ET  c $ADN  S ACB  3 1Br  6A r  6 @  r  6!? !r  6"> "r  6#= #r  6$< $V@ )*/M*p/ ;  zBCFDEF((F( @`)*/M*p/HB  # C*R/M*S/V@ )/M*A0 :  zBCFDEF((F( @`)/M*A0HB  # C*#0M*$0r  6%9 %r  6&8 &V@ !*/"p/ 7  zBCFDEF((F( @`!*/"p/HB  # "R/"S/r  6'6 'r  6(5 (r  6)4 )r  6*3 *r  6+2 +r  6,1 ,r  6-0 -r  6./ .x@ 4'52 .~  6/4'5) /~  604)C5+ 0~  614R*C5P, 1~  624j+C5h- 2~  63?4,/5. 3~  644-C5/ 4~  654.C50 5~  66?40W52 6l@ l)11 -~  67l)j+ 7~  68*, 8~  69+- 9~  6:,. :~  6;-/ ;~  6<3/11 <V@ \&m)&) ,  zBCxDEF<x<< @`\&m)&)HB B # \&)f&)r  6=+ =H"  C G;*r  6>) >r  6?( ?H"  C G;'r  6@& @r  6A% Al@ -$(&* $~  6B-$(%w) B~  6Cv%(%w) C~  6D%(4&w) D~  6E%(\&w) E~  6F%)\&* F~  6G &)&* Gr  6H# Hr  6I" Ir  6J! Jr  6K  Kr  6L Lr  6M Mr  6N Nr  6O Or  6P Pr  6Q Qr  6R Rr  6S Sl@ C*(@,* ~  6TC*(o+w) T~  6U(+(+w) U~  6Vd+(+w) V~  6W+(,w) W~  6X2+)+* X~  6Y+)@,* YN  S AN  S Ar  6Z ZV@ n z* *   zBCxDEF<x<< @`n z* *HB  # n *o *V@ \&z*&*   zBCxDEF<x<< @`\&z*&*HB B # \&*f&*r  6[ [r  6\ \r  6] ]r  6^ ^N  S A V@  3z*3*    zBCxDEF<x<< @` 3z*3*HB B #  3*3*@ e'6!'    zBxCPDEFx(P(x( @` e'6!'HB  # jJ''HB   # jJ''HB   # jJ ' 'HB   # jJ2 'F 'HB   # jJd 'x 'HB   # jJ ' 'V@ N-_(-w)    zBOCDEF((O( @`N-(-w)HB  # v-_(w-(V@ {!.+! /    zBPCDEF((P( @`{!.! /HB  # !.+!.V@ @,m),)   zBCxDEF<x<< @`@,m),)HB  # @,)A,)r  6_ _r  6` `r  6a ar  6b br  6c cr  6d d`@ /#1% "~  6e/O$41?% e~  6f/#41x$ f~   6g1#1x$ g~ ! 6h/$1% hHB # C DB S  ?  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~.# } }4"%| 4Qh4Ph4P4hS 4h&4_P4 2 414  4 R 4p4 4]4(4 4L4 X 4`4` I 44WN 4$ S4`44`4.4t484r  4"  4^  4,  4 r 4 6 4 $  S4A+4Kc S4- 4 4 4 j4 I4 X 4 ^4} 4l44l4lv4%l4} 1?4 ?4o #?4% ?4 4 5 4  4'4' 4 ?4X f?4 ?4 v?4 M 4(  4!  n 4!  n 4] ,4' x 4' x 4V4_4u74!4 f$4 4 h)4] ,_4!4? ! 4!4 44q 4{ 4! 4 E 4; 4; 4  4 4v 4  4qp4*4q4O4l 4l 4* f+ 4saofp4fK4ei4do4`P  4_PuA4^  4] %4\  4[ v 4Z h 4YC G  4XC J = 4W h 4VC = C4U  C4T v Jw 4/ J4 4 (]94  4  4 E 4% & 4  ! 4 417NOln!"/    !#&+,17<=EFHIKLNOQRTUWX]^`acdfgijln|  !"$*/@,G. @GTimes New Roman5Symbol3& Arial9Palatino3Times71Courier;" Helvetica"qh&&$20-Butler LampsonButler LampsonCompObj/2 hObjectPool0`m.0`m.WordDocument13>+.SummaryInformation(4VY .bjbjWW +.==]ddd$D(((((uuu[]]]]]]$:.b!duuuu[((gw([[[u (d([xu[[[[Fd[(,`ĸ9"[ choose ( i ) time r 2 e 2 e d skew transmission time high low ` b g r g s skew time s 5 OK rs 4 lost last r get ( m ) last s put ( m ) getAck ( a ) R e c e i v e r S e n d e r sr 3 A 5 B send ( i , m ) rcv ( i , a ) send ( i , a ) rcv ( i , m ) msg rec s rec r Sender actions state Receiver state actions from new i sender  "*.046:<@BFHLNRZ^vz6B*CJ$OJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH B*CJOJQJhnH 56B*CJOJQJhnH 56B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH  jUmH6 ",.248:>@DFJLPR\^xz   "$&(*,.02468:<>@BDFHJLNPRTVXZ\^`bdfhjlnprtvxz|~d  "*,.02468:<>@BDFHJLNPRZ\^vxzd     !"#&'()*+,-./01789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdd    !#&()+,./179:<=?@BCEFHIKLNOQRTUWXZ[]^`acdf6B*CJ$OJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH 56B*CJOJQJhnH B*CJOJQJhnH 56B*CJOJQJhnH 6B*CJOJQJhnH @    "#'(*+-.01899;<>?ABDEGHJKMNPQSTVWYZ\]_`bcedefghijklnopqrstuvwxyz{|defhikloprsuvxy{|fgijlnpqstvwyz|56B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH 56B*CJOJQJhnH 6B*CJ$OJQJhnH H      !"#$*+,-)  !"$*.6B*CJOJQJhnH B*CJOJQJhnH 5B*CJOJQJhnH  !#$+,-.N N!"#c$c%za#+ 'w{( wwza뭆  }O( wwza_fp<CP( zaP%Hsp羙Ь( 33za-8VX*0t%( wwwwOh+'0d   , 8DLT\ssButler Lampsonutl Normal.dotsButler Lampson2tlMicrosoft Word 8.0@@`@`DocumentSummaryInformation8__9400578567 FPm.p׺m.1TablehCompObj69h՜.+,D՜.+,0 hp  MSFTitlj  Title 6> _PID_GUIDAN{1FBE404B-542D-11D1-9194-00609797EA20}5 [4@4Normal,nOJQJkHmH >> Heading 1 $h< 5CJKH66 Heading 2 $<522 Heading 3 $6<A@<Default Paragraph Font b,bulletedl & Fh>Th(O(c,code OJQJkH(O( e,emphasis6,",i,indent h!2ib,indent bulletedh & F>Th!Biu. indent nUmberedh & F>Th.2OQ2 m,coMment6OJQJkH2>b2Title $< 5CJ$KHr u,nUmberedh & Fh>Th. "%(+147:=@EHKNQTZ]`cfilx{~$+.147@CILTWZ]aehlsw| !'*38;?BEHKN      !"#%&'()*+,-./0123456789:;<=>?@ABCDEFGHIR\]abcdefghijkmnsuvwxyz}~$%'(*+-. "%(+147:=@EHKNQTZ]`cfilx{~$+.147@CILTWZ]aehlsw| !'*38;?BEHKNQ  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~: c 2kH{ dDp H323o2$D<5L]Vr$#+ 'w{i:r$̸l gG]i:r$_fp<CPi:r$-8VX*0t%iY;r$P%Hsp羙Ьi;@l12 (  N  S AB  3 8cr  6 r  6 r  6 r  6 r   6 r   6 r   6 r   6 r   6   r  6   r  6   r  6   r  6   r  6 r  6 r  6 r  6 r  6 l@ #,%. ~  6#,$- ~  6$,%- ~  6$,K%- ~  6$,s%- ~  6$-_%. ~  6%-%. l@ G),+. $~  6G),*- ~  6*,+- ~   6*,O+- ~ ! 6*,w+- ~ " 6*-O+. ~ # 6*-+. r % 6 r & 6   r ' 6! !r ( 6" "r ) 6# #r * 6$ $r + 6% %r , 6& &r - 6' 'r . 6( (r / 6) )r 0 6* *r 1 6+ +r 2 6, ,r 3 6- -r 4 6. .r 5 6/ /r 6 60 0r 7 61 1r 8 62 2r 9 63 3r : 64 4r ; 65 5r < 66 6r = 67 7r > 68 8r ? 69 9r @ 6: :r A 6; ;r B 6< <r C 6= =r D 6> >r E 6? ?r F 6@ @r G 6A Ar H 6B Br I 6C CN J S AB K 3 jJT L c $AT M c $AT N c $AN O S AB P 3 1T Q c $Ar R 6D DN S S AB T 3 jJN U S AB V 3 jJN W S AB X 3 8cT Y c $A<2 Z # H2 [ C Ԕr \ 6E~ Er ] 6F} FN ^ S A|B _ 3 8c{H" ` C Gzr a 6Gy Gr b 6Hx Hr c 6Iw Ir d 6Jv Jr e 6Ku Kr f 6Lt Lr g 6Ms Mr h 6Nr Nr i 6Oq Or j 6Pp Pr k 6Qo Q@ 6&Y#q' % onT" l C G(6&Y#D'%~ m 6Rm&#q'$ R~ n 6S&0$5' % SN p S AmB q 3 jJlT r c $Akr s 6Tj TH" t C G<ir u 6Uh Ur v 6Vg Vr w 6Wf Wr x 6Xe Xr y 6Yd Yr z 6Zc Z<2 { # bH2 | C Ԕar } 6[` [r ~ 6\_ \V@ (%[)$& ^  zBCnDEF2n22 @`(%[)$&HB  # Q)%[)%V@ /$}/R% ]  zBxCDEF<<x< @`/$}/R%HB  # A/$B/$V@  -( ( \  zBnCDEF<<n< @` -( (HB  #  -( .(r  6][ ]r  6^Z ^V@  " $ Y  zBPCDEF((P( @` $ $HB  #  " $N  S AXB  3 jJWN  S AVB  3 jJUV@  l$E!$ T  zBCxDEF<x<< @` l$E!$HB  # ;!$E!$V@ (v$[)$ S  zBCnDEF2n22 @`(v$[)$HB  # Q)$[)$V@ i%!%" R  zBCnDEF<n2< @`i%!%"HB  # i%!s%!V@  H  Q  zBnCDEF22n2 @` H HB  #  H R N"  S G&!ԔPT  c $AON  S ANN  S AMN  S ALN  S AKB  3 1Jr  6_I _r  6`H `r  6aG ar  6bF br  6cE cr  6dD dV@ (-e)- C  zBCFDEF(F @`(-e)-HB  # [)-e)-V@ (.e). B  zBCFDEFF @`(.e).HB  # [).e).r  6eA er  6f@ fV@  -1!- ?  zBCFDEF((F( @` -1!-HB  # '!-1!-r  6g> gr  6h= hr  6i< ir  6j; jr  6k: kr  6l9 lr  6m8 mr  6n7 nx@  5(q62 6~  6o 5(q6* o~  6p15)]6+ p~  6q15+]6- q~  6r15,]6. r~  6sY5_-I6]/ s~  6t15w.]6u0 t~  6u15/]61 u~  6v150I62 vl@ Y)1 5~  6wY)W+ w~  6x*, x~  6y+- y~  6z,. z~  6{ .0 {~  6|!/1 |V@ s% ) &w) 4  zBCnDEF2n22 @`s% ) &w)HB B # s%;)}%<)r  6}3 }H"  C G;2r  6~1 ~r  60 H"  C G(/r  6. r  6- r  6, H"  C G(+r  6* r  6) N  S A(N  S A'r  6& V@ * * %  zBCnDEF2n22 @`* *HB  # I*J*V@ s%* &* $  zBCnDEF2n22 @`s%* &*HB B # s%I*}%J*N  S A#V@ 3*#4* "  zBCnDEF2n22 @`3*#4*HB B # 3I*3J*N  S A!B  3 jJ N  S AB  3 jJT  c $Ar  6 @ &1(3 T"  C G<&1(|3~  6'2(3 ~  6'19(2 N  S AB  3 jJN  S AN  S Ar  6 @ Z'U '   zBxCQDEFx)Q)x) @`Z'U 'HB  # jJ''HB  # jJ''HB  # jJ'3'HB  # jJQ'e'HB  # jJ''HB  # jJ''@ R U     zBxCPDEFx(P(x( @`R U HB  # jJz { HB  # jJz { HB  # jJz %{ HB  # jJCz W{ HB  # jJuz { HB  # jJz { HB  # jJz { HB  # jJ z { HB  # jJ=z Q{ HB   # jJoz { HB   # jJz { HB   # z { F@ /n"0"    zBxCPDEF(xx(xP( @`/n"0"HB B # jJ0"0"HB B # jJ0"0"HB B # jJY0"m0"HB B # jJ'0";0"N  S AB  3 8cN  S AV@  * -   zBFCDEF((F( @` A- -HB  #  * A-V@ /&U/(   zBPCDEF((P( @`/U(U/(HB  # -/&./U(V@ - ).w)    zBCnDEF2n22 @`- ).w)HB B # -;)-<)V@ +!]," !   zBCnDEF2n22 @`+!],"HB  B # +!+!N " S A H" # C G r $ 6  r % 6 @ 'g$(8& )T" & C G('g$()&~ ' 6'$(% ~ ( 6'H%(8& r * 6 r + 6 H" , C G;r - 6 r . 6 V@ }%U2&2 1 / zBCnDEF2n22 @`}%U2&2HB 0B # }%2%2HB 2 C DB S  ?  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~2 X X41 R 4. ~4- t4, [4+ v 4* 0 4)  4%>RV4$zj4# o4"2 2 4!l4a^4D 94 %4 , Rh 4 *q 4 *q 44 4  4.4 P 4 9( 4 \7 4 W< 44f c~4M 454:4-  4(  4ob4Nv94 oH 4oN4N8 K44D> 44P9)44C4 [4 4 j4<)4<aQ4*4 G4 aH 4^w4H%4644x4&4~/2y4/y4p/$y4&/y4pW4/$ 34 G4)4W4W4W&4W|4W64 4 H34 a 4 a 4y4 y 4y4?{4@j j4>,4 4 l4 < 4 < 4y94t>4 _A 4 dF 44* 4  4 P 4 44D  4 | 4~,4}P^4|r4{r4z~F24yF4xpF$4w&F4v~4u 4t 4s.F4rC 4qq4pv4ou x 4k*~ 4jO  4iO  4hO F 4g&O ( 4f4l4e0l4dl4c.lD4bv  4a& & 4`c  4_ r 4^ r 4]4\p4[@ 4Z@ 4YC % 4X r 4W r 4V  7 4U < 4T  q4S v4RB j4QM 4Pa4Oa4NM 4M{R4Lu R4KU{A 4JPvF 4If4HR4G*4Fl4E4D  4Cv  4BD  4A  4@ N 4?h 4>rh4=bPJ4<hV 4;Xh4:P49p48Vp47D6&46^6&45  p44N  p43 6 &42~ 6 &41*40f4/ Ru4. *u4-l u4, u4+  4* d 4)  4(y4'De4&BDy4%y4$I)4 I )4b  4  4& u4 v u4 : u4n u4p< , 4>< , 4f 4 4 4  4  4 X < , 4 & < , 4  4b  4  4 : 4:. 4:. 4 *+WZ_`rw $%*,579> !%*+019>EFNRWZ_`efkorwz{ $%*,579>DGLMRSUVXY[\^bdegjopuy{|~@hfG@GTimes New Roman5Symbol3& Arial9Palatino3Times71Courier;" Helvetica"qh&&$20-Butler LampsonButler LampsonObjectPooltp׺m.p׺m.WordDocumentmation8:+<SummaryInformationrmation(;DocumentSummaryInformation8 FY bjbjWW +<==O](((XXXXX,\XͶͶͶikkkkkk$<0b(ͶͶͶͶińiiiͶZ(i<JͶiiiip(i<ɅXX'Bi rcv ( j , i ) send ( j , i ) send ( i , m ) rcv ( i , a ) send ( i , a ) [ erase last r ] [ copy ] rcv ( i , m ) send (needI, j ) rcv (needI, j ) Sender actions state Receiver state actions send ( i , done) rcv ( i , done) j-new j s i r assignI ( j, i ) choose ( i ) rs 12 5 sr needI 12 put ( m ) j r g r last r get ( m ) last s put ( m ) getAck ( a ) R e c e i v e r S e n d e r sr 5 B 5 OK rs 4 lost msg sr done 5 cleanup new r 12 4 g s 3 A    !%'(*+-.0134679CEFHIKLNRTUWZ\]_`bc6B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH  jUmHS      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdddefghijklmnopqrstuvwxyz{|}~d      !%&'()*+,-./0123456789CDd     !&')*,-/02235689DEGHJKMNSTVW[\^_abdeghjkDEFGHIJKLMNRSTUVWZ[\]^_`abcdefghijkopqxyz{|}~dcefhikoqxz{}~  6B*CJOJQJhnH 56B*CJOJQJhnH 56B*CJOJQJhnH 5B*CJOJQJhnH B*CJOJQJhnH 6B*CJOJQJhnH Akpqyz|}    !"#$%&'()*,-.012345789>?@BCDGHIJKLMNOPQRSTUVWXYZ[\]^bcdefgjklmnopd   !#$&')*-.124589?@CDH !"$%'(*,.023579>@BDGIJLMOPRSUVXY[\^bdegjlmoprsuy{|~6B*CJ$OJQJhnH 56B*CJOJQJhnH B*CJOJQJhnH 5B*CJOJQJhnH 56B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH @HIKLNOQRTUWXZ[]^cdfgklnoqrtuz{pqrstuyz{|}~d{}~6B*CJOJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH 56B*CJOJQJhnH 6B*CJ$OJQJhnH 6B*CJOJQJhnH B*CJOJQJhnH A      )   6B*CJOJQJhnH 6B*CJOJQJhnH 6B*CJ$OJQJhnH B*CJOJQJhnH 5B*CJOJQJhnH 56B*CJOJQJhnH N N!"#$%za#+ 'w{( wwza̸l gG]( >|za_fp<CP( za-8VX*0t%( wwwwzaP%Hsp羙Ь( 33Oh+'0d   , 8DLT\ssButler Lampsonutl Normal.dotsButler Lampson2tlMicrosoft Word 8.0@@`@`՜.+,D՜.+,0 hp  MSFTitlj  Title 6> _PID_GUIDAN{1FBE4050-542D-11D1-9194-00609797EA20}      !"#$%&'()*+,-./0123478:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`ԿB̿(OWJ+cR qzXW=\"NDs8q:%tKXXXp@.u@:j:j:j:`C#Ml 5!= ZId On?*';^]WӿWN{c\Gjiog)w[**㝔>k7"5f'`o~Blm{J`߃yso·ċc̓c΅c? W pah 'RW;*k-Q:+ƳHQVg+w*?L1ޑB*7s=#sW*G\)jsk[[y'_ -~` 76\Y!MRFH-%:f_Q̅3rXD9d|뒬s.t;/~ROȼΞICG)ԝJKK3g:{`x whcϏ>~ߕȏL3>`mo[FN!_/m׻ubs8b=6BVH ڔ4BzdUO ms#GUޱUvL!&g(.6u$x>bk` =q~ѕRg(500m"Eу6Sܷ =A!^zf}2T5P>`x|ܦm) PI5ZNBf7ѹO(@U7W/>s7f;8Q32WwQS(ʊ]YsԎ}.j}#䨿UL/x[̠-WujM9ґa֪ު|:`}Bfad83UUU<&7Pm0K}.'lJGO_/&GړB1<>F[zrVPCbr~ V{(U\>_U䘭jÓcmfS& rju?`x|~j9cOkグvny+u}ߘܕXs~T Oomd(ŠAbxhK er~۟- e%r~T!;<ߜp2ʚDGe%6h3G >qe3(|3(eo@ܚW\KYkv:;Qfׅ:,ذezI7^6&'˚]OqM*'QoyrDe ]hg#nduװ;BRt\Fp\EU!W39:"z(B?Fu0BFD59Bur폐+{hp^i)W&pe =GQpG=7ӵ'|R ގ-q r~3BfE3ȓm]WEcUnEіuȋAU?'v9(gR/OjrG_G͚'A~ A%_;]A\J͖w]$k$#ͧRO($X էOkA\gs_=SWEUr%`ϟ ѾJҿdOd.x|h_ m1,dR6r_ 2`xV+A-+A*/rWh ma]5Cd Uh8V~ǵS O[ ͼLX=vWsĦmqUQ_M0w{ԣ-==Ѡ*u%jy<˶I٥+MW}V){>^cz>MŎD;zdp;d9To tVŦw/(P†eYOsK{a+FqlgRQx\YW†ezᙁ? v>]%+ <;=:ϕ|iP٤ c>mcwPn1^yulXSw1Uŷg~^8gg]QfYQøn^jS\3 귯w!E-o:=S=:QՆTjhYϵpR \,s uh};ٿ6L`."j'E5<\if~#jxӲ9s~t)O}OLKe|(D 4!F6B5k}Nz {bWЛA?7U ?L[?e?%KIsjI?=痒 Zذ,QwоTAeNK9W{y Q A% ɉf;"U\oEu"Bǵ!Wy\H\k@\3"z%BCr5=88WK\Iz1tt?t+m3z9A)_JGtGt^-{].8 GlV:K|}"i|-grlmm-U#:3>m!ºCg[2p C12p`^l}}-U 1@ܖ!)ZIHjPˠUPER:m("Pu uO:dtt?__"ωÆ0Xfx6=lT+ĦI !gYTѲ悢9h(Z'*ZE@P6T'P (z*zmEhG(vSE*C)J]GYf56M~=`|5xvJطihԐr!ͳu@ .vMZA0VS uWZUd‘Ѿtо`x|?6+XO̟ e Mp: moy70<6+LmU3VX.F1ޞezcK'䕔6Z6x5O儫)ZIQfz_,$ ~Uy7v e:\exGzm{u ɋ5> ')GU^Ŷ6K6~՞_8͢oPlGo9BgM i[{I30hd6wйV*}{gjwsy^:U; yZ֘-PCo<8.O6 c>u^} M_;qH3HDY "aA>,HƪlM\(K}h>bmHe$q .(\3_>zŽ z¨--7k뱌z4%@[G‰%dPpf4˅mٌbxriLZ֥4tDGW6JyVSw-ZSQf4V*S!GΟ2?iM‹Cr,&9i%ñMmɔp$K\.\:N8 0 l$j@% hΒˤgĎuiA1޹zEUƎW),nHˤoxh%+e ^)j/+Kƫ3kLx>F|u XbG;4U]\ gW8 Gvq*xSWzfk(J^6$~=/A+ / C=+}cF%#c510<1 FiU!*o@z_ Ow& El,?qUE0VS(U6H׫Z)%cUi89FCbz9Ep={$MPx| t];Zuv4MzM8pv5)/n1ޯ)!*0WTF ^Da1Ӱfˤm~3lfAz-B@Tlq?bx"g6S9.P}KU}㢁$j[%<#[j'`%o&iZ31eΣ2̙6jHS^oǐM}smZ_\%ź닼b]st:9ˬ#f.17f}si{~VX>_oaJau6cJIwoÈ7/ԃa)U*j38 >s w$9Qmux_P=fCz2UVosU>E_I03)U6Vy0N[uc1G-_?k`"e4q1 uR&F-yB]uJPw_$b"hc"EKBvHwZF|loɵ$kD/Cyir &熤<Te>HP ϳm+ͼFT8>q}+ٍ`8_KQ3?JR4Έoaߧ8'#ӈ^~Ě1K aDϺ9:9gDrm{1&m:bf}մ۷P^}(6~i__RvZq{`yp ;VUxwF>{sn~wO. MJ r/se-cޟ %G1D'?0{:\694jIPjMDokZ/,ܢbM:L/Ȭ[ܖ56-7&^[5L9gy[ogZ9 mvsi~x[ngZɳۭܵnYgFn)Di=ZƿQmyē ЪVZ>#Lvm<-/mh{eei_gy;ʊvfEszXTH*zBGf!zޛn-X&Ϸ=ޞυۙrzAZu-9Y 6^g?~<^ /hs E&!q.H/z2%A} uVU}̿h ɹ_C{j Iw(k;Wҝ , N.t1 wp7K|U}WJ;ܧ~%a9aua=[-;LWK#V VIw45ܵoj;{X pOȹ4#́npKy[#;$Z0op3\,w$Wܪ0?pCQ=)*Fq9! $`pG w0'jq+. QᮑtR($M`np 1_kE1=%&kL+܋%`pn;inBI\.nk5\~v|?lb+) S`p `ELᐺˏpLI ?pP0/p' w;Y]&cJntWp?twOJ{ⰺˏplI~0^-s[%[%`p`.p w `aIw4?d\;F]~?t{9PíxIR0pk{[ m}F+4ܗ [5R.?]~CƍF+Qu ^ s;RS$ݟ9QÍ ^Iwwi w̕F'nsWG%ݏZ?ˏȸ%JkL+܋%`pn;inBI\.nk%tKhLg^%Zz`閧{N-كPb-z٨Qa˭nA&Z_ٽtt8znz"]!nѺZh}h}/g]h݄h=h}hYh!Zآ*Urr2e /^.1\.cx\rr2e /^.1\.cx\rrb.W rb.W rb.W rb.W rb.W rb.W rb.W rb.W rb.W r1@b.'s9 \N r1@b.'s9 \N r1܈ˍ܈ˍ܈ˍ܈ˍ܈ˍ܈ˍ܈ˍ܈ˍ܈ˍ2b@p.`so~+\[ 6V췂el.`so~+\[ 6V췂el.SZ`>z2+Sŝ:P\L|nw."nE~0*R l'«e?wL-A;|=u6^9cf3mJW#zstj}^y͵ɻSLպe-Sou}TYjZ׷Lպe-Sou5T2UZ׷Lպe-SfZj]2UZ׷Lպe,S^XT[j]2UZ׷Lպe ku}T[j]2UZWu^5?3[)~~uo=RsǠ]:"A&){-m== g[O_/֭Yj_,/j5KER{fQ޿Yj_,/j5KER{fi_/պu5 /U,\V[WrYn]eպu5 /U,\V[WrYn]eպu\V[Wjݺ˪uj^.֭YxZfjݺ˪uj^.֭YxZfjݺJ.֭Kn]eպu5 /U,\V[WrYn]eպu5 /U,\V[WrYn]%UUZfjݺ˪uj^.֭YxZfjݺ˪uj^.֭YxZ˪u*R[WrYn]eպu5 /U,\V[WrYn]eպu5 /U,\V[Weպu~x\jr˥6^.x\jr˥6^.x\jr˥6^.x\jr˥6^.x\j|a}І~+\[ 6V췂el.`so~+\[ 6V췂el.`so6*Ӗo'kg J;o#k2>Xfeq[feq[f9n`q2-3[2-3[2լL.y܅+d:歧֟#n[w7Pq뫪kHyeeC'mB^5R։kZ{)\;>[lEOݍAN%w+oY]wdZi?ކyW]q7Q;[kS,׃R}OWA}꺙UuuU53I/k @NۯOn}Ǯ+{q8V[2mjZ>^_5sRg:+_M 8R6[Sd Ӄb)o֞Ԫ)Sr *HߊN[2`AT}Ӄ5CGK?{sv3հ@!qJrJǻOYov%}bĪ'j+{KZ/K̢moAKKbҮ1~-( {GBI3PҔ 87+Jl7OZ[R eH.}=UƶXխ]&;kJ2ڐdo9f!ƜIogcw|M [f! OQZg576猍?67;6IsݿLup/t;\ýRՒXpi >$wL/J p%߂_̑s{\-u\tISmuws{;K4JKA] %.p7I7OmoצhvQIc0pynp熌[K]cn_^,s{p%ݱ`Np}Hҝ" wp_t\!?K} wpynȸ>OL;egEE-xX&XC(+Rޖ-%= !z3--Vnym.4m,]Ek*Xf\Nmq9-y[^'ͳ`+w+q#dzw,G++G+X᳭+;V5htU ;ۂkFs-FX9וj ;g{{ڔ@ks,X >'42["oc=y)#8x8y)#8x8y)#8x8y)#8x8y)#8I\N"r1D$b.'s9I\N"r1D$b.'s9ɀs矲ہ3\[ 6V췂el.`so~+\[ 6V췂el.`so~+\Z`cB=Sww٭>Xxe[xe[xe2-s<_2-s<_2,s<9o9o9f}:TnSM(~tT(Nifg41SD$նЦp&;bf:|pɾݜ5zڂh}h(X|\ 朦;;0ʞ޻gžO C3ҏP[种eXԦ/ Od~zkຽokmy #[O8۲eZ?Sb)oZ{&zr2:T^ƶӗrFCamLvb9=xW,/*9F2>y585FFؚ}unt+Iߢ{t { ܍=>ڋgoi_^cgzݬ~V2Avg{^fol ^W l{a׳^ైZO=ҟnd~euk u:hukQauy}sʇ"Fߦ,X?Cb"*Z۪@_!? و֓֟v<|DFD!{7սx_!4byê{< n(uĵv rDkV:f B!Z!Z@Ph]hz óEG^Chpز n~>s7N }':+UTYC6D+TQ~V7o=Z oFN+#Z/!Z)5ZVw+Ux![aUT, #T՛ڄh}h 55Ѻj@ q6 q؀8#p;8܎8#0(8Da$7#Qqp088#p088#p:88#åp)8\8"åpi[ ǀǡ v`ǡ v`ǡ*8,t5'߄Gjh XU0?iVݑMߝ+t37C" s]Eq7ǽA%^_iyhă&WPEhAA"jb-DOZ5%\2{ovpfgw籉lAK M֢d : PKkhݍm@Sǐ[@va|#= x(3%.x?)o$l_K:o68V|d1!;8Jdl+^̳ѳqQʼc?(yQtqpܶcG O-f\G].3nl>FVqwqȝD5YߕPA8n!m+p_ >N?p:t(<^ 7l ݀ ~t9B-s7/o756^kkARйt3X_\Dc:fDbr[t2+s{=ęWocDGl֩"1YC ~w3B]=fUP:;;q*S0Vha1mݩkxd|mڞ*QO-qO%{]?d+ueԒ̟ZՕTIqTIqTIqX0a8W ^a*Vqت0[a8lUQ.X]F8buq0a8,W \a+rqX0a8Su NaT;NqSaT;a8lV Ya6+kn#@Y^Wqhluf]ơYq7_F0{/C{CƷ [8f]ZsOJ u+.u]ь[[7]AC~ ݈X]M y\>E'l\>iGJWƕL'zj%ZԧQZoô2 p 8Jd☞/̛P0,c X#G;̙,$0K$ilu_B9cO(L&zo̓ s21*|y}4ľ C!o"] N°!-H,ckjzM_à84;vahu[cgSgϰ3#w-/$=)gx߫g]bZ$ߟb/Ǹߝ"y Nс-ht]~wQb}e2!>. 9ELkiY˿%8ۨ|8dPfu{}MLAi2c=>4{~~ ܪs {2CsoNʙ3LkךW}`¼F9o;3/H^L{wo bw֙36R觎1v *#(sC l(,/Uw]ާc@\;"1|,>raǸ3/%vLDlr tqgDLoS j!DoZ:H7-h*E+!|:b)oe,h i"E c;i UrLb%g2q~&7VmH/iML>+F}ACݨh$ކV4 {s_o_fa 0F{pi]pn `J{)& ӕqu4%- 0Qb-e2^ |1y0gk+`lW\c.Q`8uub&-V+ng吏MT?f٨ Ax ?& xסH߀  _+@\x~w@gA80~>xk.k/ @׃s&wsZ">VvJ ߡU:=(<,5\FV)QcenJdd"AE;}YJ;O3ߝy2nY %~'2.'bՕݵ~MvM.Qb0d,_ "v11^|oLfzC2`Åy6L&22]K%]Th/E?xJdd ҏCt)*;Tc%63鍰Oq@)Y)Տį~53S @.n]_c=/Gg2S SVҘ9DF// Z Zr *ran`ƜL-L?-ZRiqy %2g27  S%.̧b>DLfja|'L$/qd[˸zp͒&=1^},D/VK\/_bcdAb!`΅?ts:D/fC|):fP6f_mL#|0xic>{1'&lIyM2x>OQM̫*zj]/Q6L־^je&}m tOh:] u)ԵSftLB]*B]YWB]+ԵE:;=ͺF+5[D΁Ao5,`]!x{6Q룶dKvX뚨PBP7 utSkB][Bst XWEA^]2n mF3qM}&߸2Ƶ*>5zNc`n>FĎ>gӘC+AK 0QqlaUҎs2ٸ^'Ϥγq=SRTKl=2ϰqxfۻgc8%F1yxq5%<2*4?/ NJG9>GqiVO_kZ*_z?)ϟ Az~+}/]'1^<m&3eڏ]bPV3 + je7n}*"Fv dC"x7"vm뗌HfӺ s@GQ(myvϴ< k VzSjW n Zs n":L&ͬj?׮i}˅2LwLP8R;GCTǸ{QSwE&qx.>]4+;43!.Dd>oB  S A? 2n-,;24,co J-U2`!B-,;24,co Z/ H?-x] |T= U[DZOg 3JVy. -(>xѪTˀ:>`V]gYuY*2v$rOnnܐ|_Ƚ_{/眜$ 4_5Gw,'ݴoo=J 敉EDB|BN >$Z*i gk!< MKiXbXؚ6mu>ٿu]| \KH 8Log2[o(ðoSbyf+,L#gAb>e+,{aJH,+[vz#֫իի^5ZX%ZXڅX]IՓkbF!kb!qz=Xs8Ja JX-Ye[T22V& -ݝp}ϴ3-vn";-4E ;S~]+Sڊ?UJ$˧URG0&c'Է6M;혟N5eތzLm>?g{"ܪywsɔ>*ISSf״A]N5L:Kl/haFW5H7h3*#=Hײu 7>}:/ڨ߳쒮x KՊ%xT5ǽkl8̿m/̯Ԏ\`us'yb.l**H? Š=?$}cR |FD10an|R ʼ_d:%<ݦ{eD綗hsQzycN$^nVһO^NJƓcfO7 [<9OQO?'&1o'{1x9fUz|9O|SR'cFz8r̽[n^ &lqsր>5/րőcnV>Ϙ/>1x̅Me>[;'"擁wwy#1sn m@m,N7Wf5KO>x=7a{njT]>+hRőq.0"ӖdZ/ő1a>8VI/gKc@ӍzePC \TS򈘏1>|cΤ\آ@t;@˓%{Z|ڒAzZ/ԖE5Pd֪%l | |qV˙ƛܻB-䋹"l Ib,d> |(A \̅-604F3saՖ:hʋq63?Gz̅Me~yd'|B㯖)YSYV|NPaAE^u$|eڣz]eZ5 ߳+ս(l^lкG^Y{l .¦2ѾοL~6x~ǟ628| {ׇdv]z9 zq'vp~'hx {F1)5ܻMjMR{–ӫ\]Я=jcKo}P}95>0_<1Kf}mR|y95.ϸ`us?}s\XZtȽz1 3^jvK2x-:ϱ{a c2%(%'KhaRB]:]{QUV 4<i /c7I}R#!lq\[Lg3}>\z̅-C9~q- ]cjA*- GO+s [!GȤ8z237I GVW$- rw18sh=|ɖi`[eVޱ~`ltXjNT͍V(^v-Ke՘RKS3N7IO6YkvO|b'{[4ۢf2ϱ'H-.KRy菒fƳCe2^j{.=N\`Xe,KXz{`BZ8"vD=VBZwul{*sEoDb^Gp4mn"G~O)@r D'zD]X=(DEX#bmG*xX#l+*gj&(c-7f-57nl[gFm?P$ňX7"b=RxX?Gz cDcc}NӘ*cEd,@Z(58l}Q-{EY, =6"bC*/Lk4"b4M:܄M:܄M:܄vD#Q:lGa;+ <Vx:0tXaaD Q5:Aa  p  p  pI :^}=+'5BW:~z "ɱ:!b-Gڀ,qV'%1cqUX7ECp΍?h|tngqɰV=G~*#ٺs/ o*Kx/a4OCMӡPtx:Fa5uXjDV#Q:Ea-kuXfD6#Q͈:lFa37#p37#p37#p3;u؁Dv Q: 1$<B êAcūC1)/MXЉXЉX0W$b [Ȋrg g \w?w?۶WKϯ+jgiU#V^`0wA;U߁ւi,nZ'X_ bMǺk)"3XcJJ~իwuy̮'ҡ KsC\]J*R l\ D~&J^V*axYeJ^V*axYewVRJc$f,.wv0g۱mWlJlD$Z\ '͈X!b};gM8.Fĺ)DX>É52f,]bGK*[En K!kڞЙ]Lӥhw3Xz?Aĺ Q-:lAa [u؂-:܂-:܂-:܂Ã:<Ã:<Ã:< O0<`x:t8p'!p'!p'! QM:lBau%XЉXЉXHgyʞcggįknl<@WseRטl…12M|7>op{Zz6#y=m2ɓy'wS8Lԙr{v\o ZƆBk;~Or3+b}la^ |~C&e >? '`sW%s/{^70˯s+ؚ`2YĞ̇ 8\rklmt4γFFvF {z饞=fh & "4ޓyX>Ke.l*W$ЉE=qo`tvOtlKeH.J =!7[CBN/y j {6].]xUwCmj|jl5ޫQK5E*z;]'atVHvA_@'7݋y`/}%|ʤoaS=t?M>S7?"}@r]lq=kd$~ǼXU0}ļ" 꿢Mtz8`e16a^+=i] 'ZGm v;|*O1h+RZ fQ>=/aX/g1| P}03Y>u+aySCRizn8\rZOde=|1kY{|K)UӪDV,Y 'WvH/6^]ϒGrwz`i-xwXC UU3X倵9r,57Fy_Lw!~Cd<[ӟ$5_ ¯…**\x¯…**\x¯…Ū$x:$x:$x:$x:$x:$x:1:1:1:\e:\e:\e:|Q"YD>gu, p p pO:̰8N qWSxxuĊWNxuĊWNuXjDYC铺iʔ[jdi3ϑDN饎 :jPU3Yۦkr,_])>|^O>s6H> |!y/%&_I^ |ޕӷyo?n| SANH7'zoڤwzWzN=7Ar4MI_J 3sTt'>rG;,kH/-Gڋ*v2Ӡ+27Iit[ դKajFҔ8x }SWu=CYsWݼ9V9C`Z]-ԫa!PsBN'+|>A""泯*`OG yj=z c9[#ڳ}e1N'YU}(vZؿaUᦦ `ݐ'2b~,2͹l}6znL3?( 2s-95[;2QI`C?| ,3S$eBir+jHVhROɳDj*8猪n: ΠC`cب#8.SyubvQYYnQ3eZ]Gfz8C`&e"{YDf>22bAݑQҠY){-w=ldsi~hqȭ㈝[o'\=h6rGRoo#a##ڧ}:>Ov`iHdq( 7s=rAuray2,XKF' 'VtI$ m# ooށ߾xxDKl$@L|] tETuaQT|F 12ODAA1,6*L 6#eߓ%2 F@0 }ǹ?uZ|,̅LQ E\?dsE};[! 2QNȷ6Ŀ9n!mX;$bTyXKʕUd,> X%Ir/3@DJŸ# JջciЪS<2CqXG$b5v+M"$XJJ"V׽X%b=#kD}~c#kDEvJRCC"֓$b}!K1ݸ%`w-ZX-\%5@",X$bN2jbB˩{W+Dk}2%b=/=X$b]嗇Y"$cY۶%rK͑^N+88888;,j,m!o{Z0@XfjMc-S~&MtnxwWlNmS7qsƎkVq?+dWdڿ64#G.k)M1?VA\g;tܸt7i(|WM*?V֜纈A1&`n8q`>Bf~P>ViN1myZ̺\1?uW#q(cNǡKj%Y%8 iMLם68ouϮșr 3r&E.>qmr&9󰫜;͙>. c>B6N_V֧z{:eQN6MO Z_.bGZ׮>__XHk^ T/a]ƏErR/ul5~&X|iQAbr]Լހwz~^&3dlm=ؙM+qz*C<)[Muw7̹|r'̗UY`?a^|ײ ՞5X\<_z|ߧ6Mb柙VV\'TsO_egyPqXlsӊ7s_08a^y1K Hi38a~˜"2k8oB+;Cg)Sf nŴb:ze\g,%˓2NU'`l8b8Q̽JuXg~Rq¼˜< eft'_(C<eS̞yn,9%[h08a>-iQkF!4NO?r+u24]I*? k8ir= Dx5uӒcGdv6eok̪\O`{m,:Z5p"=BF 2~KS$~O?n A@&tڍAsi6]Lҕt}щt-ЍG܋ۙ8u+@Hu9iOƋRSI`ZD/ldDh쪄?VZua)>ړ3/̓49a^meeuV*-kE0+5N']SlQ7zR&䀺T H:\tg H6[Lr [Mư9Lf%BJ!NcJ`)4ե٬֥Uj PUz@U.0+ 8o<1g 6=ܴ'%'+l- MM4s<ʹzWV0:}NGPe6ϪrjD'z4Ws 5R3QٝkMfw!"tS=tD2|q_*W+ jU88?J:RJH:5D%bmu\"uID%buX"VΕ*kDUJĺ"s":HzZ"rX{%bx>f0kejZ퀫:<|hNSB͔k6o8~cDu3Nb۲gƈj?8C{K9aWE> ^@pHBSt.A\ao2ɟCi>İ,3zdH`TFo\O7} h9-wh'MF 26f0FMF_ 2*`zKYAFG0JOAFmwxwxwIcQ(A@J 6suc u>Ϯ1 2,nx& AF5ܣ: 2.^0zd4Zѣ`(<LFf.^0b2#hX]`ѻf.^0zdY:X6u&AF[b+ FLF'`sX/U"' ߛwD}<˪?f^T%[@5m_ΞZf-h| I Pq}Ykb lMF2f.^0ɨTV 6{b>s!=Tg܌MV2XA"XÒ=}Muy p?z]O_?xrD>pSP&Hek ׹E<5b;{~ W;>V@y)%YudXA-do8“qxZK髝 Z2LO{tcu髩:hά`Z,Zxka %Esf)3_ܭ|hܓcIa8fo5~PN<<Ǣ9sL5 w:O'?R{»N|2 r}uNxuOtv;2|`e>g|[P'lo3Y[MR]`{|6k}_h;}RAmw\[VNi $tC6YdH>_Mo;1۷]imM1B}֝֍5|κOglӦ6طvMh;2EvGc:O}˂wׁ~Ҡh`2؅67[ۂM6 &χn%ClۃhIp8+M!l8w!X yH 8 oEYMA)j+6i-fVv/ A:v&/dؽ:.bMtoRZ6cw1J7̹<7ݛNfi;ʜ"vNU06l} ZFfm-,JZLFl4S#Qn"6[-#0yDAwqasp#i]@i`!`p؎sWCJпڎpdM:Դ'Y˳G2oD3ݩʜۣV;Oh5JGL3YURep(SkX GWT~9b:mCԱO867*zi)I;1TableyInformation9NSummaryInformationrmation(>DocumentSummaryInformation8 FCompObj!jOh+'0( @L h t /Reliable Messages and Connection Establishment0eliLampson&connection, at most once message, LSWli Normal.dot Butler Lampsonm7tlMicrosoft Word 8.0 @캃@7:@*[.w A՜.+,D՜.+,l( px   bl9uj /Reliable Messages and Connection Establishment Title 6> _PID_GUIDAN{31E4EC96-8DAD-11D0-B4E9-000000000000}  FMicrosoft Word Document MSWordDocWord.Document.89qC [B@BNormal$dCJOJQJkHmH X@X Heading 1,1$d CJOJQJkHN@N Heading 2,2$Dd  OJQJkHH@HHeading 3,3,body$P688Heading 4,4,q0$588Heading 5,5,q1 88Heading 6,6,q2 88Heading 7,q3,7 p88Heading 8,q4,8 @ > > Heading 9 6CJOJQJkH<A@<Default Paragraph Font6*@6Endnote ReferenceH*""TOC 3&!&TOC 2 h..TOC 1 X !&&Index 6&&Index 5& &Index 48& &Index 3& &Index 2h6 6Index 1$xCJ&(@& Line Number, @,Footer  !,@,Header  !<&@<Footnote ReferenceCJEH@@@ Footnote Textd$(CJ&)@& Page Number((ie0  $O$cont P  ex !h4"4Glossary entry"<*2* Reference#x2B2pub$x BRBtype%| XCJOJQJkH$Ob$in&DP2r2ax'$$P 4,O,ref(d44gr)$d $ 4O4pic*$d"FOalin+P&O&cap,8 qlax-P2O2fnormal. OJQJkH"O"tcap/d,,tab0$$$ajn1h:O2:sig"2$$Hd( X:O!B:pe 3d$ CJ$1B$pa4lL8O1B8pf5d( CJ2Ob2t6$"FCJ6r6points7$dCJ0<<ex18$Hd  CJ0<a<in19$d CJ0BaBin2%:$Pd LCJ0..in3;x 8 l$$in4 < \A\rule-=$$Dd@& 8 5CJOJQJkHP1Ptag$>$Xd@& 8 6CJOJQJkH>O>gdaf1!?$d  84O4inv@$P !RORstate6A$Dd"F ( 4p O" linvBPjR8i} OOQQTWl'0;EAF|HORSV[ci,wh~bڌvИxxnݺhx2z~<`J Lt"@( -/f1P34V7:<DILN]cfhklnnpqvs?zCz  !"%')+-./149>?BDFGKMNOQRTUXY[\`cehjlol8`FFcGGHQERSMSTXdY&[rqv܎P̐ؒפ|'$T@ZdBf |* -(/j03N44A3KNdvijjkn'oVpq^rsCz   #$&(*0235678:<=@ACEHJLPSVZ]^_bdfgikmh,FGERSZ ħn4Tk>zCz ,;IWanBZ\999IIIccc9lQlSl}sssx yy-y::::::11:: _940025544 _940057739 _940057751 _940025417 _940057771 _940057783 _940057799 _940057814 _940057837 _940057856ZZ9IIcQls@@@@@@@@@ @ZZ9IIcQls$*+22244j5p555)6/6o6u666????!@'@+@.@n@q@@@@@@@@@@@@@@@AA#B&BBBEBJJMJPJJJJJJJJJK!K5K8KMKPKRKUKjKmKoKrKKKKKMM8M;M"O,OOO#P%P,P.PVPXP[P`PiPkPPPPPPPPPPPPPPPPPPPPP4T6THTJTUUZZ [ [$[%[N]T]w]{]__bbMjQj'k(kkkllbngnooqq3q8q>qAqjqmqrrrrrrrr7x:xxxxxyy:y;y=y@yVyWylymy{y|yyyyyyyyyyyyyyyyyyyzz zzzzz$z>zAzIzPzXzYzezjzkzlzrzszzzzzzzzzzzzzz{ {{#{&{Y{\{p{q{|{}{{{{{{{{{{{{{{{{{{{{{{{{|||||!|"|2|3|?|B|O|P|J}M}r}u}}}rs|}ԂՂ2<ABMOST^_uvNJȊЊڊBK!dgސ OQY[”Ôʔ̔MOpr=?TV˙̙GH}FIU_vx֡١MPVZ IJuz׬ج߬LMUVZ\qr|}ۭ 2457OQSUVXprȮɮЮҮ79?@įůϯЯ '(+,NSTYgh°ǰȰɰntz`cjm~ϼԼ !":<=>Z\dgntx}ĽŽƽ̽ͽѽڽILWaps~ѾԾ47ST\]ſƿ'(23MNTU_`rs24+.QSxy}~ 57GN`epu ABZ[efRSabqrUV`a89st]` ),9>]e56DFGLZ\ab{}!?AORqr~#$'(-.=>`cwz,-;< NQfi )*1268@BJLxz$%JKSU[\giCD()cd  |}%&sxXYab +,ABQRx{|~bi        ! 6 : f i             [ c y |     ORCFw QTfi| "#$)*=@BGHIRSjmsz!$*-24<CMPZ]afghqr ,48>BEMP~58ALPSefqr|}!".1?@ij  PQ LMXZIT& _58wbc "E$$d)l)5*9*--..11<2@222L5O55566@6C666~99n:q:===J?????CADABB2DEHHJ%JLLMMUUxZ~ZN]U]^^^^``LaVafkgkooppqqr%rhrjrrrrrww||'~LN>2:dgǍɐ*.9:ܘ?B)+MOMP*.\aݼY`_<LOMPcgxy $'>A #'%Z^XZ?CSWPSWZoqGK$cgw $F  5 9 LMButler LampsonQC:\temp\AutoRecovery save of 47 - Reliable messages and connections (DS book).asdButler LampsonLC:\Data\Files\My papers\47 - Reliable messages and connections (DS book).docButler LampsonMC:\Data\Files\My papers\47 zz Reliable messages and connections (DS book).docButler LampsonOD:\Data\Files\My papers\47 - Reliable messages and connections (DS book) PC.docButler LampsonOD:\Data\Files\My papers\47 - Reliable messages and connections (DS book) PC.docButler LampsonOD:\Data\Files\My papers\47 - Reliable messages and connections (DS book) PC.docButler LampsonOD:\Data\Files\My papers\47 - Reliable messages and connections (DS book) PC.docButler LampsonOD:\Data\Files\My papers\47 - Reliable messages and connections (DS book) PC.docButler Lampson2C:\Autorecover files\AutoRecovery save of Word.asdButler Lampson:D:\Data\Files\My papers\+html\47-ReliableMessages\Word.doc@HP LaserJet 5P/5MP PostScriptLPT1:winspoolHP LaserJet 5P/5MP PostScriptHP LaserJet 5P/5MP PostScriptG o<XLetterPRIV''''HP LaserJet 5P/5MP PostScriptG o<XLetterPRIV''''I,*+-ABLMgPgQyZy[yaybghjkBqBrBxByBzB{B|B}BBBDDDDDDDDDDDDDDD}}}}}}ĶķĻļĽľĿ6666VVVVVcccL L LLLLLP@P.P0Ph@PHP@PTP@PZP@PfP@PnP@PvP@PzP@PP@PPPPPP(@PPPH@PPPT@PPPPPPPt@PP|@PPP@PPPP@PP@PPPPPPP@PP@PPPPPPP@PPPPPP@P P@PPP$@PP0@PPPP@@P*PX@P.P0P2Ph@P6P8P:P<P|@PFPHP@PLPNP@PbPdPfPhPjPlP@PpPrP@GTimes New Roman5Symbol3& Arial;" Helvetica9New York9Palatino3Times71Courier!ChX&7fw A9+20u.Reliable Messages and Connection Establishment%connection, at most once message, LSW Scaling 83%LampsonButler Lampson