Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 63
Текст из файла (страница 63)
Consider the rst such pair. Then the second predicateguarantees us that there is exactly one such pair. The rst predicate then guarantees thatall nodes j < i ; 1 have xj = xi;1 and all nodes k > i have xk = xi. Thus only one action isenabled. If xi = xi;1 and i ; 1 6= 0 then only Move Downi;1 is enabled. If xi = xi;1 andi ; 1 = 0 then only Move Up0 is enabled. If xi 6= xi;1 and i 6= n ; 1 then only Move Upiis enabled.
If xi 6= xi;1 and i = n ; 1 then only Move Downn;1 is enabled.Similarly we can show that if exactly one action is enabled then all local predicates hold.Thus if the system is in a bad state, some pair of neighbors will be able to detect this fact.Hence we conclude that D2 is locally checkable. However, we would like to go even furtherand be able to correct the system to a good state by adding extra correction actions to eachnode. If we can add correction actions so that all link predicates will eventually become true,308then we say that the D2 is also locally correctable. Adding local correction actions is trickybecause the correction actions of nodes may \interfere" and result in a form of \thrashing".However, a line is a special case of a tree with (say) 0 as the root each node i other than0, can consider i ; 1 to be its parent.
The tree topology suggests a simple correction strategy.For each node i 6= 0, we can add a new action Correct Childi (which is a separate class foreach i). Basically, Correct Childi checks whether the link predicate on the link betweeni and its parent is true. If not, i changes its state such that the predicate becomes true.Notice that Correct Childi leaves the state of i's parent unchanged. Suppose j is theparent of i and k is the parent of j . Then Correct Childi will leave the local predicateon link (j k) true if it was true in the previous state.Thus we have an important stability property: correcting a link does not aect thecorrectness of links above it in the tree. Using this it is easy to see that eventually all linkswill be in a good state and so the system is in a good state. We will ignore the details ofthis proof but the basic idea should be clear.
Dijkstra's actual code does not use an explicitcorrection action. However, we feel that this way of understanding his example is clearerand illustrates a general method. The general method of local checking and correction wasrst introduced in APV-91].23.3.3 Dijkstra's rst example as Counter FlushingThe counter ushing paradigm described in this section is taken from V92].Dijkstra's rst example is modeled by the automaton D2 shown in Figure 23.6. As inthe previous example, the nodes (once again numbered from 0 to n ; 1) are arranged suchthat node 1 has node 0 and node 2 as its neighbors and so on.
However, in this case wealso assume that Process 0 and n ; 1 are neighbors. In other words, by making 0 and n ; 1adjacent we have made the line into a ring. For process i, let us call Process i ; 1 (we assumethat all arithmetic on indices and counters is mod n) the counter-clockwise neighbor of i andi + 1 the clockwise neighbor of i.Each node has a counter counti in the range 0 : : : n that is incremented mod n + 1. Onceagain the easiest way to understand this protocol is to understand what happens when itis properly initialized.
Thus assume that initially Process 0 has its counter set to 1 whileall other processes have their counter set to 0. Processes other than 0 are only allowedto \move" (see Figure 23.6) when their counter diers in value from that of their counterclockwise neighbor in this case, the process is allowed to make a move by setting its counterto equal that of its counter-clockwise neighbor. Thus initially, only Process 1 can make amove after which Process 1 has its counter equal to 1 next, only Process 2 can move, afterwhich Process 2 sets its counter equal to 1 and so on, until the value 1 moves clockwise309The state of the system consists of an integer variablecount 2 f0 : : :ng, one for every process in the ring.We assume that Process 0 and n ; 1 are neighborsiIn the initial state count = 0 for i = 1 : : :n ; 1 and count1 = 1iMove0 (*action for Process 0 only *)Precondition: count0 = count ;1 (*equal to counter-clockwise neighbor?*)Eect: count0 := (count0 + 1) mod (n + 1) (*increment counter*)nMove 1 i n ; 1 (*action for other processes*)Precondition: count =6 count ;1 (*not equal to counter-clockwise neighbor?*)iiiEects:count := count ;1(*set equal to counter-clockwise neighbor*)iiAll actions are in a separate classFigure 23.6: Automaton D1: a version of Dijkstra's rst example with initial states.
Theprotocol does token passing on a ring using nodes with n states.around the ring until all processes have their counter equal to 1.Process 0 on the other hand cannot make a move until Process n ; 1 has the same countervalue as Process 0. Thus until Process 1 sets its counter to 1, Process 0 cannot make a move.However, when this happens, Process 1 increments its counter mod n + 1. Then the cyclerepeats as now the value 2 begins to move across the ring (assuming n > 2) and so on. Thusafter proper initialization, this system does perform a form of token passing on a ring eachnode is again considered to have the token, when the system is in a state in which the nodecan take a move.It is easy to see that the system is in a good state i the following local predicates aretrue.
For i = 1 : : : n ; 1, either counti;1 = counti or counti;1 = counti + 1. Either count0 = countn;1 or count0 = countn;1 + 1.The system is locally checkable but it does not appear to be locally correctable. However,it does stabilize using a paradigm that we can call counter ushing. Even if the counter valuesare arbitrarily initialized (in the range 0 : : : n) the system will eventually begin executingas some sux of a properly initialized execution. We will prove this informally using threeclaims:310 In any execution, Process 0 will eventually increment its counter.
Supposenot. Then since Process 0 is the only process that can \produce" new counter values,the number of distinct counter values cannot increase. If there are two or more distinctcounter values, then moves by Processes other 0 will reduce the number of distinctcounter values to 1, after which Process 0 will increment its counter. In any execution, Process 0 will eventually reach a \fresh" counter valuethat is not equal to the counter values of any other process. To see this, notethat that in the initial state there are at most n distinct counter values.
Thus thereis some counter value say m that is not present in the initial state. Since, process 0keeps incrementing its counter, Process 0 will eventually reach m and in the interimno other process can set their counter value to m. Any state in which Process 0 has a fresh counter value m is eventually followed by astate in which all processes have counter value m. It is easy to see that the value mmoves clockwise around the ring \ushing" any other counter values, while Process 0remains at m.
This is why I call this paradigm counter ushing.The net eect is that any execution of D1 eventually reaches a good state in which itremains. The general counter ushing paradigm can be stated roughly as follows: A sender (in our case, Process 0) periodically sends a message to a set of respondersafter all responders have received the message the sender sends the next message (thiscorresponds to one cycle around the ring in our case).
To make the protocol stabilizing, the sender numbers each message with a counter.The size of the counter must be greater than the maximum number of distinct countervalues that can be present in the network in any state. The sender increments itscounter after the message has reached all responders. The protocol must ensure that the sender counter value will always increment andso eventually reach a \fresh" value not present in the network. A freshly numberedmessage m from the sender must guarantee that all old counter values will be \ushed"from the network before the sender sends the next message.In Dijkstra's rst example, the ushing property is guaranteed because the topologyconsists of a ring of unidirectional links.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
