Distributed Algorithms. Nancy A. Lynch (1993) (Distributed Algorithms. Nancy A. Lynch (1993).pdf), страница 81

If bu (C ) < 1 then there exists j > i with tj ti + bu (C ) such that either j 2 C orsj 2 disabled (A C ).2. There does not exist j > i with tj < ti + b` (C ) and j in C .The rst condition says that, starting from an initial index for C , within time bu (C )either some action in C occurs or there is a point at which no such action is enabled. Notethat if bu (C ) = 1, no upper bound requirement is imposed. The second condition saysthat, again starting from an initial index for C , no action in C can occur before time b` (C )415has elapsed. Note in particular that if a class C becomes disabled and then enabled onceagain, the lower bound calculation gets \restarted" at the point where the class becomesre-enabled.The timed schedule of a timed execution of a timed automaton (A b) is the subsequenceconsisting of the (action,time) pairs, and the timed behavior is the subsequence consistingof the (action,time) pairs for which the action is external.

The timed schedules and timedbehaviors of (A b) are just those of the timed executions of (A b).We model each timing-dependent concurrent system as a single timed automaton (A b),where A is a composition of ordinary I/O automata (possibly with some output actionshidden). We also model problem specications, including timing properties, in terms oftimed automata.We note that the denition we use for timed automata may not be suciently general tocapture all interesting systems and timing requirements.

It does capture many, however.The MMT paper contains a generalization of this model, in which we have bounds thatcan be open or closed. Also, upper bound of 0 allowed (?). Finally, don't restrict to onlynitely many processes. Do results about composition similar to I/O automata.17C.2 Simple Mutual Exclusion ExampleJust as an illustrative example, I'll describe a very basic problem weconsidered within this model { to get simple upper and lower boundresults for a basic problem.Started with mutual exclusion.When we did this, we did not have a clear idea of which parameters,etc., would turn out to be the most important, so we consideredeverything.C.3 Basic Proof MethodsAlgorithms such as the ones in this paper quickly lead to the need forproof methods for verifying correctness of timing-based algorithms.An equivalent way of looking at each system is as a composition of timed automata.

An appropriatedenition for a composition of timed automata is developed in MerrittMT90], together with theoremsshowing the equivalence of the two viewpoints.17416In the untimed setting, we make heavy use of invariants andsimulations, so it seems most reasonable to try to extend thesemethods to the timed setting.However, it is not instantly obvious how to do this.In an asynchronous system, everything important about the system'sstate (i.e., everything that can aect the system's futurebehavior) is summarized in the ordinary states of the processes andchannels, i.e., in the values of the local variables and the multiset ofmessages in transit on each link.In a timing-based system, that is no longer the case.Now if a message is in transit, it is important to know whether it hasjust been placed into a channel or has been there a long time (and istherefore about to be delivered).Similar remarks hold for process steps.Therefore, it is convenient to augment the states with some extrapredictive timing information, giving bounds on how long it will bebefore certain events may or must occur.C.4 ConsensusNow we can also revisit the problem of distributed consensusin the timed setting.This time, for simplicity, we ignore the separate clocks and justsuppose we have processes with upper and lower bounds of c c ]on step time.The questions is how much time it takes to reach consensus, if thereare f faulty processes.1C.5 More Mutual ExclusionLynch-Shavit mutual exclusion with proofs.4172C.6 Clock SynchronizationWork from Lamport, Melliar-SmithLundelius, LynchFischer, Lynch, Merritt4186.852J/18.437J Distributed AlgorithmsHandout 2September 10, 19926.852 Course Reading ListGeneral References1] N.

Lynch and I. Saias. Distributed Algorithms. Fall 1990 Lecture Notes for 6.852.MIT/LCS/RSS 16, Massachusetts Institute of Technology, February 1992.2] N. Lynch and K. Goldman. Distributed Algorithms. MIT/LCS/RSS 5, MassachusettsInstitute of Technology, 1989. Lecture Notes for 6.852.3] M. Raynal. Algorithms for Mutual Exclusion. M.I.T.

Press, 1986.4] M. Raynal. Networks and Distributed Computation. M.I.T. Press, 1988.5] J. M. H%elary and M. Raynal. Synchronization and Control of Distributed Systems andPrograms. John Wiley & Sons, 1990.6] K. M. Chandy and J. Misra. Parallel program design: a foundation. Addison-Wesley,1988.7] Butler Lampson, William Weihl, and Eric Brewer. 6.826 Principles of computer systems, Fall 1991. MIT/LCS/RSS 19, Massachusetts Institute of Technology, 1992.Lecture Notes and Handouts.D.1 Introduction1] L. Lamport and N.

Lynch. Distributed computing. Chapter of Handbook on Theoretical Computer Science. Also, appeared as Technical Memo MIT/LCS/TM-384,Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge,MA, February 1989.419D.2 Models and Proof MethodsD.2.1 Automata1] Nancy Lynch and Frits Vaandrager.

Forward and backward simulations for timingbased systems. In Proceedings of REX Workshop \Real-Time: Theory in Practice",volume 600 of Lecture Notes in Computer Science, Mook, The Netherlands, 1992.Springer-Verlag. Also, MIT/LCS/TM 458.D.2.2 Invariants1] S. Owicki and D.

Gries. An axiomatic proof technique for parallel programs. ActaInformatica, 6(4):319{340, 1976.2] L. Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems, 5(2):190{222, April 1983.3] Butler Lampson, William Weihl, and Eric Brewer. 6.826 Principles of computer systems, Fall 1991. MIT/LCS/RSS 19, Massachusetts Institute of Technology, 1992.Lecture notes and Handouts.D.2.3 Mapping Methods1] Nancy Lynch and Frits Vaandrager.

Forward and backward simulations for timingbased systems. In Proceedings of REX Workshop \Real-Time: Theory in Practice",volume 600 of Lecture Notes in Computer Science, Mook, The Netherlands, 1992.Springer-Verlag. Also, MIT/LCS/TM 458.2] M%artin Abadi and Leslie Lamport. The existence of renement mapping. TheoreticalComputer Science, 2(82):253{284, 1991.3] Nils Klarlund and Fred B. Schneider. Proving nondeterministically specied safetyproperties using progress measures, May 1991.

To appear in Information and Computation Spring, 1993.D.2.4 Shared Memory Models1] N. Lynch and M. Fischer. On describing the behavior and implementation of distributed systems. Theoretical Computer Science, 13:17{43, 1981.4202] Kenneth Goldman, Nancy Lynch, and Kathy Yelick. Modelling shared state in a sharedaction model, April 1992. Manuscript. Also, earlier verison in Proceedings of the 5thAnnual IEEE Symposium on Logic in Computer Science, pages 450-463, Philadelphia,PA, June 1990.D.2.5 I/O Automata1] Nancy A. Lynch and Mark R. Tuttle.

An introduction to input/output automata.CWI-Quarterly, 2(3), 1989.2] Mark Tuttle. Hierarchical correctness proofs for distributed algorithms. Master'sthesis, Massachusetts Institute of Technology, MIT Dept. of Electrical Engineeringand Computer Science, April 1987.3] Nick Reingold, Da-Wei Wang and Lenore Zuck. Games I/O automata play, September1991.

Technical Report YALE/DCS/TR{857.4] Da-Wei Wang, Lenore Zuck, and Nick Reingold. The power of I/O automata.Manuscript, May, 1991.D.2.6 Temporal Logic1] Z. Manna and A.Pnueli. The Temporal Logic of Reactive and Concurrent Systems.Springer-Verlag, 1992.2] K. M. Chandy and J. Misra. Parallel program design: a foundation. Addison-Wesley,1988.3] Leslie Lamport. The temporal logic of actions. Technical Report 79, Digital SystemsResearch Center, December 25 1991.D.2.7 Timed Models1] F. Modugno, M. Merritt, and M.

Tuttle. Time constrained automata. In CONCUR'91Proceedings Workshop on Theories of Concurrency: Unication and Extension, Amsterdam, August 1991.2] Nancy Lynch and Frits Vaandrager. Forward and backward simulations for timingbased systems. In Proceedings of REX Workshop \Real-Time: Theory in Practice",volume 600 of Lecture Notes in Computer Science, Mook, The Netherlands, 1992.Springer-Verlag. Also, MIT/LCS/TM 458.4213] Rajeev Alur and David L. Dill.