PRL Seminars

This talk will be about the application of formal methods to real-world group communication systems. Group communication is a generalization of point-to-point communication between pairs of processes (such as TCP) to communication among groups of processes. I will use as an example a group communication system called Ensemble that was written in ML.

Ensemble is both a general purpose toolkit for building reliable distributed systems and a modular system for carrying out research in distributed systems. It evolved from Isis, a previous group communication system that is widely used. Ensemble consists of small communication protocols that are stacked together to get high-level protocol stacks. A key feature of Ensemble is that it was designed from the start to support the application of formal methods for verifying its communication protocols. All of the protocol layers are written in ML in a functional style that allows them to be easily imported into the Nuprl theorem prover where they can be manipulated for verification. Interestingly, it has turned out that the support for formal methods intended for verifying Ensemble also enables a set of optimizations that greatly improve its performance.

In the talk I will give a quick overview of group communication, present our approach to verifying and optimizing Ensemble, and argue why group communication is an excellent application area for functional programming language research.

This is joint work with Robbert vanRenesse, Ken Birman, Robert Constable, Jason Hickey, and Christoph Kreitz. Ensemble and Nuprl were developed as part of the Horus and Nuprl projects, respectively, at Cornell.

Further information about Ensemble, including a freely available software distribution, can be found at: