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:

AsynchronousBroadcast

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

tasks

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 AsynchronousBroadcast_m, one for each m:

AsynchronousBroadcast,,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

tasks

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 DistributeAsynchronousBroadcast_m(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 AsynchronousBroadcast_m. If we want to simulate the full AsynchronousBroadcast automaton, we just compose together all the automata for all m.

DistributedAsynchronousBroadcast,,m,,(p)

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

tasks

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

tasks

each output action is a separate task

Now we'll do a simulation argument that shows that the composition of (a) DistributedAsynchronousBroadcast_m(p) for all p and (b) ReliableReorderingChannel_m(p,p') for all (p,p') in the graph simulates AsynchronousBroadcast_m. To avoid excessive typing, we'll drop the m's and abbreviate DistributedAsynchronousBroadcast_m(p) as Dp, ReliableReorderingChannel_m(p,p') as C(p,p'), and AsynchronousBroadcast_m as AB. The simulation map f sets AB.sent = max_p 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').sent^old + 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 AsynchronousBroadcast_m to put all deliveries of the same task in the same partition, and everything would still work.)

CategoryDistributedComputingNotes