Skip header Section
Skip Bibliometrics Section
Distributed AlgorithmsApril 1996
- Author:
- Nancy A. Lynch
Skip Abstract Section
Abstract
In Distributed Algorithms, Nancy Lynch provides a blueprint for designing, implementing, and analyzing distributed algorithms. She directs her book at a wide audience, including students, programmers, system designers, and researchers. Distributed Algorithms contains the most significant algorithms and impossibility results in the area, all in a simple automata-theoretic setting. The algorithms are proved correct, and their complexity is analyzed according to precisely defined complexity measures. The problems covered include resource allocation, communication, consensus among distributed processes, data consistency, deadlock detection, leader election, global snapshots, and many others. The material is organized according to the system model-first by the timing model and then by the interprocess communication mechanism. The material on system models is isolated in separate chapters for easy reference. The presentation is completely rigorous, yet is intuitive enough for immediate comprehension. This book familiarizes readers with important problems, algorithms, and impossibility results in the area: readers can then recognize the problems when they arise in practice, apply the algorithms to solve them, and use the impossibility results to determine whether problems are unsolvable. The book also provides readers with the basic mathematical tools for designing new algorithms and proving new impossibility results. In addition, it teaches readers how to reason carefully about distributed algorithms-to model them formally, devise precise specifications for their required behavior, prove their correctness, and evaluate their performance with realistic measures. Table of Contents 1 Introduction 2 Modelling I; Synchronous Network Model 3 Leader Election in a Synchronous Ring 4 Algorithms in General Synchronous Networks 5 Distributed Consensus with Link Failures 6 Distributed Consensus with Process Failures 7 More Consensus Problems 8 Modelling II: Asynchronous System Model 9 Modelling III: Asynchronous Shared Memory Model 10 Mutual Exclusion 11 Resource Allocation 12 Consensus 13 Atomic Objects 14 Modelling IV: Asynchronous Network Model 15 Basic Asynchronous Network Algorithms 16 Synchronizers 17 Shared Memory versus Networks 18 Logical Time 19 Global Snapshots and Stable Properties 20 Network Resource Allocation 21 Asynchronous Networks with Process Failures 22 Data Link Protocols 23 Partially Synchronous System Models 24 Mutual Exclusion with Partial Synchrony 25 Consensus with Partial Synchrony
- Martin Abadi and Leslie Lamport. An old-fashioned recipe for real time. In J. W. de Bakker et al., editors, Real-Time: Theory in Practice (REX Workshop, Mook, The Netherlands, June 1991), volume 600 of Lecture Notes in Computer Science , pages 1-27. Springer-Verlag, New York, 1992. Google Scholar
- Karl Abrahamson. On achieving consensus using a shared memory. In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing , pages 291-302, Toronto, Ontario, Canada, August 1988. Google Scholar
Digital Library
- Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. Atomic snapshots of shared memory. Journal of the ACM , 40(4):873-890, September 1993. Google Scholar
- Yehuda Afek, Hagit Attiya, Alan Fekete, Michael Fischer, Nancy Lynch, Yishay Mansour, Da-Wei Wang, and Lenore Zuck. Reliable communication over unreliable channels. Journal of the ACM , 41(6):1267-1297, November 1994. Google Scholar
- Yehuda Afek and Eli Gafni. End-to-end communication in unreliable networks. In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing , pages 131-148, Toronto, Ontario, Canada, August 1988. ACM, New York. Google Scholar
- Yehuda Afek and Eli Gafni. Time and message bounds for election in synchronous and asynchronous complete networks. SIAM Journal on Computing , 20(2):376-394, April 1991. Google Scholar
- Gul A. Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, 1986. Google Scholar
- Bowen Alpern and Fred B. Schneider. Defining liveness. Processing Letters , 21(4):181-185, October 1985.Google Scholar
- Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science , 126(2):183-235, April 1994. Google Scholar
- Rajeev Alur and Gadi Taubenfeld. Results about fast mutual exclusion. In Proceedings of the Real-Time Systems Symposium , pages 12-21, Phoenix, December 1992. IEEE, Los Alamitos, Calif.Google Scholar
- James H. Anderson. Composite registers. Distributed Computing , 6(3):141-154, April 1993. Google Scholar
- James H. Anderson. Multi-writer composite registers. Distributed Computing , 7(4):175-195, May 1994. Google Scholar
- Dana Angluin. Local and global properties in networks of processors. In Proceedings of the 12th Annual ACM Symposium on Theory of Computing , pages 82-93, Los Angeles, April 1980. Google Scholar
- Eshrat Arjomandi, Michael J. Fischer, and Nancy A. Lynch. Efficiency of synchronous versus asynchronous distributed systems. Journal of the ACM , 30(3):449-456, July 1983. Google Scholar
- E. A. Ashcroft. Proving assertions about parallel programs. Journal of Computer and System Sciences , 10(1):110-135, February 1975. Google Scholar
- James Aspnes and Maurice Herlihy. Fast randomized consensus using shared memory. Journal of Algorithms , 11(3):441-461, September 1990. Google Scholar
- H. Attiya and M. Mavronicolas. Efficiency of semisynchronous versus asynchronous networks. Mathematical Systems Theory , 27(6):547-571, November/ December 1994. Google Scholar
- Hagit Attiya, Amotz Bar-Noy, and Danny Dolev. Sharing memory robustly in message-passing systems. Journal of the ACM , 42(1):124-142, January 1995. Google Scholar
- Hagit Attiya, Amotz Bar-Noy, Danny Dolev, Daphne Koller, David Peleg, and Rüdiger Reischuk. Achievable cases in an asynchronous environment. In 28th Annual Symposium on Foundations of Computer Science , pages 337-346. IEEE, Los Alamitos, Calif., October 1987. Google Scholar
- Hagit Attiya, Amotz Bar-Noy, Danny Dolev, David Peleg, and Rüdiger Reischuk. Renaming in an asynchronous environment. Journal of the ACM , 37(3):524-548, July 1990. Google Scholar
- Hagit Attiya, Shlomi Dolev, and Jennifer L. Welch. Connection management without retaining information. In Proceedings of the 28th Annual Hawaii International Conference on System Sciences , volume II (Software Technology), pages 622-631, Wailea, Hawaii, January 1995. IEEE, Los Alamitos, Calif. Google Scholar
- Hagit Attiya, Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Bounds on the time to reach agreement in the presence of timing uncertainty. Journal of the ACM , 41(1):122-152, January 1994. Google Scholar
- Hagit Attiya, Michael Fischer, Da-Wei Wang, and Lenore Zuck. Reliable communication using unreliable channels. Manuscript, 1989.Google Scholar
- Hagit Attiya, Nancy Lynch, and Nir Shavit. Are wait-free algorithms fast? Journal of the ACM , 41(4):725-763, July 1994. Google Scholar
- Hagit Attiya and Nancy A. Lynch. Time bounds for real-time process control in the presence of timing uncertainty. Information and Computation , 110(1):183-232, April 1994. Google Scholar
- Hagit Attiya and Ophir Rachman. Atomic snapshots in O(n log n) operations. In Proceedings of the 12th Annual ACM Symposium on Principles of Distributed Computing , pages 29-40, Ithaca, N.Y., August 1993. Google Scholar
- Hagit Attiya, Marc Snir, and Manfred K. Warmuth. Computing in an anonymous ring. Journal of the ACM , 35(4):845-875, October 1988. Google Scholar
- Hagit Attiya and Jennifer L. Welch. Sequential consistency versus linearizability. ACM Transactions on Computer Systems , 12(2):91-122, May 1994. Google Scholar
- Baruch Awerbuch. Complexity of network synchronization. Journal of the ACM , 32(4):804-823, October 1985. Google Scholar
- Baruch Awerbuch. Reducing complexities of the distributed max-flow and breadth-first search algorithms by means of network synchronization. Networks , 15(4):425-437, winter 1985.Google Scholar
- Baruch Awerbuch. Optimal distributed algorithms for minimum weight spanning tree, counting, leader election and related problems. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing , pages 230-240, New York, May 1987. Google Scholar
- Baruch Awerbuch, Bonnie Berger, Lenore Cowen, and David Peleg. Near-linear cost sequential and distributed constructions of sparse neighborhood covers. In 34th Annual Symposium on Foundations of Computer Science , pages 638-647, Palo Alto, Calif., November 1993. IEEE, Los Alamitos, Calif. Google Scholar
- Baruch Awerbuch and Robert G. Gallager. Distributed BFS algorithms. In 26th Annual Symposium on Foundations of Computer Science , pages 250-256, Portland, Ore., October 1985. IEEE, Los Alamitos, Calif. Google Scholar
- Baruch Awerbuch, Oded Goldreich, David Peleg, and Ronen Vainish. A tradeoff between information and communication in broadcast protocols. Journal of the ACM , 37(2):238-256, April 1990. Google Scholar
- Baruch Awerbuch and David Peleg. Sparse partitions. In 31st Annual Symposium on Foundations of Computer Science , volume II, pages 503- 513, St. Louis, October 1990. IEEE, Los Alamitos, Calif. Google Scholar
- Baruch Awerbuch and David Peleg. Routing with polynomial communication-space trade-off. SIAM Journal of Discrete Mathematics , 5(2):151-162, 1992. Google Scholar
- Baruch Awerbuch and Michael Saks. A Dining Philosophers algorithm with polynomial response time. In 31st Annual Symposium on Foundations of Computer Science , volume I, pages 65-74, St. Louis, October 1990. IEEE, Los Alamitos, Calif. Google Scholar
- J. C. M. Baeten and W. P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, Cambridge, U.K., 1990. Google Scholar
- Amotz Bar-Noy, Danny Dolev, Cynthia Dwork, and H. Raymond Strong. Shifting gears: Changing algorithms on the fly to expedite Byzantine agreement. In Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing , pages 42-51, Vancouver, British Columbia, Canada, August 1987. Google Scholar
- Amotz Bar-Noy, Danny Dolev, Daphne Koller, and David Peleg. Fault-tolerant critical section management in asynchronous environments. Information and Computation , 95(1):1-20, November 1991. Google Scholar
- Alan E. Baratz and Adrian Segall. Reliable link initialization procedures. IEEE Transactions on Communications , 36(2):144-152, February 1988.Google Scholar
- K. A. Bartlett, R. A. Scantlebury, and P. T. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM , 12(5):260-261, May 1969. Google Scholar
- Richard Bellman. On a routing problem. Quarterly of Applied Mathematics , 16(1):87-90, 1958.Google Scholar
- Dag Belsnes. Single-message communication. IEEE Transactions on Communications , COM-24(2):190-194, February 1976.Google Scholar
- M. Ben-Ari. Principles of concurrent programming. Prentice Hall, Englewood Cliffs, N.J., 1982. Google Scholar
- Michael Ben-Or. Another advantage of free choice: Completely asynchronous agreement protocols. In Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing , pages 27-30, Montreal, Quebec, Canada, August 1983. Google Scholar
- Claude Berge. Graphs and Hypergraph. North-Holland, Amsterdam, 1973.Google Scholar
- Piotr Berman and Anupam A. Bharali. Distributed consensus in semisynchronous systems. In Proceedings of the Sixth International Parallel Processing Symposium , pages 632-635, Beverly Hills, March 1992. IEEE, Los Alamitos, Calif. Google Scholar
- Piotr Berman and Juan A. Garay. Cloture voting: n/4-resilient distributed consensus in t + 1 rounds. Mathematical Systems Theory--An International Journal on Mathematical Computing Theory , 26(1):3-20, 1993. Special issue on Fault-Tolerant Distributed Algorithms.Google Scholar
- P. A. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency Control and Recovery in Database Systems. Addison-Wesley, Reading, Mass., 1987. Google Scholar
- Ofer Biran, Shlomo Moran, and Shmuel Zaks. A combinatorial characterization of the distributed 1-solvable tasks. Journal of Algorithms , 11(3):420- 440, September 1990. Google Scholar
- Kenneth P. Birman and Thomas A. Joseph. Reliable communication in the presence of failures. ACM Transactions on Computer Systems , 5(1):47-76, February 1987. Google Scholar
- Bard Bloom. Constructing two-writer atomic registers. IEEE Transactions on Communications , 37(12):1506-1514, December 1988. Google Scholar
- Gregor Bochmann and Jan Gecsei. A unified method for the specification and verification of protocols. In B. Gilchrist, editor, Information Processing 77 (Toronto, August 1977), volume 7 of Proceedings of IFIP Congress , pages 229-234. North-Holland, Amsterdam, 1977.Google Scholar
- Elizabeth Borowsky and Eli Gafni. Generalized FLP impossibility result for t -resilient asynchronous computations. In Proceedings of the 25th Annual ACM Symposium on Theory of Computing , pages 91-100, San Diego, May 1993. Google Scholar
- Gabriel Bracha and Sam Toueg. Asynchronous consensus and broadcast protocols. Journal of the ACM , 32(4):824-840, October 1985. Google Scholar
- Gabriel Bracha and Sam Toueg. Distributed deadlock detection. Distributed Computing , 2(3):127-138, December 1987.Google Scholar
- Michael F. Bridgland and Ronald J. Watro. Fault-tolerant decision making in totally asynchronous distributed systems. In Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing , pages 52-63, Vancouver, British Columbia, Canada, August 1987. Google Scholar
- Manfred Broy. Functional specification of time sensitive communicating systems. In W. P. de Roever, J. W. de Bakker, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (REX Workshop, Mook, The Netherlands, May/June 1989), volume 430 of Lecture Notes in Computer Science , pages 153-179. Springer-Verlag, New York, 1990. Google Scholar
- James E. Burns. Mutual exclusion with linear waiting using binary shared variables. ACM SIGACT News , 10(2):42-47, summer 1978. Google Scholar
- James E. Burns. A formal model for message passing systems. Technical Report TR-91, Computer Science Department, Indiana University, Bloomington, September 1980.Google Scholar
- James E. Burns, Paul Jackson, Nancy A. Lynch, Michael J. Fischer, and Gary L. Peterson. Data requirements for implementation of N -process mutual exclusion using a single shared variable. Journal of the ACM , 29(1):183-205, January 1982. Google Scholar
- James E. Burns and Nancy A. Lynch. Bounds on shared memory for mutual exclusion. Information and Computation , 107(2):171-184, December 1993. Google Scholar
- O. S. F. Carvalho and G. Roucairol. On mutual exclusion in computer networks. Communications of the ACM , 26(2):146-148, February 1983. Google Scholar
- Tushar Deepak Chandra, Vassos Hadzilacos, and Sam Toueg. The weakest failure detector for solving consensus. Journal of the ACM , 43(4):685-722, July 1996. Google Scholar
- Tushar Deepak Chandra and Sam Toueg. Unreliable failure detectors for asynchronous systems. Journal of the ACM , 43(2):225-267, March 1996. Google Scholar
- K. M. Chandy and J. Misra. The Drinking Philosophers problem. ACM Transactions on Programming Languages and Systems , 6(4):632-646, October 1984. Google Scholar
- K. Mani Chandy and Leslie Lamport. Distributed snapshots: Determining global states of distributed systems. ACM Transactions on Computer Systems , 3(1):63-75, February 1985. Google Scholar
- K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, Reading, Mass., 1988. Google Scholar
- K. Mani Chandy, Jayadev Misra, and Laura M. Haas. Distributed deadlock detection. ACM Transactions on Computer Systems , 1(2):144-156, May 1983. Google Scholar
- Ernest Chang and Rosemary Roberts. An improved algorithm for decentralized extrema-finding in circular configurations of processes. Communications of the ACM , 22(5):281-283, May 1979. Google Scholar
- Ernest J. H. Chang. Echo algorithms: Depth parallel operations on general graphs. IEEE Transactions on Software Engineering , SE-8(4):391-401, July 1982. Google Scholar
- Soma Chaudhuri. More choices allow more faults: Set consensus problems in totally asynchronous systems. Information and Computation , 105(1):132-158, July 1993. Google Scholar
- Soma Chaudhuri, Rainer Gawlick, and Nancy Lynch. Designing algorithms for distributed systems with partially synchronized clocks. In Proceedings of the 12th Annual ACM Symposium on Principles of Distributed Computing , pages 121-132, Ithaca, N.Y., August 1993. Google Scholar
- Soma Chaudhuri, Maurice Herlihy, Nancy A. Lynch, and Mark R. Tuttle. Tight bounds for k -set agreement. Technical Report 95/4, Digital Equipment Corporation, Cambridge Research Lab, Cambridge, Mass. To appear.Google Scholar
- Soma Chaudhuri, Maurice Herlihy, Nancy A. Lynch, and Mark R. Tuttle. A tight lower bound for k -set agreement. In 34th Annual Symposium on Foundations of Computer Science , pages 206-215, Palo Alto, Calif., November 1993. IEEE, Los Alamitos, Calif. Google Scholar
- Soma Chaudhuri, Maurice Herlihy, Nancy A. Lynch, and Mark R. Tuttle. A tight lower bound for processor coordination. In Donald S. Fussell and Miroslaw Malek, editors, Responsive Computer Systems: Steps Toward Fault-Tolerant Real-Time Systems , chapter 1, pages 1-18. Kluwer Academic, Boston, 1995. (Selected papers from Second International Workshop on Responsive Computer Systems , Lincoln, N.H., September 1993.)Google Scholar
- Benny Chor, Amos Israeli, and Ming Li. On processor coordination using asynchronous hardware. In Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing , pages 86-97, Vancouver, British Columbia, Canada, 1987. Google Scholar
- Ching-Tsun Chou and Eli Gafni. Understanding and verifying distributed algorithms using stratified decomposition. In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing , pages 44-65, Toronto, Ontario, Canada, August 1988. Google Scholar
- Manhoi Choy and Ambuj K. Singh. Efficient fault tolerant algorithms for resource allocation in distributed systems. In Proceedings of the 24th Annual ACM Symposium on Theory of Computing , pages 593-602, Victoria, British Columbia, Canada, May 1992. Google Scholar
- William Douglas Clinger. Foundations of Actor Semantics. Ph.D. thesis, Department of Mathematics, Massachusetts Institute of Technology, Cambridge, June 1981. University Microfilms, Ann Arbor, Mich.Google Scholar
- Brian A. Coan. Achieving Consensus in Fault-Tolerant Distributed Computer Systems: Protocols, Lower Bounds, and Simulations. Ph.D. thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, June 1987. Google Scholar
- Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to Algorithms. MIT Press/McGraw-Hill, Cambridge, Mass./New York, 1990. Google Scholar
- Armin B. Cremers and Thomas N. Hibbard. Mutual exclusion of N processors using an O(N) -valued message variable. In G. Ausiello and C. Böhm, editors, Automata, Languages and Programming: Fifth Colloquium (5th ICALP, Udine, Italy, July 1978), volume 62 of Lecture Notes in Computer Science , pages 165-176. Springer-Verlag, New York, 1978. Google Scholar
- Armin B. Cremers and Thomas N. Hibbard. Arbitration and queueing under limited shared storage requirements. Technical Report 83, Department of Informatics, University of Dortmund, March 1979.Google Scholar
- N. G. de Bruijn. Additional comments on a problem in concurrent programming control. Communications of the ACM , 10(3):137-138, March 1967. Google Scholar
- W. P. de Roever and F. A. Stomp. A correctness proof of a distributed minimum-weight spanning tree algorithm. In Proceedings of the Seventh International Conference on Distributed Computing Systems , pages 440- 447, Berlin, September 1987. IEEE, Los Alamitos, Calif.Google Scholar
- Richard A. DeMillo, Nancy A. Lynch, and Michael J. Merritt. Cryptographic protocols. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing , pages 383-400, San Francisco, May 1982. Google Scholar
- Harish Devarajan. A correctness proof for a network synchronizer. Master's thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, May 1993. Technical Report MIT/LCS/TR-588. Google Scholar
- E. W. Dijkstra. Solution of a problem in concurrent programming control. Communications of the ACM , 8(9):569, September 1965. Google Scholar
- E. W. Dijkstra. Hierarchical ordering of sequential processes. Acta Informatica , 1(2):115-138, 1971. Google Scholar
- Edsger W. Dijkstra and C. S. Scholten. Termination detection for diffusing computations. Information Processing Letters , 11(1):1-4, August 1980.Google Scholar
- D. Dolev and H. R. Strong. Authenticated algorithms for Byzantine agreement. SIAM Journal of Computing , 12(4):656-666, November 1983.Google Scholar
- Danny Dolev. The Byzantine generals strike again. Journal of Algorithms , 3(1):14-30, March 1982.Google Scholar
- Danny Dolev, Cynthia Dwork, and Larry Stockmeyer. On the minimal synchronism needed for distributed consensus. Journal of the ACM , 34(1):77- 97, January 1987. Google Scholar
- Danny Dolev, Michael J. Fischer, Rob Fowler, Nancy A. Lynch, and H. Raymond Strong. An efficient algorithm for Byzantine agreement without authentication. Information and Control , 52(3):257-274, March 1982.Google Scholar
- Danny Dolev, Maria Klawe, and Michael Rodeh. An O(n log n) unidirectional distributed algorithm for extrema finding in a circle. Journal of Algorithms , 3(3):245-260, September 1982.Google Scholar
- Danny Dolev, Nancy A. Lynch, Shlomit S. Pinter, Eugene W. Stark, and William E. Weihl. Reaching approximate agreement in the presence of faults. Journal of the ACM , 33(3):499-516, July 1986. Google Scholar
- Danny Dolev, Rudiger Reischuk, and H. Raymond Strong. Early stopping in Byzantine agreement. Journal of the ACM , 37(4):720-741, October 1990. Google Scholar
- Danny Dolev and Nir Shavit. Bounded concurrent time-stamp systems are constructible. In Proceedings of the 21st Annual ACM Symposium on Theory of Computing , pages 454-466, Seattle, May 1989. To appear in SIAM Journal of Computing. Google Scholar
- Danny Dolev and H. Raymond Strong. Polynomial algorithms for multiple processor agreement. In Proceedings of the 14th Annual ACM Symposium on Theory of Computing , pages 401-407, San Francisco, May 1982. Google Scholar
- Cynthia Dwork, Maurice Herlihy, Serge A. Plotkin, and Orli Waarts. Time-lapse snapshots. In D. Dolev, Z. Galil, and M. Rodeh, editors, Theory of Computing and Systems (ISTCS '92, Israel Symposium, Haifa, May 1992), volume 601 of Lecture Notes in Computer Science , pages 154-170. Springer-Verlag, New York, 1992. Google Scholar
- Cynthia Dwork, Maurice P. Herlihy, and Orli Waarts. Contention in shared memory algorithms. In Proceedings of the 25th Annual ACM Symposium on Theory of Computing , pages 174-183, San Diego, May 1993. Expanded version in Technical Report CRL 93/12, Digital Equipment Corporation, Cambridge Research Lab, Cambridge, Mass. Google Scholar
- Cynthia Dwork, Nancy Lynch, and Larry Stockmeyer. Consensus in the presence of partial synchrony. Journal of the ACM , 35(2):288-323, April 1988. Google Scholar
- Cynthia Dwork and Yoram Moses. Knowledge and common knowledge in a Byzantine environment: Crash failures. Information and Computation , 88(2):156-186, October 1990. Google Scholar
- Cynthia Dwork and Dale Skeen. The inherent cost of nonblocking commitment. In Proceedings of the Second Annual ACM Symposium on Principles of Distributed Computing , pages 1-11, Montreal, Quebec, Canada, August 1983. Google Scholar
- Cynthia Dwork and Orli Waarts. Simple and efficient bounded concurrent timestamping and the traceable use abstraction. In Proceedings of the 24th Annual ACM Symposium on Theory of Computing , pages 655-666, Victoria, British Columbia, Canada, May 1992. Preliminary. Final version to appear in Journal of the ACM. Google Scholar
- Murray A. Eisenberg and Michael R. McGuire. Further comments on Dijkstra's concurrent programming control problem. Communications of the ACM , 15(11):999, November 1972. Google Scholar
- A. Fekete, N. Lynch, and L. Shrira. A modular proof of correctness for a network synchronizer. In J. van Leeuwen, editor, Distributed Algorithms (2nd International Workshop, Amsterdam, July 1987), volume 312 of Lecture Notes in Computer Science , pages 219-256. Springer-Verlag, New York, 1988. Google Scholar
- A. D. Fekete. Asymptotically optimal algorithms for approximate agreement. Distributed Computing , 4(1):9-29, March 1990.Google Scholar
- A. D. Fekete. Asynchronous approximate agreement. Information and Computation , 115(1):95-124, November 15, 1994. Google Scholar
- Alan Fekete, Nancy Lynch, Yishay Mansour, and John Spinelli. The impossibility of implementing reliable communication in the face of crashes. Journal of the ACM , 40(5):1087-1107, November 1993. Google Scholar
- Paul Feldman and Silvio Micali. An optimal probabilistic protocol for synchronous Byzantine agreement. To appear in SIAM Journal on Computing. Preliminary version appeared as Technical Report MIT/LCS/TM-425.b, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, December 1992. Google Scholar
- Paul Neil Feldman. Optimal Algorithms for Byzantine Agreement. Ph.D. thesis, Department of Mathematics, Massachusetts Institute of Technology, Cambridge, June 1988.Google Scholar
- Colin J. Fidge. Timestamps in message-passing systems that preserve the partial ordering. In Proceedings of the 11th Australian Computer Science Conference , pages 56-66, Brisbane, Australia, February 1988.Google Scholar
- Michael Fischer. Re: Where are you? E-mail message to Leslie Lamport. Arpanet message number [email protected] (47 lines), June 25, 1985.Google Scholar
- Michael J. Fischer. The consensus problem in unreliable distributed systems (a brief survey). Research Report YALEU/DCS/RR-273, Yale University, Department of Computer Science, New Haven, Conn., June 1983.Google Scholar
- Michael J. Fischer, Nancy D. Griffeth, and Nancy A. Lynch. Global states of a distributed system. IEEE Transactions on Software Engineering , SE- 8(3):198-202, May 1982. Google Scholar
- Michael J. Fischer and Nancy A. Lynch. A lower bound for the time to assure interactive consistency. Information Processing Letters , 14(4):183- 186, June 1982.Google Scholar
- Michael J. Fischer, Nancy A. Lynch, James E. Burns, and Allan Borodin. Resource allocation with immunity to limited process failure. In 20th Annual Symposium on Foundations of Computer Science , pages 234-254, San Juan, Puerto Rico, October 1979. IEEE, Los Alamitos, Calif. Google Scholar
- Michael J. Fischer, Nancy A. Lynch, James E. Burns, and Allan Borodin. Distributed FIFO allocation of identical resources using small shared space. ACM Transactions on Programming Languages and Systems , 11 (1):90- 114, January 1989. Google Scholar
- Michael J. Fischer, Nancy A. Lynch, and Michael Merritt. Easy impossibility proofs for distributed consensus problems. Distributed Computing , 1(1):26-39, January 1986. Google Scholar
- Michael J. Fischer, Nancy A. Lynch, and Michael S. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM , 32(2):374-382, April 1985. Google Scholar
- Robert W. Floyd. Assigning meanings to programs. In Mathematical Aspects of Computer Science (New York, April 1966), volume 19 of Proceedings of the Symposia in Applied Mathematics , pages 19-32. American Mathematical Society, Providence, 1967.Google Scholar
- L. R. Ford, Jr. and D. R. Fulkerson. Flows in Networks. Princeton University Press, Princeton, N.J., 1962.Google Scholar
- Nissim Francez. Distributed termination. ACM Transactions on Programming Languages and Systems , 2(1):42-55, January 1980. Google Scholar
- Greg N. Frederickson and Nancy A. Lynch. Electing a leader in a synchronous ring. Journal of the ACM , 34(1):98-115, January 1987. Google Scholar
- Harold N. Gabow. Scaling algorithms for network problems. Journal of Computer and System Sciences , 31(2):148-168, October 1985. Google Scholar
- Eli Gafni. Personal communication, April 1994.Google Scholar
- R. G. Gallager, P. A. Humblet, and P. M. Spira. A distributed algorithm for minimum-weight spanning trees. ACM Transactions on Programming Languages and Systems , 5(1):66-77, January 1983. Google Scholar
- Robert G. Gallager. Distributed minimum hop algorithms. Technical Report LIDS-P-1175, Laboratory for Information and Decision Systems, Massachusetts Institute of Technology, Cambridge, January 1982.Google Scholar
- Juan A. Garay, Shay Kutten, and David Peleg. A sub-linear time distributed algorithm for minimum-weight spanning trees. In 34th Annual Symposium on Foundations of Computer Science , pages 659-668, Palo Alto, Calif., November 1993. IEEE, Los Alamitos, Calif. Google Scholar
- Juan A. Garay and Yoram Moses. Fully polynomial Byzantine agreement in t + 1 rounds. In Proceedings of the 25th Annual ACM Symposium on Theory of Computing , pages 31-41, San Diego, May 1993. Google Scholar
- Stephen J. Garland and John V. Guttag. A guide to LP, the Larch Prover. Research Report 82, Digital Systems Research Center, Palo Alto, Calif., December 1991.Google Scholar
- Rainer Gawlick, Nancy Lynch, and Nir Shavit. Concurrent time-stamping made simple. In D. Dolev, Z. Galil, and M. Rodeh, editors, Theory of Computing and Systems (ISTCS '92, Israel Symposium, Haifa, May 1992), volume 601 of Lecture Notes in Computer Science , pages 171-185. Springer-Verlag, New York, 1992. Google Scholar
- Rainer Gawlick, Roberto Segala, Jørgen Søgaard-Andersen, and Nancy Lynch. Liveness in timed and untimed systems. In Serge Abiteboul and Eli Shamir, editors, Automata, Languages and Programming (21st International Colloquium, ICALP '94, Jerusalem, July 1994), volume 820 of Lecture Notes in Computer Science , pages 166-177. Springer-Verlag, New York, 1994. Google Scholar
- David K. Gifford. Weighted voting for replicated data. In Proceedings of the Seventh Symposium on Operating Systems Principles , pages 150-162, Pacific Grove, Calif., December 1979. ACM, New York. Google Scholar
- Virgil D. Gligor and Susan H. Shattuck. On deadlock detention in distributed systems. IEEE Transactions on Software Engineering , SE- 6(5):435-440, September 1980. Google Scholar
- Kenneth Goldman and Kathy Yelick. A unified model for shared-memory and message-passing systems. Technical Report WUCS-93-35, Washington University, St. Louis, June 1993.Google Scholar
- Kenneth J. Goldman and Nancy Lynch. Quorum consensus in nested transaction systems. ACM Transactions on Database Systems , 19(4):537- 585, December 1994. Google Scholar
- Kenneth J. Goldman and Nancy A. Lynch. Modelling shared state in a shared action model. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science , pages 450-463, Philadelphia, June 1990.Google Scholar
- J. N. Gray. Notes on data base operating systems. In R. Bayer, R. M. Graham, and G. Seegmüller, editors, Operating Systems: An Advanced Course , volume 60 of Lecture Notes in Computer Science , chapter 3.F, page 465. Springer-Verlag, New York, 1978. Google Scholar
- Vassos Hadzilacos and Sam Toueg. Fault-tolerant broadcasts and related problems. In Sape Mullender, editor, Distributed Systems , second edition, chapter 5, pages 97-145. ACM Press/Addison-Wesley, New York/Reading, Mass., 1993. Google Scholar
- S. Haldar and K. Vidyasankar. Constructing 1-writer multireader multivalued atomic variables from regular variables. Journal of the ACM , 42(1):186-203, January 1995. Google Scholar
- Joseph Y. Halpern, Yoram Moses, and Orli Waarts. A characterization of eventual byzantine agreement. In Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing , pages 333-346, Quebec City, Quebec, Canada, August 1990. Google Scholar
- Joseph Y. Halpern and Lenore D. Zuck. A little knowledge goes a long way: Knowledge-based proofs for a family of protocols. Journal of the ACM , 39(3):449-478, July 1992. Google Scholar
- Frank Harary. Graph Theory. Addison-Wesley, Reading, Mass., 1972.Google Scholar
- Constance Heitmeyer and Nancy Lynch. The generalized railroad crossing: A case study in formal verification of real-time systems. Technical Memo MIT/LCS/TM-511, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, November 1994. Abbreviated version in Proceedings of the Real-Time Systems Symposium , pages 120-131, San Juan, Puerto Rico, December 1994. IEEE, Los Alamitos, Calif. Later version to appear in C. Heitmeyer and D. Mandrioli, editors Formal Methods for Real-time Computing , chapter 4, Trends in Software series, John Wiley & Sons, New York. Google Scholar
- Maurice Herlihy. A quorum-consensus replication method for abstract data types. ACM Transactions on Computer Systems , 4(1):32-53, February 1986. Google Scholar
- Maurice Herlihy. Wait-free synchronization. ACM Transactions on Programming Languages and Systems , 13(1):124-149, January 1991. Google Scholar
- Maurice Herlihy and Nir Shavit. A simple constructive computatability theorem for wait-free computation. In Proceedings of the 26th Annual ACM Symposium on Theory of Computing , pages 243-262, Montreal, Quebec, Canada, May 1994. Google Scholar
- Maurice P. Herlihy and Nir Shavit. The asynchronous computability theorem for t -resilient tasks. In Proceedings of the 25th Annual ACM Symposium on Theory of Computing , pages 111-120, San Diego, May 1993. Google Scholar
- Maurice P. Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects. ACM Transactions on Programming Languages and Systems , 12(3):463-492, July 1990. Google Scholar
- Maurice Peter Herlihy. Replication Methods for Abstract Data Types. Ph.D. thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, May 1984. Technical Report MIT/LCS/TR-319. Google Scholar
- Lisa Higham and Teresa Przytycka. A simple, efficient algorithm for maximum finding on rings. In André Schiper, editor, Distributed Algorithms (7th International Workshop, WDAG '93, Lausanne, Switzerland, September 1993), volume 725 of Lecture Notes in Computer Science , pages 249- 263. Springer-Verlag, New York, 1993. Google Scholar
- D. S. Hirschberg and J. B. Sinclair. Decentralized extrema-finding in circular configurations of processes. Communications of the ACM , 23(11):627- 628, November 1980. Google Scholar
- Gary S. Ho and C. V. Ramamoorthy. Protocols for deadlock detection in distributed database systems. IEEE Transactions on Software Engineering , SE-8(6):554-557, November 1982. Google Scholar
- C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica , 1(4):271-281, 1972. Google Scholar
- C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall International, United Kingdom, 1985. Google Scholar
- Pierre A. Humblet. A distributed algorithm for minimum weight directed spanning trees. IEEE Transactions on Communications , COM-31(6):756- 762, June 1983.Google Scholar
- Sreekaanth S. Isloor and T. Anthony Marsland. An effective "on-line" deadlock detection technique for distributed database management systems. In Proceedings of COMPSAC 78: IEEE Computer Society's Second International Computer Software and Applications Conference , pages 283-288, Chicago, November 1978.Google Scholar
- Amos Israeli and Ming Li. Bounded time-stamps. Distributed Computing , 6(4):205-209, July 1993. Google Scholar
- Amos Israeli and Meir Pinhasov. A concurrent time-stamp scheme which is linear in time and space. In A. Segall and S. Zaks, editors, Distributed Algorithms: Sixth International Workshop (WDAG '92, Haifa, Israel, November 1992), volume 647 of Lecture Notes in Computer Science , pages 95-109. Springer-Verlag, New York, 1992. Google Scholar
- Wil Janssen and Job Zwiers. From sequential layers to distributed processes: Deriving a distributed minimum weight spanning tree algorithm. In Proceedings of the 11th Annual ACM Symposium on Principles of Distributed Computing , pages 215-227, Vancouver, British Columbia, Canada, August 1992. Google Scholar
- Bengt Jonsson. Compositional specification and verification of distributed systems. ACM Transactions on Programming Languages and Systems , 16(2):259-303, March 1994. Google Scholar
- Richard M. Karp and Vijaya Ramachandran. Parallel algorithms for shared-memory machines. In Jan Van Leeuwen, editor, Algorithms and Complexity , volume A of Handbook of Theoretical Computer Science , chapter 17, pages 869-942. Elsevier/MIT Press, New York/Cambridge, 1990. Google Scholar
- Jon Kleinberg, Hagit Attiya, and Nancy Lynch. Trade-offs between message delivery and quiesce times in connection management protocols. In Proceedings of ISTCS 1995: The Third Israel Symposium on Theory of Computing and Systems , pages 258-267, Tel Aviv, January 1995. IEEE, Los Alamitos, Calif. Google Scholar
- Donald E. Knuth. Additional comments on a problem in concurrent programming control. Communications of the ACM , 9(5):321-322, May 1966. Google Scholar
- Donald E. Knuth. Fundamental Algorithms , volume 1 of The Art of Computer Programming , second edition. Addison-Wesley, Reading, Mass., 1973.Google Scholar
- Dénes König. Sur les correspondances multivoques des ensembles. Fundamenta Mathematicae , 8:114-134, 1926.Google Scholar
- Clyde P. Kruskal, Larry Rudolph, and Marc Snir. Efficient synchronization on multiprocessors with shared memory. In Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing , pages 218-228, Calgary, Alberta, Canada, August 1986. Google Scholar
- Jaynarayan H. Lala. A Byzantine resilient fault-tolerant computer for nuclear power plant applications. In FTCS: 16th Annual International Symposium on Fault-Tolerant Computing Systems , pages 338-343, Vienna, July 1986. IEEE, Los Alamitos, Calif.Google Scholar
- Jaynarayan H. Lala, Richard. E. Harper, and Linda S. Alger. A design approach for ultrareliable real-time systems. Computer , 24(5):12-22, May 1991. Issue on Real-time Systems. Google Scholar
- Leslie Lamport. A new solution of Dijkstra's concurrent programming problem. Communications of the ACM , 17(8):453-455, August 1974. Google Scholar
- Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering , SE-3(2):125-143, March 1977. Google Scholar
- Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM , 21(7):558-565, July 1978. Google Scholar
- Leslie Lamport. Specifying concurrent program modules. ACM Transactions on Programming Languages and Systems , 5(2):190-222, April 1983. Google Scholar
- Leslie Lamport. The weak Byzantine generals problem. Journal of the ACM , 30(3):669-676, July 1983. Google Scholar
- Leslie Lamport. Using time instead of timeout for fault-tolerant distributed systems. ACM Transactions on Programming Languages and Systems , 6(2):254-280, April 1984. Google Scholar
- Leslie Lamport. The mutual exclusion problem. Part II: Statement and solutions. Journal of the ACM , 33(2):327-348, April 1986. Google Scholar
- Leslie Lamport. On interprocess communication, Part I: Basic formalism. Distributed Computing , 1(2):77-85, April 1986.Google Scholar
- Leslie Lamport. On interprocess communication, Part II: Algorithms. Distributed Computing , 1(2):86-101, April 1986.Google Scholar
- Leslie Lamport. The part-time parliament. Research Report 49, Digital Systems Research Center, Palo Alto, Calif., September 1989.Google Scholar
- Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems , 16(3):872-923, May 1994. Google Scholar
- Leslie Lamport and Nancy Lynch. Distributed computing: Models and methods. In Jan Van Leeuwen, editor, Formal Models and Semantics , volume B of Handbook of Theoretical Computer Science , chapter 18, pages 1157-1199. Elsevier/MIT Press, New York/Cambridge, 1990. Google Scholar
- Leslie Lamport and Fred B. Schneider. Pretending atomicity. Research Report 44, Digital Equipment Corporation, Systems Research Center, Palo Alto, Calif., May 1989. Google Scholar
- Leslie Lamport, Robert Shostak, and Marshall Pease. The Byzantine generals problem. ACM Transactions on Programming Languages and Systems , 4(3):382-401, July 1982. Google Scholar
- Butler Lampson, Nancy Lynch, and Jørgen Søgaard-Andersen. At-most-once message delivery: A case study in algorithm verification. In W. R. Cleaveland, editor, CONCUR '92 (Third International Conference on Concurrency Theory, Stony Brook, N.Y., August 1992), volume 630 of Lecture Notes in Computer Science , pages 317-324. Springer-Verlag, New York, 1992. Google Scholar
- Butler Lampson, William Weihl, and Umesh Maheshwari. Principles of Computer Systems: Lecture Notes for 6.826, Fall 1992. Research Seminar Series MIT/LCS/RSS 22, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, July 1993.Google Scholar
- Butler W. Lampson, Nancy A. Lynch, and Jørgen F. Søgaard-Andersen. Correctness of at-most-once message delivery protocols. In Richard L. Tenney, Paul D. Amer, and M. Ümit Uyan, editors, Formal Description Techniques VI (Proceedings of the IFIP TC6/WG6.1 Sixth International Conference on Formal Description Techniques, FORTE '93, Boston, October, 1993) IFIP Transactions C , pages 385-400. North-Holland, Amsterdam, 1994. Google Scholar
- Gérard Le Lann. Distributed systems--towards a formal approach. In Bruce Gilchrist, editor, Information Processing 77 (Toronto, August 1977), volume 7 of Proceedings of IFIP Congress , pages 155-160. North-Holland, Amsterdam, 1977.Google Scholar
- Daniel Lehmann and Michael O. Rabin. On the advantages of free choice: A symmetric and fully distributed solution to the Dining Philosophers problem. In Proceedings of Eighth Annual ACM Symposium on Principles of Programming Languages , pages 133-138, Williamsburg, Va., January 1981. Google Scholar
- F. Thomson Leighton. Introduction to Parallel Algorithms and Architectures: Arrays, Trees, Hypercubes. Morgan Kaufmann, San Mateo, Calif., 1992. Google Scholar
- Harry R. Lewis. Finite-state analysis of asynchronous circuits with bounded temporal uncertainty. Technical Report TR-15-89, Center for Research in Computing Technology, Aiken Computation Laboratory, Harvard University, Cambridge, Mass., 1989.Google Scholar
- Harry R. Lewis and Christos H. Papadimitriou. Elements of the Theory of Computation. Prentice Hall, Englewood Cliffs, N.J., 1981.Google Scholar
- Ming Li and Paul M. B. Vitányi. How to share concurrent wait-free variables. Journal of the ACM , 43(4):723-746, July 1996. Google Scholar
- Barbara Liskov and Rivka Ladin. Highly-available distributed services and fault-tolerant distributed garbage collection. In Proceedings of the Fifth Annual ACM Symposium on Principles of Distributed Computing , pages 29-39, Calgary, Alberta, Canada, August 1986. Google Scholar
- Barbara Liskov, Alan Snyder, Russell Atkinson, and Craig Schaffert. Abstraction mechanisms in CLU. Communications of the ACM , 20(8):564- 576, August 1977. Google Scholar
- Michael C. Loui and Hosame H. Abu-Amara. Memory requirements for agreement among unreliable asynchronous processes. In Franco P. Preparata, editor, Parallel and Distributed Computing , volume 4 of Advances in Computing Research , pages 163-183. JAI Press, Greenwich, Conn., 1987.Google Scholar
- Michael Luby. A simple parallel algorithm for the maximal independent set problem. SIAM Journal of Computing , 15(4):1036-1053, November 1986. Google Scholar
- Victor Luchangco. Using simulation techniques to prove timing properties. Master's thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, June 1995.Google Scholar
- Victor Luchangco, Ekrem Söylemez, Stephen Garland, and Nancy Lynch. Verifying timing properties of concurrent algorithms. In Dieter Hogrefe and Stefan Leue, editors, Formal Description Techniques VII: Proceedings of the 7th IFIP WG6.1 International Conference on Formal Description Techniques (FORTE '94, Berne, Switzerland, October 1994), pages 259- 273. Chapman and Hall, New York, 1995. Google Scholar
- N. Lynch. Concurrency control for resilient nested transactions. In Proceedings of the Second ACM SIGACT-SIGMOD Symposium on Principles of Database Systems , pages 166-181, Atlanta, March 1983. Google Scholar
- Nancy Lynch. Simulation techniques for proving properties of real-time systems. In W. P. de Roever, J. W. de Bakker, and G. Rozenberg, editors, A Decade of Concurrency: Reflections and Perspectives (REX School/Symposium, Noordwijkerhout, The Netherlands, June 1993), volume 803 of Lecture Notes in Computer Science , pages 375-424. Springer-Verlag, New York, 1994. Google Scholar
- Nancy Lynch. Simulation techniques for proving properties of real-time systems. In Sang H. Son, editor, Advances in Real-Time Systems , chapter 13, pages 299-332. Prentice Hall, Englewood Cliffs, N.J., 1995. Google Scholar
- Nancy Lynch, Yishay Mansour, and Alan Fekete. The data link layer: Two impossibility results. In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing , pages 149-170, Toronto, Ontario, Canada, August 1988. Google Scholar
- Nancy Lynch, Michael Merritt, William Weihl, and Alan Fekete. Atomic Transactions. Morgan Kaufmann, San Mateo, Calif., 1994.Google Scholar
- Nancy Lynch, Isaac Saias, and Roberto Segala. Proving time bounds for randomized distributed algorithms. In Proceedings of the 13th Annual ACM Symposium on Principles of Distributed Computing , pages 314-323, Los Angeles, August 1994. Google Scholar
- Nancy Lynch and Nir Shavit. Timing-based mutual exclusion. In Proceedings of the Real-Time Systems Symposium , pages 2-11, Phoenix, December 1992. IEEE, Los Alamitos, Calif.Google Scholar
- Nancy Lynch and Frits Vaandrager. Forward and backward simulations for timing-based systems. In J. W. de Bakker et al., editors, Real-Time: Theory in Practice (REX Workshop, Mook, The Netherlands, June 1991), volume 600 of Lecture Notes in Computer Science , pages 397-446. Springer-Verlag, New York, 1992. Google Scholar
- Nancy Lynch and Frits Vaandrager. Forward and backward simulations-- Part II: Timing-based systems. Information and Computation , 128(1): 1-25, July 1996. Google Scholar
- Nancy Lynch and Frits Vaandrager. Action transducers and timed automata. Technical Memo MIT/LCS/TM-480.b, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, October 1994.Google Scholar
- Nancy A. Lynch. Upper bounds for static resource allocation in a distributed system. Journal of Computer and System Sciences , 23(2):254- 278, October 1981.Google Scholar
- Nancy A. Lynch. Multivalued possibilities mappings. In W. P. de Roever, J. W. de Bakker, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (REX Workshop, Mook, The Netherlands, May/June 1989), volume 430 of Lecture Notes in Computer Science , pages 519-543. Springer-Verlag, New York, 1990. Google Scholar
- Nancy A. Lynch and Hagit Attiya. Using mappings to prove timing properties. Distributed Computing , 6(2):121-139, September 1992. Google Scholar
- Nancy A. Lynch and Michael J. Fischer. On describing the behavior and implementation of distributed systems. Theoretical Computer Science , 13(1):17-43, 1981. Special issue on Semantics of Concurrent Computation.Google Scholar
- Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. Master's thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, April 1987. Technical Report MIT/LCS/TR-387. Abbreviated version in Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing , pages 137-151, Vancouver, British Columbia, Canada, August, 1987. Google Scholar
- Nancy A. Lynch and Mark R. Tuttle. An introduction to input/output automata. CWI-Quarterly , 2(3):219-246, September 1989. Centrum voor Wiskunde en Informatica, Amsterdam. Technical Memo MIT/LCS/TM-373, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, November 1988.Google Scholar
- Zohar Manna and Amir Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1992. Google Scholar
- Yishay Mansour and Baruch Schieber. The intractability of bounded protocols for on-line sequence transmission over non-FIFO channels. Journal of the ACM , 39(4):783-799, October 1992. Google Scholar
- John C. Martin. Introduction to Languages and the Theory of Computation. McGraw-Hill, New York, 1991. Google Scholar
- Friedemann Mattern. Virtual time and global states of distributed systems. In Michel Cosnard et al., editors, Parallel and Distributed Algorithms: Proceedings of the International Workshop on Parallel and Distributed Algorithrns (Chateau de Bonas, Gers, France, October, 1988), pages 215-226. North-Holland, Amsterdam, 1989.Google Scholar
- John M. McQuillan, Gilbert Falk, and Ira Richer. A review of the development and performance of the ARPANET routing algorithm. IEEE Transactions on Communications , COM-26(12):1802-1811, December 1978.Google Scholar
- Daniel A. Menasce and Richard R. Muntz. Locking and deadlock detection in distributed data bases. IEEE Transactions on Software Engineering , SE-5(3):195-202, May 1979. Google Scholar
- Karl Menger. Zur allgemeinen Kurventheorie. Fundamenta Mathematicae , 10:96-115, 1927.Google Scholar
- Michael Merritt, 1985. Unpublished Notes.Google Scholar
- Michael Merritt, Francesmary Modugno, and Mark R. Tuttle. Time constrained automata. In J. C. M. Baeten and J. F. Goote, editors, CONCUR '91: 2nd International Conference on Concurrency Theory (Amsterdam, August 1991), volume 527 of Lecture Notes in Computer Science , pages 408-423. Springer-Verlag, New York, 1991. Google Scholar
- Robin Milner. An algebraic definition of simulation between programs. In 2nd International Joint Conference on Artificial Intelligence , pages 481- 489, Imperial College, London, September 1971. British Computer Society, London. Google Scholar
- Robin Milner. Communication and Concurrency. Prentice-Hall International, United Kingdom, 1989. Google Scholar
- Shlomo Moran and Yaron Wolfstahl. Extended impossibility results for asynchronous complete networks. Information Processing Letters , 26(3):145-151, November 1987. Google Scholar
- Yoram Moses and Orli Waarts. Coordinated traversal: ( t + 1)- round Byzantine agreement in polynomial time. Journal of Algorithms , 17(1):110-156, July 1994. Google Scholar
- Gil Neiger and Sam Toueg. Simulating synchronized clocks and common knowledge in distributed systems. Journal of the ACM , 40(2):334-367, April 1993. Google Scholar
- Tobias Nipkow. Formal verification of data type refinement: Theory and practice. In W. P. de Roever, J. W. de Bakker, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness (REX Workshop, Mook, The Netherlands, May/June 1989), volume 430 of Lecture Notes in Computer Science , pages 561-591. Springer-Verlag, New York, 1990. Google Scholar
- Ron Obermarck. Distributed deadlock detection algorithm. ACM Transactions on Database Systems , 7(2):187-208, June 1982. Google Scholar
- Susan Owicki and David Gries. An axiomatic proof technique for parallel programs, I. Acta Informatica , 6(4):319-340, 1976. Google Scholar
- David Park. Concurrency and automata on infinite sequences. In Peter Deussen, editor, Theoretical Computer Science (5th GI Conference, Karlsruhe, Germany, March 1981), volume 104 of Lecture Notes in Computer Science , pages 167-183. Springer-Verlag, New York, 1981. Google Scholar
- M. Pease, R. Shostak, and L. Lamport. Reaching agreement in the presence of faults. Journal of the ACM , 27(2):228-234, April 1980. Google Scholar
- G. L. Peterson. Myths about the mutual exclusion problem. Information Processing Letters , 12(3):115-116, June 1981.Google Scholar
- Gary L. Peterson. An O(n log n) unidirectional distributed algorithm for the circular extrema problem. ACM Transactions on Programming Languages and Systems , 4(4):758-762, October 1982. Google Scholar
- Gary L. Peterson. Concurrent reading while writing. ACM Transactions on Programming Languages and Systems , 5(1):46-55, 1983. Google Scholar
- Gary L. Peterson and James E. Burns. Concurrent reading while writing II: The multi-writer case. In 28th Annual Symposium on Foundations of Computer Science , pages 383-392, Los Angeles, October 1987. IEEE, Los Alamitos, Calif. Google Scholar
- Gary L. Peterson and Michael J. Fischer. Economical solutions for the critical section problem in a distributed system. In Proceedings of the Ninth Annual ACM Symposium on Theory of Computing , pages 91-97, Boulder, Colo., May 1977. Google Scholar
- Amir Pnueli. Personal communication, 1988.Google Scholar
- Amir Pnueli and Lenore Zuck. Verification of multiprocess probabilistic protocols. Distributed Computing , 1(1):53-72, January 1986. Google Scholar
- Stephen Ponzio. Consensus in the presence of timing uncertainty: Omission and Byzantine failures. In Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing , pages 125-138, Montreal, Quebec, Canada, August 1991. Google Scholar
- Stephen Ponzio. Bounds on the time to detect failures using bounded-capacity message links. In Proceedings of the Real-time Systems Symposium , pages 236-245, Phoenix, December 1992. IEEE, Los Alamitos, Calif.Google Scholar
- Stephen J. Ponzio. The real-time cost of timing uncertainty: Consensus and failure detection. Master's thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, June 1991. Technical Report MIT/LCS/TR-518. Google Scholar
- Michael O. Rabin. Randomized Byzantine generals. In 24th Annual Symposium on Foundations of Computer Science , pages 403-409, Tucson, November 1983. IEEE, Los Alamitos, Calif. Google Scholar
- M. Raynal. Algorithms for Mutual Exclusion. MIT Press, Cambridge, 1986. Google Scholar
- Michel Raynal. Networks and Distributed Computation: Concepts, Tools, and Algorithms. MIT Press, Cambridge, 1988. Google Scholar
- Michel Raynal and Jean-Michel Helary. Synchronization and Control of Distributed Systems and Programs. John Wiley & Sons, Ltd., Chichester, U.K., 1990. Google Scholar
- Glenn Ricart and Ashok K. Agrawala. An optimal algorithm for mutual exclusion in computer networks. Communications of the ACM , 24(1):9-17, January 1981. Corrigendum in Communications of the ACM , 24(9):578, September 1981. Google Scholar
- Michael Saks and Fotios Zaharoglou. Wait-free k -set agreement is impossible: The topology of public knowledge. In Proceedings of the 25th Annual ACM Symposium on the Theory of Computing , pages 101-110, San Diego, May 1993. Google Scholar
- Russell Schaffer. On the correctness of atomic multi-writer registers. Technical Memo MIT/LCS/TM-364, Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, June 1988.Google Scholar
- Fred B. Schneider. Implementing fault-tolerant services using the state machine approach. ACM Computing Surveys , 22(4):299-319, December 1990. Google Scholar
- Reinhard Schwarz and Friedemann Mattern. Detecting causal relationships in distributed computations: In search of the holy grail. Distributed Computing , 7(3):149-174, March 1994. Google Scholar
- Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing , 2(2):250-273, August 1995. Special issue on selected papers from CONCUR'94. Google Scholar
- Adrian Segall. Distributed network protocols. IEEE Transactions on Information Theory , IT-29(1):23-35, January 1983. Google Scholar
- A. Udaya Shankar. A simple assertional proof system for real-time systems. In Proceedings of the Real-Time Systems Symposium , pages 167-176, Phoenix, December 1992. IEEE, Los Alamitos, Calif.Google Scholar
- A. Udaya Shankar and Simon S. Lam. A stepwise refinement heuristic for protocol construction. ACM Transactions on Programming Languages and Systems , 14(3):417-461, July 1992. Google Scholar
- Nit Shavit. Concurrent Time Stamping. Ph.D. thesis, Department of Computer Science, Hebrew University, Jerusalem, Israel, January 1990.Google Scholar
- Abraham Silberschatz, James L. Peterson, and Peter B. Galvin. Operating System Concepts , third edition. Addison-Wesley, Reading, Mass., 1992. Google Scholar
- Ambuj K. Singh, James H. Anderson, and Mohamed G. Gouda. The elusive atomic register. Journal of the ACM , 41(2):311-339, March 1994. Google Scholar
- Jørgen Søgaard-Andersen. Correctness of Protocols in Distributed Systems. Ph.D. thesis, Department of Computer Science, Technical University of Denmark, Lyngby, December 1993. ID-TR: 1993-131.Google Scholar
- Jørgen F. Søgaard-Andersen, Stephen J. Garland, John V. Guttag, Nancy A. Lynch, and Anna Pogosyants. Computer-assisted simulation proofs. In Costas Courcoubetis, editor, Computer-Aided Verification (5th International Conference, CAV '93, Elounda, Greece, June/July 1993), volume 697 of Lecture Notes in Computer Science , pages 305-319. Springer-Verlag, New York, 1993. Google Scholar
- Edwin H. Spanier. Algebraic Topology. McGraw-Hill, New York, 1966.Google Scholar
- E. Sperner. Neuer beweis für die invarianz der dimensionszahl und des gebietes. A bhandlungen Aus Dem Mathematischen Seminar Der Hamburgischen Universität , 6:265-272, 1928.Google Scholar
- John M. Spinelli. Reliable communication on data links. Technical Report LIDS-P-1844, Laboratory for Information and Decision Systems, Massachusetts Institute of Technology, Cambridge, December 1988.Google Scholar
- T. K. Srikanth and Sam Toueg. Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distributed Computing , 2(2):80- 94, August 1987.Google Scholar
- N. V. Stenning. A data transfer protocol. Computer Networks , 1(2):99- 110, September 1976.Google Scholar
- Tom Stoppard. Rosencrantz & Guildenstern Are Dead. Grove Press, New York, 1968.Google Scholar
- Eugene Styer and Gary L. Peterson. Improved algorithms for distributed resource allocation. In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing , pages 105-116, Toronto, Ontario, Canada, August 1988. Google Scholar
- Andrew S. Tanenbaum. Computer Networks , second edition. Prentice Hall, Englewood Cliffs, N.J., 1988. Google Scholar
- Y. C. Tay and W. Tim Loke. On deadlocks of exclusive AND-requests for resources. Distributed Computing , 9(2):77-94, October 1995. Google Scholar
- Gerard Tel. Assertional verification of a timer based protocol. In Timo Lepistö and Arto Salomaa, editors, Automata, Languages and Programming (15th International Colloquium, ICALP '88, Tempere, Finland, July 1988), volume 317 of Lecture Notes in Computer Science , pages 600-614. Springer-Verlag, New York, 1988. Google Scholar
- Gerard Tel. Introduction to Distributed Algorithms. Cambridge University Press, Cambridge, U.K., 1994. Google Scholar
- Ewan Tempero and Richard Ladner. Recoverable sequence transmission protocols. Journal of the ACM , 42(5):1059-1090, September 1995. Google Scholar
- Ewan Tempero and Richard E. Ladner. Tight bounds for weakly-bounded protocols. In Proceedings of the Ninth Annual A CM Symposium on Principles of Distributed Computing , pages 205-218, Quebec City, Quebec, Canada, August 1990. Google Scholar
- Russell Turpin and Brian A. Coan. Extending binary Byzantine agreement to multivalued Byzantine agreement. Information Processing Letters , 18(2):73-76, February 1984.Google Scholar
- Jan L. A. van de Snepscheut. The sliding-window protocol revisited. Formal Aspects of Computing , 7(1):3-17, 1995.Google Scholar
- George Varghese and Nancy A. Lynch. A tradeoff between safety and liveness for randomized coordinated attack protocols. In Proceedings of the 11th Annual ACM Symposium on Principles of Distributed Computing , pages 241-250, Vancouver, British Columbia, Canada, August 1992. Google Scholar
- Paul M. B. Vitányi. Distributed elections in an Archimedean ring of processors. In Proceedings of the 16th Annual ACM Symposium on Theory of Computing , pages 542-547, Washington, D.C., April/May 1984. Google Scholar
- Paul M. B. Vitányi and Baruch Awerbuch. Atomic shared register access by asynchronous hardware. In 27th Annual Symposium on Foundations of Computer Science , pages 233-243, Toronto, Ontario, Canada, October 1986. IEEE, Los Alamitos, Calif. Corrigendum in 28th Annual Symposium on Foundations of Computer Science , page 487, Los Angeles, October 1987. Google Scholar
- Da-Wei Wang and Lenore D. Zuck. Tight bounds for the sequence transmission problem. In Proceedings of the Eighth Annual ACM Symposium on Principles of Distributed Computing , pages 73-83, Edmonton, Alberta, Canada, August 1989. Google Scholar
- Jennifer Welch and Nancy Lynch. A modular Drinking Philosophers algorithm. Distributed Computing , 6(4):233-244, July 1993. Google Scholar
- Jennifer Lundelius Welch. Simulating synchronous processors. Information and Computation , 74(2):159-171, August 1987. Google Scholar
- Jennifer Lundelius Welch. Topics in Distributed Computing: The Impact of Partial Synchrony, and Modular Decomposition of Algorithms. Ph.D. thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, March 1988.Google Scholar
- Jennifer Lundelius Welch, Leslie Lamport, and Nancy Lynch. A lattice-structured proof technique applied to a minimum spanning tree algorithm. In Proceedings of the Seventh Annual ACM Symposium on Principles of Distributed Computing , pages 28-43, Toronto, Ontario, Canada, August 1988. Google Scholar
- John H. Wensley et al. SIFT: Design and analysis of a fault-tolerant computer for aircraft control. Proceedings of the IEEE , 66(10):1240-1255, October 1978.Google Scholar
- Hubert Zimmerman. OSI reference model--the ISO model of architecture for open systems interconnection. IEEE Transactions on Communications , COM-28(4):425-432, April 1980.Google Scholar
Please enable JavaScript to view thecomments powered by Disqus.