6.852 Lecture 8●Finish up formal model–fairness–composition●Basic asynchronous network algorithms●Reading: Chapters 8 (continued), 14, 15●Next lecture: Finish Chapter 15.Last lecture●Defined I/O automaton model–sig(A): input, output, internal actions–states(A) (typically defined by state variables)–start(A) ⊆ states(A)–trans(A) ⊆ states(A) × acts(A) × states(A) (“steps”)●typically defined using precondition-effect form–tasks(A): fairness partition (must be countable)–defined executions, traces●Hierarchical proofs and simulation relations–automata as specs: prove one automaton implements another●Safety and liveness propertiesFairness●Task (set of actions) corresponds to “thread of control”–used to define “fair” executions●a “thread” that is continuously enabled gets to take a step–needed to prove liveness●Formally, an execution α is fair to C ∈ tasks (A) if:–α is finite and C is not enabled in final state–α is infinite and either●infinitely many events in C occur in α; or●C is not enabled in infinitely many states in αSpecifications●Trace property: Problem specification –( sig(P), traces(P) )●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–( extsig(A), traces(A) )●use simulation relations to prove–( extsig(A), fairtraces(A) )Safety and liveness●Safety property: “bad” thing doesn't happen–nonempty (null trace is always safe)–prefix-closed: every prefix of a safe trace is safe–limit-closed: limit of sequence of safe traces is safe●Liveness property: “good” thing happens eventually–every finite sequence over acts(P) has an extension (is a prefix) of some sequence in traces(P)●“it's never too late”●Every trace property is intersection of a safety and a liveness property.●Every (closed) safety property can be specified as automaton.p1C1,2p2C2,1send(m)1,2send(m)2,1receive(m)1,2receive(m)2,1init(v)1decide(v)1Composition: Asynchronous networkComposition●“Put multiple automata together”–output actions of one may be input actions of others●Look first at composing two automata–generalize to composing infinitely many automata (in book)●Recall: –sig(A) = ( in(A), out(A), int(A) )–local(A) = out(A) ∪ int(A)●Two automata A and B are compatible if–local(A) and local(B) are disjoint–int(A) and acts(B) are disjoint–int(B) and acts(A) are disjointComposition●A × B, composition of A and B–int(A × B) = int(A) ∪ int(B)–out(A × B) = out(A) ∪ out(B)–in(A × B) = in(A) ∪ in(B) – (out(A) ∪ out(B))–states(A × B) = states(A) × states(B)–start(A × B) = start(A) × start(B)–trans(A × B): includes (s, π, s') iff●(sA, π, s'A) ∈ trans(A) if π ∈ acts(A); sA = s'A otherwise●(sB, π, s'B) ∈ trans(B) if π ∈ acts(B); sB = s'B otherwise–tasks(A × B) = tasks(A) ∪ tasks(B)●∏ ∈ i I Ai, composition of { Ai : i ∈ I } (I countable)Composition: Basic results●Projection–execution of composition “looks good” to each component●Pasting–if execution “looks good” to each component, it is good.●Substitutability–can replace a component with one that implements itComposition: Basic results●Projection–If α ∈ execs(∏ Ai) then α|Ai ∈ execs(Ai) for all i.–If β ∈ traces(∏ Ai) then β|Ai ∈ traces(Ai) for all i.–If α ∈ fairexecs(∏ Ai) then α|Ai ∈ fairexecs(Ai) for all i.–If β ∈ fairtraces(∏ Ai) then β|Ai ∈ fairtraces(Ai) for all i.Composition: Basic results●Pasting–Suppose β is a sequence of external actions of ∏ Ai.–If αi ∈ execs(Ai) and β|Ai = trace(αi) for all ithen there is an execution α of ∏ Ai such that β = trace(α) and αi = α|Ai for all i.–If αi ∈ fairexecs(Ai) and β|Ai = trace(αi) for all ithen there is a fair execution α of ∏ Ai such that β = trace(α) and αi = α|Ai for all i.–If β|Ai ∈ traces(Ai) for all i then β ∈ traces(∏ Ai).–If β|Ai ∈ fairtraces(Ai) for all i then β ∈ fairtraces(∏ Ai).Composition: Basic results●Substitutability–If Ai implements A'i for all i then ∏ Ai implements ∏ A'i (assuming ∏ Ai and ∏ A'i are defined).●follows from trace projection and pasting–Analogous result for “fair implementation”.Other operations on I/O automata●Hiding–make some output actions internal–hides internal communication among components of system●Renaming–change names of some actions (changes sig, trans, tasks)–important because communication between automata is through shared actions–typically just make names right in first placeChannel 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)Composing two channel automata●Output of B is input of A–rename receive(m) of B and send (m) of A to pass(m)●hide{ pass(m) | m ∈ M } A × B implements C–define simulation relation R:●for s ∈ states(A × B) and u ∈ states(C), s R u iff u.queue is concatenation of s.A.queue and s.B.queue–start: all queues empty, so start states correspond–step: define “step correspondence”Asend(m) receive(m)Bpass(m)Composing two channel automata●step correspondence: –for each step (s, π,s') ∈ trans(A × B) and u such that s R u,define execution fragment α of C●starts with u ends with u' such that s' R u'●trace(α) = trace( π)–actions in α depends only on π, uniquely determine post-state●same action if external, λ otherwiseAsend(m) receive(m)Bpass(m)s R u iff u.queue is concatenation of s.A.queue and s.B.queueComposing two channel automata●step correspondence: –π = send(m) corresponds to send(m) in C–π = receive(m) corresponds to receive(m) in C–π = pass(m) corresponds to λ in C●verify actions are enabled, preserve simulation relation–boring case analysisAsend(m) receive(m)Bpass(m)s R u iff u.queue is concatenation of s.A.queue and s.B.queueAsynchronous networks●Processes communicate via