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

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 67)

Recall that nil denotes the absenceof any packet on a link. Thus the state of the (u v) subsystem just before the response issent is (a0 nil nil b). Similarly, the state of the (u v) subsystem just after the response isdelivered is (a nil nil b0).We claim that it is possible to construct some other execution of the (u v) subsystemwhich starts in state (a0 nil nil b), has an intermediate state equal to (a nil nil b) and has anal state equal to (a nil nil b0). This is because we could have rst applied all the actionsthat changed the state of node u from a0 to a, which would cause the (u v) subsystem toreach the intermediate state.

Next, we could apply all the actions that changed the state ofnode v from b to b0, which will cause the (u v) subsystem to reach the nal state. Note thatthis construction is only possible because u and v do not send data packets to each otherbetween the time the response is sent and until the time the response is delivered.Thus the state (a nil nil b) recorded by the snapshot is a possible successor of the state of(u v) subsystem when the response is sent. The recorded state is also a a possible predecessorof the state of (u v) subsystem when the response is delivered.

But Lu v is a closed predicate{ it remains true once it is true. Thus if Lu v was true just before the response was sent,then the state recorded by the snapshot must also satisfy Lu v . Similarly, if Lu v is false justafter the response is delivered, then the state recorded by the snapshot does not satisfy Lu v .Thus the snapshot detection mechanism will not produce false alarms if the local predicateholds at the start of the phase. Also the snapshot mechanism will detect a violation if thethe local predicate does not hold at the end of the phase.23.7.2 Intuition Behind Local ResetsThe diagram on the right of Figure 23.11 shows why a local reset works correctly if theresponse from v is sent following the receipt of the request at u.

Let b be the state of node vjust before the response is sent. Let a and b0 be the state of nodes u and v respectively justbefore the response is delivered. This is sketched in Figure 23.11.The code for an augmented automaton will ensure that just after the response is sent,node v will locally reset its state to f (b u). Similarly, immediately after it receives theresponse, node u will locally reset its state to f (a v).

Using similar arguments to the onesused for a snapshot, we can show that there is some execution of the (u v) subsystemwhich begins in the state (f (a v) nil nil f (b u)) and ends in the state (f (a v) nil nil b0).But the latter state is the state of the (u v) subsystem immediately after the response324uvuSnapshot RequestvReset RequestTIMEa’bbf(b, u)aab’b’f(a, v)Correct Snapshot PhaseCorrect Reset PhaseFigure 23.11: Local Snapshots and Resets work correctly if requests and responses are properly matched.is delivered. But we know, from the correction property of a local reset function, that(f (a v) nil nil f (b u)) satises Lu v .

Since Lu v is a closed predicate, we conclude that Lu vholds at the end of the reset phase.23.7.3 Intuition Behind Local Correction TheoremWe can now see intuitively why the augmented automaton will ensure that all local predicateshold in time proportional to the height of the partial order. Consider a (u v) subsystemwhere fu vg 6< fw xg for any pair of neighbors w x { i.e., fu vg is a minimal element in thepartial order. Then, within 5 phases of the (u v) subsystem the request-response matchingwill begin to work correctly. If the sixth phase of the (u v) subsystem is a snapshot phase,then either Lu v will hold at the end of the phase or the snapshot will detect a violation. Butin the latter case, the seventh phase will be a reset phase which will cause Lu v to hold atthe end of the seventh phase.But once Lu v remains true, it remains true.

This is because Lu v is a closed predicate ofthe original automaton N and the only extra actions we have added to N + that can aect Lu vare actions to locally reset a node using the reset function f . But by the stability propertyof a local reset function, any applications of f at u with respect to some neighbor other thanv cannot aect Lu v . Similarly, any applications of f at v with respect to some neighborother than u cannot aect Lu v . Thus in constant time, the local predicates { correspondingto link subsystems that are minimal elements in the partial order { will become and remaintrue.325Now suppose that the local predicates for all subsystems with height i hold from somestate si onward.

By similar arguments, we can show that in constant time after si, thelocal predicates for all subsystems with height i + 1 become and remain true. Once again,the argument depends crucially on the stability property of a local reset function. Theintuition is that applications of the local reset function to subsystems with height i do notoccur after state si .

But these are the only actions that can falsify the local predicates forsubsystems with height i + 1. The net result is that all local predicates become and remaintrue within time proportional to the height of the partial order <.23.8 Implementing Local Checking in Real Networks:Timer FlushingIn the previous section, we made the snapshot/reset protocol stabilizing by numbering snapshot requests and responses. We also relied on the fact that each link was a UDL.

In practice,however, there is an even simpler way of making the snapshot/reset protocol stabilizing. Thiscan be done using timers.Suppose there is a known bound on the length of time a packet can be stored in a linkand a known bound on the length of time between the delivery of a request packet and thesending of a matching response packet. Then by controlling the interval between successivesnapshot/reset phases it is easily possible to obtain a stabilizing snapshot protocol.

Theinterval is chosen to be large enough such that all packets from the previous phase will havedisappeared at the end of the interval APV91:sigcomm]. We call the general method timerushing.The main idea in timer ushing is to bound the lifetime of \old" state information inthe network.

This is done by using node clocks that run at approximately the same rateand by enforcing a maximum packet lifetime over every link. State information that isnot periodically refreshed is \timed out" by the nodes. Timer ushing has been used inthe OSI Network Layer Protocol Perlman83] and the IEEE 802.1 Spanning Tree protocolPerlman85]. Spinelli S-88] uses timer ushing to build (practical) stabilizing Data Link andvirtual circuit protocols.In most real networks, each node sends \keep-alive" packets periodically on every linkin order to detect failures of adjacent links.

If no keep-alive packet arrives before a localtimer expires, the link is assumed to have failed. Thus, it is common practice to assume timebounds for the delivery and processing of packets. Note also that the snapshot and resetpackets used for local checking can be \piggy-backed" on these keep-alive packets withoutany appreciable loss in eciency.32623.9 SummarySelf-stabilization was introduced by Dijkstra in a seminal paper Dijkstra74]. Dijkstra'sshared memory model is enchanting in its simplicity and makes an ideal vehicle to describenon-trivial examples of self-stabilization. We showed how to simulate Dijkstra's model as onebig IOA with a few restrictions.

We also used Dijkstra's rst two examples to introduce twopowerful methods for self-stabilization: counter ushing and local checking and correction.Next, we moved to a more realistic message passing model. We introduced a reasonablemodel for bounded storage links. Using this model, we formally dened the notions of localcheckability and correctability and described the local correction theorem. This theoremshows that any locally correctable protocol can be stabilized in time proportional to theheight of a partial order that underlies the denition of local correctability. Our proof of thistheorem was constructive: we showed how to do augment the original protocol with snapshotand reset actions.

We made the local snapshot and reset protocols stabilizing using counterushing. While counter ushing relies on bounding the number of packets that can be storedon a link, we observed that a practical implementation would be based on bounding the timethat a message could stay on a link { we called this technique timer ushing.Together counter ushing, timer ushing, and local checking (with and without localcorrection) can be used to explain a number of self-stabilizing protocols and can be used todesign new protocols.

Характеристики

Список файлов книги