6.852: Distributed Algorithms Spring, 2008Today’s planPartially synchronous system modelsModeling timed systemsMMT AutomataMMT Automata, cont’dExample: Timed FIFO channelComposition of MMT automataExample: Timeout systemExample: Two-task raceGeneral Timed AutomataExample: Timed FIFO ChannelAnother Timed FIFO ChannelTransforming MMTAs to GTAsTwo-task raceSlide 16More on GTAsTimed I/O Automata (TIOAs)Proof methods for GTAs and TIOAs.Slide 20Slide 21Simulation relationsSlide 23Simulation relationTimed mutual exclusionFischer mutual exclusion algorithmIncorrect executionFischer mutex algorithmProof of mutex propertyProof of progressStretching the time complexityLower bound on timeSlide 33Fischer algorithm is fragileAnother impossibility resultNext time…6.852: Distributed AlgorithmsSpring, 2008Class 25-2Today’s plan•Partially synchronous (timed) distributed systems•Models for timed systems•Proof methods•Mutual exclusion in timed systems•Reading: –Chapters 23, 24 •Next time:–Consensus in timed systems, clock synchronization–Reading: Chapter 25, [Dwork, Lynch, Stockmeyer]Partially synchronous system models•We’ve studied distributed algorithms in synchronous and asynchronous distributed models.•Now, intermediate, partially synchronous models.–Involve some knowledge of time, but not synchronized rounds.•Bounds on relative speed of processes, •Upper and lower bounds for message delivery, •Local clocks, proceeding at approximately-predictable rates.•Useful for studying:–Distributed algorithms whose behavior depends on time.–Practical communication protocols.–(Newer) Mobile networks, embedded systems, robot control,…•Needs new models, new proof methods.•Basis for new distributed algorithms, impossibility results.Modeling timed systems•MMT automata [Merritt, Modugno, Tuttle]–Simple, special-cased timed model–Immediate extension of I/O automata•GTA, more general timed automata, in book.•Timed I/O Automata–Still more general–[Kaynar, Lynch, Segala, Vaandrager] monograph–Tempo supportMMT Automata•Definition: An MMT automaton is an I/O automaton with finitely many tasks, plus a boundmap (lower, upper), where:–lower maps each task T to a lower bound lower(T), 0  lower(T) <  (can be 0, cannot be inifinite),–upper maps each task T to an upper bound upper(T), 0 < upper(T)   (cannot be 0, can be infinite),–For every T, lower(T)  upper(T).•Timed executions:–Like ordinary executions, but with times attached to events. = s0, (1, t1), s1, (2, t2), s2,…–Subject to the upper and lower bounds.•Task T can’t be continuously enabled for more than time upper(T) without an action of T occurring.•If an action of T occurs, then T must have been continuously enabled for time at least lower(T).–Restricts the set of executions (unlike having just upper bounds):–No fairness, just time bounds.MMT Automata, cont’d•Timed traces:–Suppress states and internal actions.–Keep info about external actions and their times of occurrence.•Admissible timed execution:–Infinite timed execution with times approaching , or–Finite timed execution such that upper(T) =  for every task enabled in the final state.•Rules out:–Infinitely many actions in finite time (“Zeno behavior”).–Stopping when some tasks still have work to do (and upper bounds by which they should do it).•Simple model, not very general, but good enough to describe some interesting examples…Example: Timed FIFO channel•Consider ordinary FIFO channel automaton.–State: queue–Actions:•Inputs: send(m), m in M•Outputs: receive(m), m in M–Tasks: receive = { receive(m) : m in M }•Boundmap:–Associate lower bound 0, upper bound d, with the receive task.•Guarantees delivery of oldest message in channel (head of queue), within time d.Composition of MMT automata•Compose MMT automata by –Composing the underlying I/O automata,–Combining all the boundmaps.–Composed automaton satisfies all timing constraints, of all components.•Satisfies pasting, projection, as before:–Project timed execution (or timed trace) of composition to get timed executions (timed traces) of components.–Paste timed executions (or timed traces) that match up at boundaries to obtained timed executions (timed traces) of the composition.•Also, a hiding operation, which makes some output actions internal.Example: Timeout system•P1: Sender process–Sends “alive” messages every time l, unless it is dead.–Express using 1 send task, bounds [0,l].•P2: Timeout process–Decrements a count from k; if reaches 0 without a message arriving, output “timeout”.–Express with 2 tasks, decrement with bounds [l1, l2], and timeout with bounds [0,l].–Need nontrivial lower bound for decrement, so that steps can be used to measure elapsed time.•Compose P1, P2, and timed channel with bound d.•Can show (assuming that k l1 > l + d):–If P2 times out P1 then P1 has in fact failed.•Even if P2 takes steps as fast as possible, enough time has passed.–If P1 fails then P2 times out P1, and does so by time k l2 + l.•P2 could actually take steps slowly.P1P2Timed channelExample: Two-task race•One automaton, two tasks:–Main = { increment, decrement, report }•Bounds [ l1, l2 ].–Interrupt = { set }•Bounds [ 0,l ].•Increment counter as long as flag = false, then decrement.•When count returns to 0, output report.•Set action sets flag true.•Q: What’s a good upper bound on the latest time at which a report may occur?•l + l2 + ( l2 / l1 ) l•Obtained by incrementing as fast as possible, then decrementing as slowly as possible.General Timed Automata•MMT is simple, but can’t express everything:–E.g.: Perform “one”, then “two”, in order, so that “one” occurs at an arbitrary time in [0,1] and “two” occurs at time exactly 1.•GTAs: –More general, expressive.–No tasks and bounds.–Instead, explicit time-passage actions (t), in addition to inputs, outputs, internal actions.–Time-passage steps (s, (t), s’), between ordinary discrete steps.Example: Timed FIFO Channel•Delivers oldest message within time d•States:queuenow, a real, initially 0last, a real or , initially •Transitions:send(m)Effect: add m to queueif |queue| = 1 then last := now + dreceive(m)Precondition: m = head(queue)Effect:remove head of queueif queue is nonempty then last