Distributed Algorithms. Nancy A. Lynch (1993) (811416), страница 62
Текст из файла (страница 62)
Typically, we will be interested in proving stabilization propertiesonly for a special kind of automata: unrestricted automata. An unrestricted IOA (UIOA) isone in which all states of the IOA are also start states. Such an IOA models a system thathas been placed in an arbitrary initial state by an arbitrary initial fault.A possible modication (which is sometimes needed) is to only require (in Denitions2 and 1) that the sux of a behavior (execution) be a sux of a behavior (execution) ofthe target set. One problem with this modied denition is that we know of no good prooftechnique to prove that the behaviors (executions) of an automaton are suxes of a speciedset of behaviors (executions).By contrast, it is much easier to prove that every behavior of anautomaton has a sux that is in a specied set.
Thus we prefer to use the simpler denitionsfor what follows.23.3 Examples from Dijkstra's Shared Memory ModelIn Dijkstra's Dijkstra74] model, a network protocol is modeled using a graph of nite statemachines. In a single move, a single node is allowed to read the state of its neighbors,304compute, and then possibly change its state. In a real distributed system such atomiccommunication is impossible. Typically communication has to proceed through channels.While Dijkstra's original model is not very realistic, it is probably the simplest model of anasynchronous distributed system. This simple model provided an ideal vehicle for introducingDijkstra74] the concept of stabilization without undue complexity.
For this section, we willuse Dijkstra's original model to introduce two important and general techniques for selfstabilization: local checking and correction and counter ushing. In the next section, we willintroduce a more realistic message passing model.23.3.1 Dijkstra's Shared Memory Model and IOAHow can we map Dijkstra's model into the IOA model? Suppose each node in Dijkstra'smodel is a separate automaton. Then in the Input/Output automata model, it is not possibleto model the simultaneous reading of the state of neighboring nodes. The solution we useis to dispense with modularity and model the entire network as a single automaton.
Allactions, such as reading the state of neighbors and computing, are internal actions. Theasynchrony in the system, which Dijkstra modeled using a \demon", is naturally a part ofthe IOA model. Also, we will describe the correctness of Dijkstra's systems in terms ofexecutions of the automaton.Formally:A shared memory network automaton N for graph G = (E V ) is an automaton in which: The state of N is the cross-product of a set of node states, Su(N ), one for each nodeu 2 V . For any state s of N , we use sju to denote s projected onto Su . This is alsoread as the state of node u in global state s. All actions of N are internal actions and are partitioned into sets, Au(N ), one for eachnode u 2 V Suppose (s s~) is a transition of N and belongs to Au(N ).
Consider any state s0of N such that s0ju = sju and s0jv = sjv for all neighbors v of u. Then there is sometransition (s0 s~0) of N such that s~0jv = s~jv for u and all u's neighbors in G. Suppose (s s~) is a transition of N and belongs to Au(N ). Then sjv = s~jv for allv=6 u.Informally, the third condition requires that the transitions of a node u 2 V only dependon the state of node u and the states of of the neighbors of u in G. The fourth conditionrequires that the eect of a transition assigned to node u 2 V can only be to change thestate of u.305Top (Process n-1)0 up = false0 up = false0 up = falseToken1 up = true1 up = true.......1 up = trueBottom (Process 0)Figure 23.4: Dijktra's protocol for token passing on a line23.3.2 Dijkstra's Second Example as Local Checking and CorrectionIn this section, we will begin by reconsidering the second example in Dijkstra74].
Thederivation here is based on some unpublished work I did with Anish Arora and MohamedGouda at the University of Texas. This protocol is essentially a token passing protocol on aline of nodes with process indices ranging from 0 to n ; 1. Imagine that the line is drawnvertically so that process 0 is at the bottom of the line (and hence is called \bottom") andProcess n ; 1 is at the top of the line (and called \top"). This is shown in Figure 23.4. Thedown neighbor of Process i is Process i ; 1 and the up neighbor is Process i + 1. Processn ; 1 and Process 0 are not connected.Dijkstra observed that it is impossible (without randomization) to solve mutual exclusionin a stabilizing fashion if all processes have identical code. To break symmetry, he made thecode for the \top" and \bottom" processes dierent from the code for the others.Dijkstra's second example is modeled by the automaton D2 shown in Figure 23.5.
Eachprocess i has a boolean variable upi, and a bit xi. Roughly, upi is a pointer at node i thatpoints in the direction of the token, and xi is a bit that is used to implement token passing.Figure 23.4 shows a state of this protocol when it is working correctly.
First, there can beat most two consecutive nodes whose up pointers dier in value and the token is at one ofthese two nodes. If the two bits at the two nodes are dierent (as in the gure) then thetoken is at the upper node else the token is at the lower node.306The state of the system consists of a boolean variableup and a bit x , one for every process in the line.We will assume that up0 = true and up ;1 = false by denitioniinIn the initial state x = 0 for i = 0 : : :n ; 1 and up = false for i = 1 : : :n ; 1iiMove Up0 (*action for the bottom process only to move token up*)Precondition: x0 = x1 and up1 = falseEect: x0 := x0Move Down ;1 (*action for top process only to move token down*)Precondition: x ;2 =6 x ;1nnEects:xn;1 := x ;2nnMove Up 1 i n ; 2 (*action for other processes to move token up*)Precondition: x =6 x ;1iiiEects:x := x ;1up := true (*point upwards in direction token was passed*)iiiMove Down 1 i n ; 2 (*action for other processes to move token down*)iPrecondition: x = x +1 and up = true and up +1 = falseEect: up := false (*point downwards in direction token was passed*)iiiiiAll actions are in a separate class.Figure 23.5: Automaton D2: a version of Dijkstra's second example with initial states.
Theprotocol does token passing on a line using nodes with at most 4 states.307For the present, assume that all processes start with xi = 0. Also, initially assumethat upi = false for all processes other than process 0. We will remove the need for suchinitialization below. We start by understanding the correct executions of this protocol whenit has been correctly initialized.A process i is said to have the token when any action at Process i is enabled.
As usual thesystem is correct when there is at most one token in the system. Now, it is easy to see thatin the initial state only Move Up0 is enabled. Once node 0 makes a move, then Move Up1is enabled followed by Move Up2 and so on as the \token" travels up the line. Finally thetoken reaches node n ; 1, and we reach a state s in which xi = xi+1 for i = 0 : : : n ; 3 andxn;1 6= xn;2. Also in state s, upi = true for i = 0 : : : n ; 2 and upn;1 = false. Thus in states, Move Downn;1 is enabled and the token begins to move down the line by executingMove Downn;2 followed by Move Downn;3 and so on until we reach the initial stateagain.
Then the cycle continues. Thus in correct executions, the \token" is passed up anddown the line.We describe these \good states" of D2 (that occur in correct executions) in terms of localpredicates. In the shared memory model, a local predicate is any predicate that only refersto the state variables of a pair of neighbors. Thus in a good state of D2 , two properties aretrue for any Process i other than 0: If upi;1 = upi then xi;1 = xi. If upi = true then upi;1 = true.First, we prove that if these two local predicates hold for all i = 1 : : : n ; 1, then thereis exactly one action enabled. Intuitively, since upn;1 = false and up0 = true, we can startwith process n ; 1 and go down the line until we nd a pair of nodes i and i ; 1 suchthat upi = false and upi;1 = true.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
