Chapter 10

Reliable Messages and Connection Establishment

Butler W. Lampson

10.1 Introduction

Given an unreliable network, we would like to reliably deliver messages from a sender to a receiver. This is the function of the transport layer of the ISO seven-layer cake. It uses the network layer, which provides unreliable message delivery, as a channel for communication between the sender and the receiver.

Ideally we would like to ensure that

Unfortunately, it’s expensive to achieve the second and third goals in spite of crashes and an unreliable network. In particular, it’s not possible to achieve them without making some change to stable state (state that survives a crash) every time a message is received. Why? When we receive a message after a crash, we have to be able to tell whether it has already been delivered. But if delivering the message doesn’t change any state that survives the crash, then we can’t tell.

So if we want a cheap deliver operation which doesn’t require writing stable state, we have to choose between delivering some messages more than once and losing some messages entirely when the receiver crashes. If the effect of a message is idempotent, of course, then duplications are harmless and we will choose the first alternative. But this is rare, and the latter choice is usually the lesser of two evils. It is called ‘at-most-once’ message delivery. Usually the sender also wants an acknowledgement that the message has been delivered, or in case the receiver crashes, an indication that it might have been lost. At-most-once messages with acknowledgements are called ‘reliable’ messages.

There are various ways to implement reliable messages. An implementation is called a ‘protocol’, and we will look at several of them. All are based on the idea of tagging a message with an identifier and transmitting it repeatedly to overcome the unreliability of the channel. The receiver keeps a stock of good identifiers that it has never accepted before; when it sees a message tagged with a good identifier, it accepts it, delivers it, and removes that identifier from the good set. Otherwise, the receiver just discards the message, perhaps after acknowledging it. In order for the sender to be sure that its message will be delivered rather than discarded, it must tag the message with a good identifier.

What makes the implementations tricky is that we expect to lose some state when there is a crash. In particular, the receiver will be keeping track of at least some of its good identifiers in volatile variables, so these identifiers will become bad at the crash. But the sender doesn’t know about the crash, so it will go on using the bad identifiers and thus send messages that the receiver will reject. Different protocols use different methods to keep the sender and the receiver more or less in sync about what identifiers to use.

In practice reliable messages are most often implemented in the form of ‘connections’. The idea is that a connection is ‘established’, any amount of information is sent on the connection, and then the connection is ‘closed’. You can think of this as the sending of a single large message, or as sending the first message using one of the protocols we discuss, and then sending later messages with increasing sequence numbers. Usually connections are full-duplex, so that either end can send independently, and it is often cheaper to establish both directions at the same time. We ignore all these complications in order to concentrate on the essential logic of the protocols.

What we mean by a crash is not simply a failure and restart of a node. In practice, protocols for reliable messages have limits, called ‘timeouts’, on the length of time for which they will wait to deliver a message or get an ack. We model the expiration of a timeout as a crash: the protocol abandons its normal operation and reports failure, even though in general it’s possible that the message in fact has been or will be delivered.

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, and summarize our results.

The goals of this chapter are to:

10.1.1 Methods

We use the definition of ‘implements’ and the abstraction function proof method explained in Chapter 3. Here is a brief summary of this material.

Suppose that X and Y are state machines with named transitions called actions; think of X as a specification and Y as an implementation. We partition the actions of X and Y into external and internal actions. A behavior of a machine M is a sequence of actions that M can take starting in an initial state, and an external behavior of M is the subsequence of a behavior that contains only the external actions. We say Y implements X iff every external behavior of Y is an external behavior of X. This expresses the idea that what it means for Y to implement X is that from the outside you don’t see Y doing anything that X couldn’t do.

The set of all external behaviors is a rather complicated object and difficult to reason about. Fortunately, there is a general method for proving that Y implements X without reasoning explicitly about behaviors in each case. It works as follows. First, define an abstraction function f from the state of Y to the state of X. Then show that Y simulates X:

A sequence of X-actions is the same externally as a Y-action if they are the same after all internal actions are discarded. So if the Y-action is internal, all the X-actions must be internal (perhaps none at all). If the Y-action is external, all the X-actions must be internal except one, which must be the same as the Y-action.

A straightforward induction shows that Y implements X: For any Y-behavior we can construct an X-behavior that is the same externally, by using (2) to map each Y-action into a sequence of X-actions that is the same externally. Then the sequence of X-actions will be the same externally as the original sequence of Y-actions.

In order to prove that Y simulates X we usually need to know what the reachable states of Y are, because it won’t be true that every action of Y from an arbitrary state of Y simulates a sequence of X-actions; in fact, the abstraction function might not even be defined on an arbitrary state of Y. The most convenient way to characterize the reachable states of Y is by an invariant, a predicate that is true of every reachable state. Often it’s helpful to write the invariant as a conjunction, and to call each conjunct an invariant. It’s common to need a stronger invariant than the simulation requires; the extra strength is a stronger induction hypothesis that makes it possible to establish what the simulation does require.

So the structure of a proof goes like this:

This method works only with actions and does not require any reasoning about behaviors. Furthermore, it deals with each action independently. Only the invariants connect the actions. So if we change (or add) an action of Y, we only need to verify that the new action maintains the invariants and simulates a sequence of X-actions that is the same externally. We exploit this remarkable fact in Section 10.9 to extend our protocols so that they use finite, rather than infinite, sets of identifiers.

In what follows we give abstraction functions and invariants for each protocol. The actual proofs that the invariants hold and that each Y-action simulates a suitable sequence of X-actions are routine, so we give proofs only for a few sample actions.

10.1.2 Types and NNotation

We use a type M for the messages being delivered. We assume nothing about M.

All the protocols except S and D use a type I of identifier;s for messages. In general we assume only that Is can be compared for equality; C assumes a total ordering. If x is a multiset whose elements have a first I component, we write ids(x) ;for the multiset of Is that appear first in the elements of x.

We define an action by giving its name, a guard that must be true for the action to occur, and an effect described by a set of assignments to state variables. We encode parameters by defining a whole family of actions with related names; for instance, get(m) is a different action for each possible m. Actions are atomic; each action completes before the next one is started.

To express concurrency we introduce more actions. Some of these actions may be internal, that is, they may not involve any interaction with the client of the protocol. Internal actions usually make the state machine non-deterministic, since they can happen whenever their guards are satisfied, not just when there is an interaction with the environment. We mark external actions with *s, two for an input action and one for an output action. Actions without *s are internal.

It’s convenient to present the sender actions on the left and the receiver actions on the right. Some actions are not so easy to categorize, and we usually put them on the left.

10.2 The Specification S

The specification S for reliable messages is a slight extension of the spec for a fifo queue. Figure 10.1 shows the external actions and some examples of its transitions. The basic state of S is the fifo queue q of messages, with put(m) and get(m) actions. In addition, the status variable records whether the most recently sent message has been delivered. The sender can use getAck(a) to get this information; after that it may be forgotten by setting status to lost, so that the sender doesn’t have to remember it forever. Both sender and receiver can crash and recover. In the absence of crashes, every message put is delivered by get in the same order and is positively acknowledged. If there is a crash, any message still in the queue may be lost at any time between the crash and the recovery, and its ack may be lost as well.

The getAck(a) action reports on the message most recently put, as follows. If there has been no crash since it was put there are two possibilities:

If there have been crashes, there are two additional possibilities:

The ack makes the most sense when the sender alternates put(m) and getAck(a) actions. Note that what is being acknowledged is delivery of the message to the client, not its receipt by some part of the implementation, so this is an end-to-end ;ack. In other words, the get should be thought of as including client processing of the message, and the ack might include some result returned by the client such as the result of a remote procedure call. This could be expressed precisely by adding an ack action for the client. We won’t do that because it would clutter up the presentation without improving our understanding of how reliable messages work.

To define S we introduce the types A (for acknowledgement) with values in {OK, lost} and Status with values in {OK, lost, ?}. Table 10.1 gives the state and actions of S. Note that it says nothing about channels; they are part of the implementation and have nothing to do with the spec.

The simplest spec which covers both these cases can lose a message at any time between a crash and its following recover, and we have adopted this alternative.

10.3 The Delayed-Decision Specification D

Next we introduce an implementation of S, called the delayed-decision specification ;D, that is more non-deterministic about when messages are lost. The reason for D is to simplify the proofs of the protocols: with more freedom in D, it’s easier to prove that a protocol simulates D than to prove that it simulates S. A typical protocol transmits messages from the sender to the receiver over some kind of channel which can lose messages; to compensate for these losses, the sender retransmits. If the sender crashes with a message in the channel it stops retransmitting, but whether the receiver gets the message depends on whether the channel loses it. This may not be decided until after the sender has recovered. So the protocol doesn’t decide whether the message is lost until after the sender has recovered. D has this freedom, but S does not.

D is the same as S except that the decisions about which messages to lose at recovery, and whether to lose the ack, are made by asynchronous drop actions that can occur after recovery. Each message in q, as well as the status variable, is augmented by an extra component ;of type Mark which is normally + but may become # between crash and recovery because of a mark action. At any time an unmark action can change a mark from # back to +, a message marked # can be lost by drop, or a status marked # can be set to lost by drop. Figure 10.2 gives an example of the transitions of D; the + marks are omitted.

To define D we introduce the type Mark which has values in the set {+, #}. Table 10.2 gives the state and actions of D.

10.3.1 Proof that D Implements S

We do not give this proof, since to do it using abstraction functions we would have to introduce ‘prophecy variables’, also known as ‘multi-valued mappings’ or ‘backward simulations’ (Abadi and Lamport [1991], Lynch and Vaandrager [1993]). If you work out some examples, however, you will probably see why the two specs S and D have the same external behavior.

10.4 Channels

All our protocols use the same channel abstraction to transfer information between the sender and the receiver. We use the name ‘packet’ for the messages sent over a channel, to distinguish them from reliable messages. A channel can freely drop and reorder packets, and it can duplicate a packet any finite number of times when it’s sent; the only thing it isn’t allowed to do is deliver a packet that wasn’t sent. The reason for using such a weak specification is to ensure that the reliable message protocol will work over any bit-moving mechanism that happens to be available. With a stronger channel spec, for instance one that doesn’t reorder packets, it’s possible to have somewhat simpler or more efficient implementations.

There are two channels sr and rs, one from sender to receiver and one from receiver to sender, each a multiset of packets initially empty. The nature of a packet varies from one protocol to another. Table 10.3 gives the channel actions.

Protocols interact with the channels through the external actions send(...) and rcv(...) which have the same names in the channel and in the protocol. One of these actions occurs if both its pre-conditions are true, and the effect is both the effects. This always makes sense because the states are disjoint.

10.5 The Generic Protocol G

The generic protocol ;G generalizes two practical protocols described later, H and C; in other words, both of them implement G. This protocol can’t be implemented directly because it has some ‘magic’ actions that use state from both sender and receiver. But both real protocols implement these actions, each in its own way.

This protocol satisfies the requirements of S; indeed, it does better since it never loses anything.

The SB protocol is widely used in practice, under names that resemble ‘queuing system’. It isn’t used to establish connections because the cost of a stable storage write for each message is too great.

Figure 10.4 shows the state of G, the most important actions, and the S-shaped flow of information. The new variables in the figure are the complement of the used variables in the code. The heavy lines show the flow of a new identifier from the receiver to the sender, back to the receiver along with the message, and then back again to the sender along with the acknowledgement.

G also satisfies the requirements of S, but not quite in the same way as SB.

G is organized into a set of implementable actions that also appear, with very minor variations, in both H and C, plus the magic grow, shrink, and cleanup actions that are simulated quite differently in H and in C.

When there are no crashes, the sender and receiver each go through a cycle of modes, the sender perhaps one mode ahead. In one cycle one message is sent and acknowledged. For the sender, the modes are idle, [needI], send; for the receiver, they are idle and ack. An agent that is not idle is busy. The bracketed mode is ‘internal’: it’s possible to advance to the next mode without receiving another message. The modes are not explicit state variables, but instead are derived from the values of the msg and last variables, as follows:

To define G we introduce the types:

The G we give is a somewhat simplified version, because the actions are not as atomic as they should be. In particular, some actions have two external interactions, sometimes one with a channel and one with the client, sometimes two with channels. However, the simplified version differs from one with the proper atomicity only in unimportant details. The appendix gives a version of G with all the fussy details in place. We don’t give these details for the C and H protocols that follow, but content ourselves with the simplified versions in order to emphasize the important features of the protocols.

Figure 10.5 is a more detailed version of Figure 10.4, which shows all the actions and the flow of information between the sender and the receiver. State variables are given in bold, and the black guards on the transitions give the pre-conditions. The mark variable can be # when the receiver has recovered since a message was put; it reflects the fact that the message may be dropped.

In addition to meeting the spec S, this protocol has some other important properties:

10.5.1 Abstraction Function to D

The abstraction function is an essential tool for proving that the protocol implements the spec. But it is also an important aid to understanding what is going on. By studying what happens to the value of the abstraction function during each action of G, we can learn what the actions are doing and why they work.

Note that the inflights exclude elements that might still be retransmitted as well as elements that are not of interest to the destination. This is so the abstraction function can pair them with the # mark.

We see that G simulates the q of D using old-q + cur-q, and that old-q is the leftover messages in the channel that are still good but haven’t been delivered, while cur-q is the message the sender is currently working on, as long as its identifier is not yet assigned or still good. Similarly, status has a different value for each step in the delivery process: still sending the message (a), normal ack (b), ack after a receiver crash (c), lost ack (d), or delivered ack (e).

10.5.2 Invariants

10.5.3 Proof that G Implements D

This requires showing that every action of G simulates some sequence of actions of D which is the same externally. Since G has quite a few actions, the proof is somewhat tedious. A few examples give the flavor.

10.6 How C and H Implement G

We now proceed to give two practical protocols, the clock-based protocol C and the handshake protocol H. Each implements G, but they handle the good sets quite differently.

We begin by giving the abstraction functions from C and H to G, and a sketch of how each implements the magic actions of G, to help the reader in comparing the protocols. Careful study of these should make it clear exactly how each protocol implements G’s magic actions in a properly distributed fashion.

Then for each protocol we give a figure that shows the flow of packets, followed by a formal description of the state and the actions. The portion of the figures that shows messages being sent and acks returned is exactly the same as the bottom half of Figure 10.4 for G; all three protocols handle messages and acks identically. They differ in how the sender obtains good identifiers, shown in the top of the figures, and in how the receiver cleans up its state. In the figures for C and H we show the abstraction function to G in outline font.

10.7 The Clock-Based Protocol C

This protocol is due to Liskov, Shrira, and Wroclawski [1991]. Figure 10.6 shows the state and the flow of information. Compare it with Figure 10.4 for G, and note that there is no flow of new identifiers from receiver to sender. In C the passage of time supplies the sender with new identifiers, and is also allows the receiver to clean up its state.

The idea behind C is to use loosely synchronized clocks to provide the identifiers for messages. The sender uses its current time for the next identifier. The receiver keeps track of low, the biggest clock value for which it has accepted a message: bigger values than this are good. The receiver also keeps a stable bound high on the biggest value it will accept, chosen to be larger than the receiver’s clock plus the maximum clock skew. After a crash the receiver sets low := high; this ensures that no messages are accepted twice.

The sender’s clock advances, which ensures that it will get new identifiers and also ensures that it will eventually get past low and start sending messages that will be accepted after a receiver crash.

If the assumptions about clock skew and maximum packet transmission time are violated, C still provides at-most-once delivery, but it may lose messages (because low is advanced too soon or the sender’s clock is later than high) or acknowledgements (because cleanup happens too soon).

Modes, types, packets, and the pattern of messages are the same as in G, except that the I set has a total ordering. The deadline variable expresses the assumption about maximum packet delivery time: real time doesn’t advance (by progress) past the deadline for delivering a packet. In a real implementation, of course, there will be some other properties of the channel from which the constraint imposed by deadline can be deduced. These are usually probabilistic; we deal with this by declaring a crash whenever the channel fails to meet its deadline.

Note that like G, this version of C sends an ack only in response to a message. This is unlike H, which has continuous transmission of the ack and pays the price of a done message to stop it. Another possibility is to make timing assumptions about rs and time out the ack; some assumptions are needed anyway to make cleanup possible. This would be less practical but more like H.

The protocol is parameterized by three constants:

These parameters must satisfy two constraints:

10.7.1 Invariants

If a message is being sent but hasn’t been delivered, and there hasn’t been a crash, then deadline gives the deadline for delivering the packet containing the message (based on the maximum time for a packet that is being retransmitted to get through sr), and it isn’t too late for it to be accepted (C5).

An identifier getting a positive ack is no later than low, hence no longer good (C6). If it’s getting a negative ack, it must be later than the last one accepted (C7).

10.8 The Handshake Protocol H

This is the standard protocol for setting up network connections, used in TCP, ISO TP-4, and many other transport protocols. It is usually called three-way handshake, because only three packets are needed to get the data delivered, but five packets are required to get it acknowledged and all the state cleaned up (Belsnes [1976]).

As in the generic protocol, when there are no crashes the sender and receiver each go through a cycle of modes, the sender perhaps one ahead. For the sender, the modes are idle, needI, send; for the receiver, they are idle, accept, and ack. In one cycle one message is sent and acknowledged by sending three packets from sender to receiver and two from receiver to sender, for a total of five packets. Table 10.6 summarizes the modes and the packets that are sent.

The modes are derived from the values of the state variables j and last:

Figure 10.7 shows the state, the flow of identifiers from the receiver to the sender at the top, and the flow of done information back to the receiver at the bottom so that it can clean up. These are sandwiched between the standard exchange of message and ack, which is the same as in G (see Figure 10.4).

Intuitively, the reason there are five packets is that:

We introduce a new type:

The sender and receiver send packets to each other. An I or J in the first component is there to identify the packet for the destination. Some packets also have an I or J as the second component, but it does not identify anything; rather it is being communicated to the destination for later use. The (i, a) and (i, done) packets are both often called ’close’ ;packets in the literature.

The H protocol has the same progress and efficiency properties as G, and in addition, although the protocol as given does assume an infinite supply of Is, it does not assume anything about clocks.

It’s necessary for a busy agent to send something repeatedly, because the other end might be idle and therefore not sending anything that would get the busy agent back to idle. An agent also has a set of expected packets, and it wants to receive one of these in order to advance normally to the next mode. To ensure that the protocol is self-stabilizing ;after a crash, both ends respond to an unexpected packet containing the identifier i by sending an acknowledgement: (i, lost) or (i, done). Whenever the receiver gets done for its current I, it becomes idle. Once the receiver is idle, the sender advances normally until it too becomes idle.

10.8.1 Invariants

10.8.2 Progress

We consider first what happens without failures, and then how the protocol recovers from failures.

If either partner fails and then recovers, the other becomes idle rather than getting stuck; in other words, the protocol is self-stabilizing. Why? When the receiver isn’t idle it always sends something, and if that isn’t what the sender wants, the sender responds done, which forces the receiver to become idle. When the sender isn’t idle it’s either in needI, in which case it will eventually get what it wants, or it’s in send and will get a negative ack and become idle. In more detail:

The receiver bails out when the sender crashes because

The sender bails out or makes progress when the receiver crashes because

10.9 Finite Identifiers

Similar observations apply to H, with some minor complications to keep the history variable seen up to date, and a similar recycle-j action. Table 10.8 gives the recycle actions for G and H.

How can we implement the guards on the recycle actions? The tricky part is ensuring that i is not still in a channel, since standard methods can ensure that it isn’t in a variable at the other end. There are three schemes that are used in practice:

For C we can recycle identifiers by using time modulo some period as the identifier, rather than unadorned time. Similar ideas apply; we omit the details.

10.10 Conclusions

We have given a precise specification S of reliable at-most-once message delivery with acknowledgements. We have also presented precise descriptions of two practical protocols (C and H) that implement S, and the essential elements of proofs that they do so; the handshake protocol H is used for connection establishment in most computer networking. Our proofs are organized into three levels: we refine S first into another specification D that delays some of the decisions of S and then into a generic implementation G, and finally we show that C and H both implement G. Most of the work is in the proof that G implements D.

In addition to complete expositions of the protocols and their correctness, we have also given an extended example of how to use abstraction functions and invariants to understand and verify subtle distributed algorithms of some practical importance. The example shows that the proofs are not too difficult and that the invariants, and especially the abstraction functions, give a great deal of insight into how the implementations work and why they satisfy the specifications. It also illustrates how to divide a complicated problem into parts that make sense individually and can be attacked one at a time.

References

Appendix

The state of the full G is:

The abstraction function to D is: