Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 65
Текст из файла (страница 65)
Suppose the physical channel can store atmost X packets in both directions. Then AfekB89] suggest numbering packets using acounter that has at least X + 1 values. Suppose instead that no packet can remain on thephysical channel for more than a bounded amount of time. S-89] exploits such a time boundto build a stabilizing Data Link protocol. The main idea is to use either numbered packets(counter ushing) or timers (timer ushing) to \ush" the physical channel of stale packets.315A stop and wait protocol is not very ecient over physical channels that have a hightransmission speed and/or high latency. It is easy to generalize a UDL to a Bounded StorageData Link or BDL that can store more than one packet.23.5 Local Checking and Correction in our MessagePassing ModelIn this section, we introduce formal denitions of local checkability and local correctability.The denitions for a message passing model will be slightly more complex than correspondingones for shared memory model because of the presence of channels between nodes.23.5.1 Link Subsystems and Local PredicatesConsider a network automaton with graph G.
Roughly speaking, a property is said to belocal to a subgraph G0 of G if the truth of the property can be ascertained by examiningonly the components specied by G0. We will concentrate on link subsystems that consistof a pair of neighboring nodes u and v and the channels between them. It is possible togeneralize our methods to arbitrary subsystems.In the following denitions, we x a network automaton N = Net(G N ).Denition 5 We dene the (u v) link subsystem of N as the composition of Nu , Cu v , Cv u ,and Nv .For any state s of N : sju denotes s projected on to node Nu and sj(u v) denotes sprojected onto Cu v . Thus when N is in state s, the state of the (u v) subsystem is the4-tuple: (sju sj(u v) sj(v u) sjv).A predicate L of N is a subset of the states of N .
Let (u v) be some edge in graph G ofN . A local predicate Lu v of N for edge (u v) is a subset of the states of the (u v) subsystemin N . We use the word \local" because Lu v is dened in terms of the (u v) subsystem.The following denition provides a useful abbreviation. It describes what it means for alocal property to hold in a state s of the entire automaton.Denition 6 We say that a state s of N satises a local predicate Lu v of N i(sju sj(u v) sj(v u) sjv) 2 Lu v :We will make frequent use of the concept of a closed predicate.
Intuitively, a property isclosed if it remains true once it becomes true. In terms of local predicates:Denition 7 A local predicate Lu v of network automaton N is closed if for all transitions(s s~) of N , if s satises Lu v then so does s~.316The following denitions provide two more useful abbreviations. The rst gives a name toa collection of local predicates, one for each edge in the graph.
The second, the conjunctionof a collection of \local properties", is the property that is true when all local properties holdat the same time. We will require that the conjunction of the local properties is non-trivial{ i.e., there is some global state that satises all the local properties.Denition 8 L is a link predicate set for N = Net(G N ) if for each (u v) 2 G there issome Lu v such that: If (a b c d) 2 Lu v then (d c b a) 2 Lv u . (i.e., Lu v and Lv u are identical except forthe way the states are written down.) L = fLu v (u v) 2 Gg There is at least one state s of N such that s satises Lu v for all Lu v 2 L.Denition 9 The conjunction of a link predicate set L is the predicate fs : s satises Lu vfor all Lu v 2 Lg.
We use Conj(L) to denote the conjunction of L.Note that Conj(L) cannot be the null set by the denition of a link predicate set.23.5.2 Local CheckabilitySuppose we wish a network automaton N to satisfy some property. An example would bethe property \all nodes have the same color".
We can often specify a property of N formallyusing a predicate L of N . Intuitively, N can be locally checked for L if we can ascertainwhether L holds by checking all link subsystems of N . The motivation for introducing thisnotion is performance: in a distributed system we can check all link subsystems in parallel inconstant time. We formalize the intuitive notion of a locally checkable property as follows.Denition 10 A network automaton N is locally checkable for predicate L using link predicate set L if: L is a link predicate set for N and L Conj(L). Each Lu v 2 L is closed.The rst item in the denition requires that L holds if a collection of local properties allhold. The second item is perhaps more surprising.
It requires that each local property alsobe closed.We add this extra requirement because in an asynchronous distributed system it appearsto be impossible to check whether an arbitrary local predicate holds all the time. Whatwe can do is to \sample" the local subsystem periodically to see whether the local property317holds. Suppose the network automaton consists of three nodes u, v and w and such thatv is the neighbor of both u and w. Suppose the property L that we wish to check is theconjunction of two local predicates Lu v and Lv w . Suppose further that exactly one of thetwo predicates is always false, and the predicate that is false is constantly changing.
Thenwhenever we \check" the (u v) subsystem we might nd Lu v true. Similarly whenever we\check" the (v w) subsystem we might nd Lv w true. Then we may never detect the factthat L does not hold in this execution. We avoid this problem by requiring that Lu v andLv w be closed.23.5.3 Local CorrectabilityThe motivation behind local checking was to eciently ensure that some property L holdsfor network automaton N . We would also like to eciently correct N to make the propertytrue. We have already set up some plausible conditions for local checking. Can we nd someplausible conditions under which N can be locally corrected?To this end we dene a local reset function f . This is a function with three arguments:the rst argument is a node say u, the second argument is any state of node automaton Nu,and the second argument is a neighbor v of u.
The function produces a state of the nodeautomaton corresponding to the rst argument. Let s be a state of N recall that sju is thestate of Nu . Then f (u sju v) is the state of Nu obtained by applying the local reset functionat u with respect to neighbor v. We will abuse notation by omitting the rst argument whenit is clear what the rst argument is.
Thus we prefer to write f (sju v) instead of the morecumbersome f (u sju v).We will insist that f meet two requirements so that f can be used for local correction(Denition 11).Assume that the property L holds if a local property Lu v holds for every edge (u v).The rst requirement is that if any (u v) subsystem does not satisfy Lu v , then applying fto both u and v should result in making Lu v hold. More precisely, let us assume that bysome magic we have the ability to simultaneously: Apply f to Nu with respect to v Apply f to Nv with respect to u Remove any packets stored in channels Cu v and Cv u.Then the resulting state of the (u v) subsystem should satisfy Lu v .
Of course, in a realdistributed system such simultaneous actions are clearly impossible. However, we will achieve318essentially the same eect by applying a so-called \reset" protocol to the (u v) subsystem.We will describe a stabilizing local reset protocol for this purpose in the next section.The rst requirement allows nodes u and v to correct the (u v) subsystem if Lu v does nothold.
But other subsystems may be correcting at the same time! Since subsystems overlap,correction of one subsystem may invalidate the correctness of an overlapping subsystem. Forexample, the (u v) and (v w) subsystems overlap at v. If correcting the (u v) subsystemcauses the (v w) subsystem to be incorrect, then the correction process can \thrash". Toprevent thrashing, we add a second requirement. In its simplest form, we might require thatcorrection of the (u v) subsystem leaves the (v w) subsystem correct if the (v w) subsystemwas correct in the rst place.However, there is a more general denition of a reset function f that turns out to be useful.Recall that we wanted to avoid thrashing that could be caused if correcting a subsystemcauses an adjacent subsystem to be incorrect.
Informally, let us say that the (u v) subsystemdepends on the (v w) subsystem if correcting the (v w) subsystem can invalidate the (u v)subsystem. If this dependency relation is cyclic, then thrashing can occur. On the other handif the dependency relation is acyclic then the correction process will eventually stabilize. Suchan acyclic dependency relation can be formalized using a partial order < on unordered pairsof nodes: informally, the (u v) subsystem depends on the (v w) subsystem if fv wg < fu vg.Using this notion of a partial order, we present the formal denition of a local resetfunction:Denition 11 We say f is a local reset function for network automaton N = net(G N )with respect to link predicate set L = fLu v g and partial order <, if for any state s of N andany edge (u v) of G: Correction: (f (sju v) nil nil f (sjv u)) 2 Lu v .
Stability: For any neighbor w of v,If (sju sj(u v) sj(v u) sjv ) 2 Lu v and fv wg 6< fu vg then(sju sj(u v) sj(v u) f (sjv w)) 2 Lu v .Notice that in the special case where all the link subsystems are independent, no edge is\less" than any other edge in the partial order.Using the denition of a reset function, we can dene what it means to be locally correctable.Denition 12 A network automaton N is locally correctable to L using link predicate setL, local reset function f , and partial order < if: N is locally checkable for L using L.319 f is a local reset function for N with respect to L and <.Intuitively, if we have a reset function f with partial order < we can expect the localcorrection to stabilize in time proportional to the maximum chain length in the partial order.Recall that a chain is a sequence a1 < a2 < a3 : : : < an.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
