Reliable Messages and Connection Establishment

Butler W. Lampson

Citation: B. Lampson. Reliable messages and connection establishment. In Distributed Systems, ed. S. Mullender, 2nd ed., Addison-Wesley, 1993, pp 251-281.

Links: Postscript, Acrobat, Web page, Word.

Email: blampson@microsoft.com. This paper is at http://research.microsoft.com.

Abstract:

Reliable messages are delivered in the order they are sent, every message sent is delivered exactly once, and, and an acknowledgement is returned for each delivered message. These properties hold when there is no crash; when there is a crash, messages and acknowledgements may be lost. In this paper we

Give a simple, clear, and precise specification of reliable message delivery in the presence of crashes.

Explain the standard handshake protocol for reliable messages that is used in TCP, ISO TP4, and many other widespread communication systems, as well as a newer clock-based protocol.

Show that both protocols can be best understood as special cases of a simpler, more general protocol for using identifiers to tag messages and acknowledgements for reliable delivery.

Use the method of abstraction functions and invariants to help in understanding these three subtle concurrent and fault-tolerant algorithms, and in the process present all the hard parts of correctness proofs for all of them.

Take advantage of the generic protocol to simplify the analysis and the arguments.

In practice reliable messages are most often implemented in the form of ‘connections’, for example in the Internet TCP protocol.

We begin by writing a careful specification S for reliable messages. Then we present a ‘lower-level’ spec D in which the non-determinism ;associated with losing messages when there is a crash is moved to a place that is more convenient for implementations. We explain why D implements S but don’t give a proof, since that requires techniques beyond the scope of this chapter. With this groundwork, we present a generic protocol G and a proof that it implements D. Then we describe two protocols that are used in practice, the handshake protocol H and the clock-based protocol C, and show how both implement G. Finally, we explain how to modify our protocols to work with finite sets of message identifiers.