Note: You are looking at a static copy of the former PineWiki site, used for class notes by James Aspnes from 2003 to 2012. Many mathematical formulas are broken, and there are likely to be other bugs as well. These will most likely not be fixed. You may be able to find more up-to-date versions of some of these notes at http://www.cs.yale.edu/homes/aspnes/#classes.

For more up-to-date notes see http://www.cs.yale.edu/homes/aspnes/classes/465/notes.pdf.

(See Flooding for a simpler version of these notes that don't do IOAutomata.)

Let's define asynchronous broadcast to mean simulating the following AsynchronousBroadcast automaton with the following specification:

states

vectors sent: {0,1}{M} and delivered: {0,1}{M×P}, where M is the message set and P is the set of processes, initially all 0

input actions
send(m,p)
effect: sent[m] := 1
output actions
deliver(m, p)
precondition: sent[m] = 1, delivered[m,p] = 0; effect: delivered[m,p] := 1
each output action is a separate task

Note that this specification only delivers a message once no matter how many times it is sent. We have a separate send(m,p) action for each process p, because we want to allow a broadcast to start any any process (maybe even at more than one process); if there was a single send(m) action that was an input to all processes we'd have already solved in our model the problem we wanted to solve in practice.

We can simplify the specification further by observing that the AsynchronousBroadcast automaton is the composition of the following broadcast automata AsynchronousBroadcastm, one for each m:

states
bit sent: {0,1} and vector delivered: {0,1}^{P}, where P is the set of processes, initially all 0
input actions
send(m,p)
effect: sent := 1
output actions
deliver(m, p)
precondition: sent = 1, delivered[p] = 0; effect: delivered[p] := 1
each output action is a separate task

Here's a distributed protocol for doing asynchronous broadcast in a weakly-connected graph. What we'll do is define a separate DistributeAsynchronousBroadcastm(p) automaton for each process p, and then argue that the composition of these automata together with a collection of reliable reordering channel automata for all p simulates AsynchronousBroadcastm. If we want to simulate the full AsynchronousBroadcast automaton, we just compose together all the automata for all m.

states
bit sent: {0,1} and vector delivered: {0,1}^{neighbors union {p}}, initially all 0
input actions
send(m,p)
effect: sent := 1
recv(p',p,m)
effect: sent := 1
output actions
send(p, p', m)
precondition: sent = 1, delivered[p'] = 0; effect: delivered[p'] := 1
deliver(m, p)
precondition: sent = 1, delivered[p] = 0; effect: delivered[p] := 1
each output action is a separate task

For completeness, we'll also throw in the ReliableReorderingChannel as a composition of message-specific channels:

ReliableReorderingChannel,,m,,(p,p')
states
counts sent: N and delivered: N, initially both 0
input actions
send(p,p',m)
effect: sent := sent + 1
output actions
recv(p, p', m)

precondition: sent > delivered; effect: delivered := delivered + 1

each output action is a separate task

Now we'll do a simulation argument that shows that the composition of (a) DistributedAsynchronousBroadcastm(p) for all p and (b) ReliableReorderingChannelm(p,p') for all (p,p') in the graph simulates AsynchronousBroadcastm. To avoid excessive typing, we'll drop the m's and abbreviate DistributedAsynchronousBroadcastm(p) as Dp, ReliableReorderingChannelm(p,p') as C(p,p'), and AsynchronousBroadcastm as AB. The simulation map f sets AB.sent = maxp Dp.sent and AB.delivered[p] = Dp.delivered[p]. The simulation map ignores the contents of the channels

For the initial state s, we have f(s).sent = 0 and f(s).delivered[p] = 0 for all p, since all the Dp's are full of zeroes and we don't care about the state of the channels. We'd like to verify that it continues to work for all operations, but to do this we first need to prove some invariants:

Channel input invariant
C(p,p').sent = Dp.delivered[p'].
Proof

Initially, both are 0. The only action that changes either value is send(p,p',m), which has precondition Dp.delivered[p'] = 0 implying C(p,p').sent = 0 by the invariant. After the operation, we set Dp.delivered[p'] := 1 and C(p,p').sent := C(p,p').sentold + 1 = 1, so the invariant is preserved.

Channel delivery invariant

C(p,p').delivered <= C(p,p').sent.

Proof
True initially, not affected by send(p,p',m), enforced by precondition of C(p,p') on recv(p,p',m).
Channel output invariant

C(p,p').delivered <= Dp.sent.

Proof

Again, it's true in the initial state. From the input and delivery invariants we have that C(p,p').delivered <= C(p,p').sent = Dp.delivered[p'] <= 1. So we only have to worry about what happens when C(p,p').delivered changes from 0 to 1 (=> recv(p,p',m) sets Dp.sent to 1 and preserves the invariant) or Dp.sent changes from 0 to 1 (possibly as the result of a different recv or send message---again invariant is preserved because RHS increases).

Process output invariant

Dp.delivered[p'] <= Dp.sent.

Proof
Yet another trivial variation of the preceding proofs.

From this we get the consolidated invariant Dp.sent >= Dp.delivered[p'] = C(p,p').sent >= C(p,p').delivered. (Technically we don't need the channel output invariant here, but we may need it later.) We can now show the simulation map works, by looking at the actions that change the state of some process. The easy part is showing that f(s).delivered[p] = s.Dp.delivered[p] works, because the only action that changes Dp.delivered[p] in the distributed system is deliver(p,m), and its precondition and effects in Dp line up exactly with the precondition and effects of deliver(p,m) in AB. Trickier is f(s).sent. There are two ways that f(s).sent could change from 0 to 1: either Dp.sent := 1 because of a send(m,p) operation (OK) or Dp.sent := 1 because of a recv(p',p,m) operation (maybe not OK). But in the latter case the precondition on recv(p',p,m) is C(p',p).sent > C(p',p).delivered >= 0 implying C(p',p).sent >= 1, and thus Dp'.sent >= C(p',p).sent = 1 in the previous state. This gives f(s).sent = 1 and so there is no change, allowing recv(p',p,m) to map to an empty trace.

So far we've just proved safety. To prove liveness, i.e. that every enabled deliver(m,p) operation eventually happens, we argue from the invariants that for every adjacent pair of processes (p,p') with Dp.sent = 1 and Dp.sent = 0, either Dp.deliver[p'] = 0 or C(p,p').sent > C(p,p').delivered. Then if {p': Dp'.sent = 0} is not empty, there is some p' in this set that is adjacent to a process p with Dp.sent = 1, and after some finite amount of time (a) p issues send(p,p',m) and (b) C(p,p') issues recv(p,p',m). At this point p' is added to the set. Repeating the argument gives that Dp.sent = 1 eventually for all p. It follows that deliver(m,p) is continuously enabled for any p that hasn't received the message yet, and so eventually it occurs by the fairness assumption.

(Comment: since only finitely many deliver(m,p) messages occur, we could weaken the task partition for AsynchronousBroadcastm to put all deliveries of the same task in the same partition, and everything would still work.)

2014-06-17 11:57