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

integer r integer s integer r + 1.2. All packets in queue sr have integer tag at most equal tointeger s .3. All packets in queue sr with integer tag equal tointeger s have their message components equal to the rstmessage of buer s.4. All packets in queue rs have integer tag at most equal tointeger r .5. If integer s appears anywhere other than the sender'sstate, then buer s is nonempty.To show the safety property, show that every behavior of theimplementation is also a behavior of the spec.Do this by using a forward simulation | actually, a renement.Specically,If s and u are states of the implementation and specicationrespectively, then we dene u = r(s) provided thatu:queue is determined as follows:1. If s:integer s = s:integer r , then u:queueis obtained by rst removing the rst element of s:buer s andthen concatenating s:buer r and the \reduced"buer s.(Invariant implies that s:buer s is nonempty.)2. Otherwise, u:queue is just the concatenation ofs:buer r and s:buer s.Now we show that r is a renement.The correspondence of initial states is easy because all queues are empty.Inductive step:380Given (s s0), and u = r(s), we consider the following cases.1.

send msg (m):Let u0 = r(s0).We must show that (u u0) is a step of MQ.This is true because the send msg event modies both queues in the same way.receive msg (m):Let u0 = r(s0). We must show (u u0) is a step of MQ. Since is enabled in s, m is rst on s:buer r , so mis also rst on u:queue r , so is also enabled in u.Both queues are modied in the same way.3. send pkt :Then we must show that u = r(s0).This is true because the action doesn't change the virtual queue.4. receive pkt tr (m i):We show that u = r(s0).The only case of interest is if the packet is accepted.This means i = s:integer r + 1, so by Lemma1, in state s, integer s = integer r + 1,so r(s) = u is the concatenation of s:buer r ands:buer s.Then in s0, the integers are equal, and m is added to the end ofbuer r .So r(s0) is determined by removing the rst element ofs0:buer sand then concatenating with s0:buer r .Then in order to see that r(s0) is the same as u, it suces to notethat m is the same as the rst element in s:buer s.But Lemma 1 implies that i = s:integer s,and that m is the same as the rst element in s:buer s, as needed.4.

receive pkt rt(i):Again we show that u = r(s0).The only case of interest is if the packet is accepted.This means i = s:integer s, which implies by Lemma3811 that s:integer s = s:integer r .This means that r(s) is the concatenation ofs:buer r and s:buer s, with the rst element ofs:buer s removed.Then s0:integer s = s0:integer r + 1, so r(s0) is justthe concatenation of s0:buer s and s0:buer r .But s0:buer s is obtained from s:buer s by removingthe rst element, so that r(s0) = u.Since r is a renement, all behaviors of Stenning's protocol arealso behaviors of the specication automaton, and so satisfy thesafety property that the sequence of messages in receive msg events isconsistent with the sequence of messages in send msg events.In particular, the fair behaviors of Stenning's protocol satisfy this safetyproperty.Liveness:The basic idea is that we rst show a correspondence between anexecution of the impl and of the spec MQ.We can get this by noticing that forward simulation actually yields astronger relationship than just behavior inclusion { executioncorrespondence lemma gives a correspondence between states andexternal actions throughout the execution.Then suppose that the liveness condition of the specication isviolated.That is, the abstract queue is nonempty from some point in theexecution, but no receive-message events ever occur.We consider what this means in the implementation execution.If the buer r is ever nonempty, then eventually delivermessage, contradiction, so can assume that buer r is always empty.Then buer s must be nonempty throughout the executionsender keeps sending packets for the rst message on buer s,gets delivered to receiver by channel fairness, then putin buer r , which is a contradiction.382A.1.2 Alternating Bit ProtocolOptimized version of Stenning's protocol that doesn't use sequencenumbers, but only Boolean values.These get associated with successive messages in an alternatingfashion.This only works for channels with stronger reliability conditions:assume channels exhibit loss and duplication, but no reordering.Liveness again says that innitely many sends lead to receives ofinnitely many of the sent packets.Sender keeps trying to send a message with a bit attached.When it gets an ack with the same bit, it switches to the opposite bitto send the next message.Receiver is also always looking for a particular bit.Code: (see Figures A.3,A.4).Correctness Proof:Model the sender and receiver as IOA's, just as before.Again, the channels are not quite IOA's, because of the fairnessconditions being dierent from usual IOA fairness.But it is again convenient to have a state machine with a livenessrestriction.This time, the channel state machine has as its state a queue.A send puts a copy of the packet at the end of the queue,and a receive can access any element of the queue when itdoes, it throws away all the preceding elements, but not theelement that is delivered.This allows for message loss and duplication.Again, need a liveness condition to say that any packet that is sentinnitely many times is also delivered innitely many times.A convenient correctness proof can be based on a forward simulation (thisone is multi-valued) to a restricted version of Stenning's protocol,which we call FIFO-Stenning.This restricted version is correct because the less restricted version is.383Interface:Input:send msg (m) m 2 Mreceive pkt rt (b) b a BooleanOutput:send pkt tr (m b) m 2 M b a BooleanThe state consists of the following components:buer , a nite queue of elements of M , initially empty, andag , a Boolean, initially 1.The steps are:send msg (m) m 2 MEect:add m to buer .send pkt tr (m b) m 2 M b a BooleanPrecondition:m is rst on buer .b = agEect:None.receive pkt rt(b) b a BooleanEect:if b = ag thenremove rst element (if any) from buer ag := ag + 1 mod 2]Partition:all send pkt tr actions are in one class.Figure A.3: ABP Sender As384Interface:Input:receive pkt tr (m b) n 2 M b a BooleanOutput:receive msg (m) m 2 Msend pkt rt (b) b a BooleanState:buer , a nite queue of elements of M , initially empty, andag , a Boolean, initially 0.Steps:receive msg (m) m 2 MPrecondition:m is rst on buer .Eect:remove rst element from buer .receive pkt tr (m b) m 2 M b a BooleanEect:if b 6= ag thenadd m to buer ag := ag + 1 mod 2]send pkt rt(b) b a BooleanPrecondition:b = agEect:None.Partition:all send pkt rt actions are in one class, andall receive msg actions are in another class.Figure A.4: ABP Receiver Ar385The restricted version is based on the FIFO channels described aboveinstead of arbitrary channels.Use an additional invariant about this restricted version of thealgorithm:Lemma 2 The following is true about every reachable state of the FIFO-Stenningprotocol.Consider the sequence consisting of the indices in queue rs(in order from rst to last on the queue),followed by integer r ,followed by the indices in queue sr ,followed by integer s.

(In other words, the sequencestarting at queue rs, and tracing the indices all the wayback to the sender automaton.)The indices in this sequence are nondecreasing furthermore, the dierencebetween the rst and last index in this sequence is at most 1.Proof: The proof proceeds by induction on the number of steps in the niteexecution leading to the given reachable state.The base case is where there are no steps, which means we have to showthis to be true in the initial state.In the initial state, the channels are empty, integer s = 1 andinteger r = 0.Thus, the specied sequence is 0 1, which has the required properties.For the inductive step, suppose that the condition is true in state s,and consider a step (s s0) of the algorithm.We consider cases, based on .1. is a send msg or receive msg event.Then none of the components involved in the stated condition is changedby the step, so the condition is true after the step.2.

is a send pkt tr (m i) event, for some m.Then queue sr is the only one of the four relevant components ofthe global state that can change.We have s0:queue sr equal to s:queue sr with the additionof (m i).But i = s:integer s by the preconditions of the action.386Since the new i is placed consecutively in the concatenated sequence withs0:integer s = i, the properties are all preserved.3. is a receive pkt rt(i) event.If i 6= s:integer s then the only change is to remove some elementsin the concatenated sequence, so all properties are preserved.On the other hand, if i = s:integer s then the inductive hypothesisimplies that the entire concatenatedsequence in state s must consist of i's.The only changes are to remove some elements from the beginning of thesequence and add one i + 1 to the end (since s0:integer s = i + 1,by the eect of the action).

Thus, the new sequence consists ofall i's followed by one i + 1, so the property is satised.4. is a send pkt rt event.Similar to the case for send pkt tr.5. is a receive pkt tr (m i) event.If i 6= s:integer r + 1 then the only change is to remove someelements from the concatenated sequence, so all properties are preserved.On the other hand, if i = s:integer r + 1then the inductive hypothesis implies that the entire concatenatedsequence in state s must consist of i ; 1's up to and includings:integer r , followed entirely by i's.The only changes are to remove some elements from the sequence andchange the value of integer r from i ; 1to i, by the eect of the action this still has the required properties.Now we will show that the ABP is correctby demonstrating a mapping from ABP to FIFO-Stenning.This mapping will be a multivalued \possibilities mapping", i.e., aforward simulation.In particular, it will ll in the integer values of tags only workingfrom bits.More precisely, we say that a state u of FIFO-Stenning is in f (s)for state s of ABP provided that the following conditions hold.3871.

s:buer s = u:buer sand s:buer r = u:buer r .2. s:ag s = u:integer s mod 2and s:ag r = u:integer r mod 2.3. queue sr has the same number of packets in s and u.Moreover, for any j , if (m i) is the j th packet inqueue sr in u,then (m i mod 2) is the j th packet in queue sr in s.Also, queue rs has the same number of packets in s and u.Moreover, for any j , if i is the j th packet inqueue rs in u,then i mod 2 is the j th packet in queue rs in s.Theorem 3 f above is a forward simulation.Proof: By induction.For the base, let s be the start state of ABP and u the start stateof FIFO-Stenning.First, all the buers are empty.Second, s:ag s = 1 = u:integer s mod2and s:ag r = 0 and u:integer r = 0, which is as needed.Third, both channels are empty.This suces.Now show the inductive step.Suppose (s s0) is a step of ABP and u 2 f (s).We consider cases based on .1.

= send msg (m)Choose u0 to be the unique state such that (u u0) is a step ofFIFO-Stenning.We must show that u0 2 f (s0).The only condition that is aected by the step is the rst, for thebuer s component.However, the action aects both s:buer s and u:buer sin the same way, so the correspondence holds.3882. = receive msg (m)Since is enabled in s, m is the rst value on s:buer r .Since u 2 f (s), m is also the rst value on u:buer r ,which implies that is enabled in u.Now choose u0 to be the unique state such that (u u0) is a step ofFIFO-Stenning.All conditions are unaected except for the rst for buer r , andbuer r is changedin the same way in both algorithms, so the correspondence holds.3. = send pkt tr (m b)Since is enabled in s,b = s:ag s and m is the rst element on s:buer s.Let i = u:integer s .Since u 2 f (s), m is also the rst element on u:buer s.It follows that $ = send pkt tr (m i) is enabled in u.Now choose u0 so that (u $ u0) is a step of FIFO-Stenning.We must show that u0 2 f (s0).The only interesting condition is the third, for C sr .By inductive hypothesis and the fact that the two steps each insertone packet, it is easy to see thatC sr has the same number of packets in s0 and u0.Moreover, the new packet gets added with tag i in state u0 and withtag b in state s0since u 2 f (s), we have s:ag s = u:integer s mod 2,i.e., b = i mod 2,which implies the result.4.