Crystall

Correct Modular Group Communication Middleware

Group communication has been widely argued to be an important enabling technology for building fault-tolerant applications in distributed systems. Applications can be made tolerant to crashes by replicating critical processes. The group communication system (or middleware) manages the interaction between the process replicas across the network.

However, the implementation of group communication with process crashes and unpredictable communication delay is a difficult task. The existing systems such as Ensemble and Transis are very complex. Therefore, we are interested in the semantic foundations (or models) of group communication and implementations of group communication that would correspond closely to the model, thus making it easier to understand the system's behaviour and verify its correctness.

In this project, we design and implement group communication using a modular approach that is based on implementing group communication services as separate protocols, and then combining selected protocols using a protocol framework. In addition to the possibility of constructing systems that are customized to the specific needs of an application, we have direct correspondence between the group communication model (defined as a set of abstractions) and its actual implementation. We currently experiment with implementing group communication using the Cactus and Appia frameworks.

Our current activities within the project fall into two complementary tracks:

Modular Group Communication

Rigorous specifications and correctness proofs of group communication protocols.
Fortika - a group communicatio toolkit featuring novel architectures and algorithms for software-based replication; Fortika supports both the crash-stop and crash-recovery models.
Modular, reusable implementation of Fortika group communication protocols (using various protocol frameworks).

Novel Protocol Frameworks

Calculi and language design for statically type-checked composition and interaction of protocols (Nuntius).
Transactional, automatic concurrency control in protocol stacks ( SAMOA ).
Programming and runtime support of dynamic protocol update ( SAMOA ).
Mathematical models of protocol frameworks (an operational semantics of their programming interfaces).

Personnel

* Principal investigators

External Collaborators

Massimo Merro (University of Verona)

We are associated with the Distributed Systems and Programming Methods groups at EPFL.

Below are papers and software developed within our project.

Papers

Modular Group Communication Middleware: Specification, Design and Proofs

	S. Mena, A. Schiper, and P. Wojciechowski, ``A Step Towards a New Generation of Group Communication Systems,'' tech. rep., 2003. [ Details \| Full Text ]
	A. Schiper, ``Dynamic Group Communication,'' tech. rep., 2003. [ Details \| Full Text ]
	S. Mena, A. Schiper, and P. T. Wojciechowski, ``A Step towards a New Generation of Group Communication Systems,'' in Lecture Notes in Computer Science, vol. 2672, pp. 414-432, 2003. [ Details \| Full Text ]
	U. Nestmann, R. Fuzzati, and M. Merro, ``Modeling Consensus in a Process Calculus,'' in CONCUR 2003 - Concurrency Theory, Lecture Notes in Computer Science, pp. 399-414, 2003. [ Details \| Full Text \| Link ]
	U. Nestmann and R. Fuzzati, ``Unreliable Failure Detectors via Operational Semantics,'' in Advances in Computing Science - ASIAN 2003, Lecture Notes in Computer Science, pp. 54-71, 2003. [ Details \| Full Text \| Link ]
	S. Mena and A. Schiper, ``A new look at atomic broadcast in the asynchronous crash-recovery model,'' tech. rep., 2004. [ Details \| Full Text ]
	S. Mena and A. Schiper in Proceedings of the 24th IEEE Symposium on Reliable Distributed Systems. [ Details \| Full Text ]
	S. Mena, C. Basile, Z. Kalbarczyk, A. Schiper, and R. K. Iyer, ``Assessing the Crash-Failure Assumption of Group Communication Protocols,'' in Proceedings of the 16th IEEE International Symposium on Software Reliability Engineering, 2005. [ Details \| Full Text \| Link ]

Modular Protocol Composition

	P. T. Wojciechowski, S. Mena, and A. Schiper. Semantics of Protocol Modules Composition and Interaction. Technical report, 2002. [ Details \| Full Text ]
	P. T. Wojciechowski, S. Mena, and A. Schiper. Semantics of Protocol Modules Composition and Interaction. In Lecture Notes in Computer Science, volume 2315, 2002. [ Details \| Link ]
	S. Mena, X. Cuvellier, C. Grégoire, and A. Schiper. Appia vs. cactus: Comparing Protocol Composition Frameworks. In Proceedings of the 22nd IEEE Symposium on Reliable Distributed Systems (SRDS'03), oct, 2003. [ Details \| Full Text \| Link ]
	P. T. Wojciechowski. Typing for Reliable Distributed Systems - Recent Advances. In DSN-2005 IEEE Workshop on Dependable Software - Tools and Methods, 2005. [ Details ]
	D. C. Bünzli, S. Mena, and U. Nestmann. Protocol Composition Frameworks, A Header Driven Model. In Proceedings of the 4th International Symposium on Network Computing and Applications (IEEE NCA05), 2005. [ Details \| Full Text ]
	D. C. Bünzli, S. Mena, and U. Nestmann. Protocol Composition Frameworks, A Header Driven Model. Technical report, 2005. [ Details \| Full Text ]
	O. Rütti, P. T. Wojciechowski, and A. Schiper. Service Interface: A New Abstraction for Implementing and Composing Protocols. In 21st ACM Symposium on Apllied Computing '06 SAC(2006), 2006. [ Details \| Full Text ]

Automatic Synchronization and Dynamic Protocol Update

	P. T. Wojciechowski, O. Rütti, and A. Schiper. SAMOA: A Framework for a Synchronisation-Augmented Microprotocol Approach. In Proc. of IPDPS '04 (18th International Parallel and Distributed Processing Symposium), 2004. [ Details \| Full Text \| Link ]
	P. T. Wojciechowski. Concurrency Combinators for Declarative Synchronization. In Lecture Notes in Computer Science, volume 3302, 2004. [ Details \| Full Text ]
	V. Tanasescu and P. T. Wojciechowski. Role-Based Declarative Synchronization for Reconfigurable Systems. In Lecture Notes in Computer Science, volume 3350, 2005. [ Details \| Link ]
	P. T. Wojciechowski. Isolation-only Transactions by Typing and Versioning. Technical report, 2004. [ Details \| Full Text ]
	P. T. Wojciechowski. Isolation-only Transactions by Typing and Versioning. In PPDP '05: The 7th ACM-SIGPLAN Symposium on Principles and Practice of Declarative Programming, 2005. [ Details \| Link ]
	P. T. Wojciechowski and O. Rütti. On Correctness of Dynamic Protocol Update. In Lecture Notes in Computer Science, volume 3535, 2005. [ Details \| Link ]
	O. Rutti, P. T. Wojciechowski, and A. Schiper. Dynamic Update of Distributed Agreement Protocols. Technical report, 2005. [ Details \| Full Text ]
	O. Rütti, P. T. Wojciechowski, and A. Schiper. Structural and Algorithmic Issues of Dynamic Protocol Update. In Proc. of IPDPS '06 (20th International Parallel and Distributed Processing Symposium), 2006. [ Details \| Full Text \| Link ]

Software

To facilitate experimentation, we also develop experimental systems and tools. Below is a sample.

The Fortika group communication middleware: an updated release is avalaible.
The SAMOA programming framework in Java: a brief description and distribution files are available.

Copyright

The following IEEE notices apply to the SRDS '03 '05, IPDPS '04, NCA '05 and IPDPS '06 papers:

(c) 2003-05 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.

The published versions of the COORDINATION '02, Middleware '03, CONCUR '03, ASIAN '03, APLAS '04 and PADL '05 and FMOODS '05 papers are (c) Springer-Verlag.

Crystall Correct Modular Group Communication Middleware