Research Projects NTT-MIT Research Collaboration: a partnership in the future of communication and computation

Cooperative Computing in Dynamic Environments

MIT9904-12

Start date: 07/99

 Nancy Lynch and Idit Keidar
MIT LCS

Yoshifumi Manabe
NTT

Project summary

We are exploring significant mathematical challenges in designing distributed systems to support group activities over networks.

Project description

 

We are working on developing models and analysis methods for distributed systems, with a focus on cooperative group activities in networks. Such group activities range from human social activities in cyber communities to powerful distributed applications involving data sharing and cooperative work. These activities are often supported by agent communication services, which provide distributed intelligence, or by group communication services, which manage group membership and guarantee coherent communication. The environments in which such activities take place are highly dynamic: participants come and go (and change location), network topology changes, and components fail and recover. Coping with such difficult environments leads to complex implementations, which are difficult to build, understand, and analyze.

This project addresses these problems using formal modeling and verification techniques, in particular, a combination of Input/Output automaton methods used at MIT and process algebraic and knowledge-based methods used at NTT. This involves extensions to the existing techniques, for example, extending I/O automata to allow dynamic process creation and destruction. As the basic framework is developed, it is being applied to a collection of typical examples from cooperative computing applications, including computer-supported cooperative work, e-commerce, and distributed databases. Other issues being studied include analysis of performance and fault-tolerance properties, and connecting the formal models with actual runnable code.

Demos, movies and other examples

The principal investigators

Presentations and posters

"Reliable Group Communication: A Mathematical Approach", Nancy Lynch, presented at the IEEE Kansai Chapter, July 7, 2000.

Publications

Agents:

"A Formal Model for Dynamic Computation", Paul Attie and Nancy Lynch, Technical Report, May 2000.

"On Formal Modeling of Agent Computations", Tadashi Araragi, Paul Attie, Idit Keidar, Kiyoshi Kogure, Victor Luchangco, Nancy Lynch and Ken Mano, NASA Workshop on Formal Approaches to Agent-Based Systems, April 2000. To appear as LNCS.

Group Communication:

"A Client-Server Approach to Virtually Synchronous Group Multicast: Specifications, Algorithms, and Proofs", Idit Keidar and Roger Khazan, to appear in The 20th International Conference on Distributed Computing Systems (ICDCS), pp. 344-355, April 2000.

"A Client-Server Oriented Algorithm for Virtually Synchronous Group Membership in WANs", Idit Keidar, Jeremy Sussman, Keith Marzullo and Danny Dolev, to appear in The 20th International Conference on Distributed Computing Systems (ICDCS), pp. 356-365, April 2000.

"Group Communication Specifications: A Comprehensive Study", Roman Vitenberg, Idit Keidar, Gregory V. Chockler and Danny Dolev, MIT Technical Report MIT-LCS-TR-790, September 1999.

"On Building Blocks for Distributed Systems", Roberto DePrisco, PhD Thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, Cambridge, MA 02139, December 1999.

"A Dynamic Primary Configuration Group Communication Service", Roberto De Prisco, Alan Fekete, Nancy Lynch, and Alex Shvartsman, In Prasad Jayanti, editor, Distributed Computing (Proceedings of DISC'99 - 13th International Symposium on Distributed Computing, Bratislava, Slovak Republic, September 1999), Volume 1693 of Lecture Notes in Computer Science, pages 64-78, Springer-Verlag-Heidelberg.

"Specifying and Using a Partitionable Group Communication Service", Alan Fekete, Nancy Lynch, and Alex Shvartsman, To appear in ACM Transactions on Computer Systems.

"QoS Preserving Totally Ordered Multicast", Ziv Bar-Joseph, Idit Keidar, Tal Anker and Nancy Lynch, MIT Technical Report MIT-LCS-TR-796, January 2000.

"Availability Study of Dynamic Voting Algorithms", Kyle W. Ingols, M.Eng. thesis, MIT department of Electrical Engineering and Computer Science, May 5, 2000.

"Group Communication", Idit Keidar, Chapter in the Encyclopedia of Distributed Computing, Joseph Urban and Partha Dasgupta, editors, Kluwer Academic Publishers. To be published.

"An Inheritance-Based Technique for Building Simulation Proofs Incrementally", Idit Keidar, Roger Khazan, Nancy Lynch and Alex Shvartsman, In the 22nd International Conference on Software Engineering (ICSE), pp. 478-487, Limerick, Ireland, June 2000.

"Totally Ordered Broadcast in the Face of Network Partitions", Idit Keidar and Danny Dolev, Exploiting Group Communication for Replication in Partitionable Networks, Chapter 3 of Dependable Network Computing, pp. 51-75, D. Avresky Editor, Kluwer Academic Publications. January, 2000.

"A Client-Server Approach to Virtually Synchronous Group Multicast: Specifications, Algorithms, and Proofs", Idit Keidar and Roger Khazan, MIT Technical Report MIT-LCS-TR-794, November 1999.

"A Client-Server Oriented Algorithm for Virtually Synchronous Group Membership in WANs", Idit Keidar, Jeremy Sussman, Keith Marzullo and Danny Dolev, MIT Technical Memorandum MIT-LCS-TM-593, June 1999. Also: University of California, San Diego, Technical Report CS99-623.

"Optimistic Virtual Synchrony", Jeremy Sussman, Idit Keidar and Keith Marzullo To appear in the 19th IEEE Symposium on Reliable Distributed Systems (SRDS), October 2000. Also appeared as MIT Technical Report MIT-LCS-TR-792, November 1999.

"Virtual Synchrony Semantics: Client-Server Implementation", Igor Tarashchanskiy, Masters thesis. MIT Department of Electrical Engineering and Computer Science, Cambridge, Ma. In progress.

Proposals and progress reports

Proposals:

NTT Bi-Annual Progress Report, July to December 1999:

NTT Bi-Annual Progress Report, January to June 2000:

NTT Bi-Annual Progress Report, July to December 2000:

NTT Bi-Annual Progress Report, January to June 2001:

NTT Bi-Annual Progress Report, July to December 2001:

NTT Bi-Annual Progress Report, January to June 2002:

NTT Bi-Annual Progress Report, July to December 2002:

For more information