6.852 Lecture 7●Asynchronous systems●Formal model–I/O automata–behaviors–simulations–composition●Reading: Chapter 8Asynchronous systems●No timing assumptions–no rounds●Asynchronous networks–nodes communicating via channels●Asynchronous shared memory–processes communicating via shared objectsp1C1,2p2C2,1send(m)1,2send(m)2,1receive(m)1,2receive(m)2,1init(v)1decide(v)1Asynchronous networkSpecifying problems and systems●Processes and channels are automata–take actions to change state–reactive●interact with environment via input and output actions●not just map from input values to output values●Behavior–we observe externally visible actions●state is hidden–interleaving semantics●behavior is sequence of actions–problems specify allowable behaviorsInput/output automaton●General mathematical model–very little structure●Designed for “structured” system description–composition–hierarchical description/reasoning●Supports good proof techniques–invariants–simulation relations–compositional reasoningInput/output automaton●State transition system–transitions labeled by actions●Actions classified as input, output, internal–input, output are externally visible–output, internal are locally controlledInput/output automaton●sig(A) = ( in(A), out(A), int(A) )–input, output, internal actions (disjoint)–acts(A) = in(A) ∪ out(A) ∪ int(A)●states(A)●start(A) ⊆ states(A)●trans(A) ⊆ states(A) × acts(A) × states(A)–input-enabled●tasks(A), partition of local(A)–needed for livenessInput/output automaton●A step of an automaton is an element of trans●Action π is enabled in a state s –if there is a step (s, π,s') for some s'●I/O automata must be input-enabled–every input action is enabled in every state–captures idea that automaton cannot control inputs–enables compositional reasoning●tasks correspond to “threads of control”–used to define fairness–needed to guarantee livenessChannel automaton●Reliable unidirectional FIFO channel for 2 processes–fix message “alphabet” M●signature–input actions: send(m) for m ∈ M–output actions: receive(m) for m ∈ M–no internal actions●states –queue: FIFO queue of M, initially emptyCsend(m) receive(m)Channel automaton●trans–send(m)●effect: add m to (end of) queue–receive(m)●precondition: m is at head of queue●effect: remove head of queue●tasks–all receive actions in one taskCsend(m) receive(m)Channel automaton●trans–send(m)i,j●effect: add m to (end of) queue–receive(m)i,j●precondition: m is at head of queue●effect: remove head of queue●tasks–all receive actions in one taskCi,jsend(m)i,jreceive(m)i,jpipjExecutions●An I/O automaton executes as follows:–start at some start state–repeatedly take step from current state to new state●Formally, an execution is a sequence:–s0 π1 s1 π2 s2 π3 s3 π4 s4 π5 s5 ... (if finite, end in state)–s0 is a start state–(si, π+1i, si+1) is a step (i.e., in trans)λ, send(a), a, send(b), ab, receive(a), b, receive(b), λExecutions●An I/O automaton executes as follows:–start at some start state–repeatedly take step from current state to new state●Formally, an execution is a sequence:–s0 π1 s1 π2 s2 π3 s3 π4 s4 π5 s5 ... (if finite, end in state)–s0 is a start state–(si, π+1i, si+1) is a step (i.e., in trans)λ, send(a), a, send(b), ab, receive(a), b, receive(b), λexecution fragmentInvariants and reachable states●A state is reachable if it appears in some execution.–equivalently, at the end of some finite execution●An invariant is a predicate that is true on every reachable state.–main tool for proving properties of concurrent algorithms–typically prove by induction on length of executionTraces●A trace of an execution is the subsequence of external actions in the execution–denoted trace(α), where α is an execution–models “observable behavior”λ, send(a), a, send(b), ab, receive(a), b, receive(b), λsend(a), send(b), receive(a), receive(b)Trace properties●A trace property P is a pair of:–sig(P): external signature (i.e., no internal actions)–traces(P): set of sequences of actions in sig(P)–can specify allowable behaviors●Automaton A satisfies trace property P if–extsig(A) = sig(P) and traces(A) ⊆ traces(P)–extsig(A) = sig(P) and fairtraces(A) ⊆ traces(P)Automata as specifications●Every I/O automaton specifies a trace property–(extsig(A), traces(A))–we can use an automaton as a problem specification●Hierarchical proofs–important strategy for proving correctness of complex asychronous distributed algorithms–automaton A implements B if●extsig(A) = extsig(B)●traces(A) ⊆ traces(B)–define a series of automata, each implementing the next●first automaton models algorithm/system; last captures specSimulation relations●Most common method to prove one automaton implements another●Similar to technique for synchronous algorithms–map states in one to states of other–show correspondence holds initially, is preserved each round–also similar to abstraction function for data type implementation●R is a simulation relation from A to B provided:–sA ∈ start(A) implies there exists sB ∈ start(B) such that sA R sB–if sA, sB are reachable states of A and B, sA R sB and (sA, π, s'A) is a step, then there exists an exec fragment β starting with sB and ending in s'B such that s'B R s'A and trace(π) = trace(β)Simulation relations●R is a simulation relation from A to B provided:–sA ∈ start(A) implies there exists sB ∈ start(B) such that sA R sB–if sA, sB are reachable states of A and B, sA R sB and (sA, π, s'A) is a step, then there exists an exec fragment β starting with sB and ending in s'B such that s'B R s'A and trace(π) = trace(β)sAs'AsBs'BR R πβSimulation relations●Theorem: If there is a simulation relation from A to B then traces(A) ⊆ traces(B).s0,Aπ1s1,Aπ2s2,Aπ3s3,Aπ4s4,Aπ5s5,ASimulation relations●Theorem: If there is a simulation relation from A to B then traces(A) ⊆ traces(B).s0,As0,BRπ1s1,Aπ2s2,Aπ3s3,Aπ4s4,Aπ5s5,ASimulation relations●Theorem: If there is a simulation relation from A to B then traces(A) ⊆ traces(B).s0,As0,BR π1β1s1,As1,BRπ2s2,Aπ3s3,Aπ4s4,Aπ5s5,ASimulation relations●Theorem: If there is a simulation relation from A to B then traces(A) ⊆ traces(B).s0,As0,BR π1β1s1,As1,BR π2β2s2,As2,BR