CLICK TO TECH

The transmitter window shown in Figure is used for buffering the unacknowledged frames. The variable lowestunack is used as an indicator for the lowest sequence number of an unacknowledged frame which has not necessarily been sent. Initially it is set to1.The variable highest sent indicates the sequence number of the last sent frame and is initialized by 0.Both values determine the size of the transmitting window bounded by the constant tws.

If the transmitter wants to send a data frame, then it has to check first whether the actual window size (highestsent-lowestunack) is less than tws.If this condition is not fulfilled the data frame is not sent until it is possible_ In the other case the transmitter increments highestsent by one_ emits the data combined with highestsent as sequence number and starts a timer for that sequence number. Whenever a correct acknowledgement (not corrupted and with a sequence number greater or equal than lowestunack) is received, all timers for frames with lower sequence numbers beginning by the received one down to lowestunack are cancelled. Then lowestunack is set to the received sequence number incremented by one. When a timeout occurs all timers according to the sequence number of the message for which the timeout has occurred up to highestsent are reset and the corresponding frames are retransmitted in a sequential order starting with the message for which the timeout occurred. This includes also the repeated starting of the timers.

In Figure the second window, which is located at the receiver is presented. The receiver window is used to buffer the received frames which can not yet be handed out to the user because some frame with a lower sequence number has not been received. The variable next required whose initial value is 1, is used to indicate the sequence number of the next expected frame. The maximum size of the receiver window is described by the constant rws.If a noncorrupted frame is received with a sequence number in the range of (nextrequired...nextrequired-rws + 1) all messages starting by nextrequired up to the first not received message are delivered to the user. Then nextrequired is set to the number of the first not received message and nextrequired -1 is sent as an acknowledgement to the transmitter.

Figure: Receiver window

2.1.1 BASIC NOTIONS

Sender and receiver

In a SW protocol, there are two main components: the sender and the receiver. The sender obtains an infinite sequence of data from the sending host. We call indivisible blocks of data in this sequence “frames”, and the sequence itself the “input sequence”. The input sequence must be transmitted to the receiver via an unreliable network. After receiving a frame via the channel, the receiver may decide to accept the frame and eventually deliver it to the receiving host. The correctness condition for a SW protocol says that the receiver should deliver the frames to the receiving host in the same order in which they appear in the input sequence.

Messages and channels

In order to transmit a frame, the sender puts it into a frame message together with some additional information, and sends it to the frame channel. After the receiver eventually accepts the frame message from this channel, it sends an acknowledgment message for the corresponding frame back to the sender. This acknowledgment message is transmitted via the acknowledgment channel. After receiving an acknowledgment message, the sender knows that the corresponding frame has been received by the receiver. The communication channels connect the sender and the receiver. Usually, the channels are unreliable and bi-directional. The packets may be duplicated, lost, or re-ordered in the channels, and will be delayed a time through the channels. In the SW protocol, the data frames are sent by the sender to the frame channel, and the acknowledgement frames are sent by the receiver to the channel: the acknowledgement channel.

Sequence numbers

The sender sends the frames in the same order in which they appear in its input sequence. However, the frame channel is unreliable, so the receiver may receive these frames in a very different order (if receive at all). Therefore it is clear that each frame message must contain some information about the order of the corresponding frame in the input sequence. Such additional information is called “sequence number”. To acknowledge a frame, in the acknowledgment message the receiver sends the sequence number with which the frame was received. Acknowledgments are “accumulative”; for example, when the sender acknowledges a frame with sequence number 3, it means that frames with sequence numbers 0, 1 and 2 have also been accepted.

Sending and Receiving Window:-

At any instant of time, the sender maintains a sending window of consecutive sequence numbers corresponding to frames it is permitted to send. These sequence numbers within the sending window represent frames sent but not yet acknowledged. Similarly, the receiver maintains a receiving window, corresponding to the number of out of order frames it is permitted to accept. Any frames falling outside the receiving window are discarded without comment. In our model we give an assumption of the same window size in the sender and the receiver.

1. Sending window

At any time, the sender maintains a sequence of sequence numbers corresponding to frames it is permitted to send. These frames are said to be a part of the sending window. Similarly, the receiver maintains a receiving window of sequence numbers it is permitted to accept. In our protocol, the sizes of sending and receiving windows are equal and represented by an arbitrary integer N.

At some point during the execution it is possible that some frames in the beginning of the sending window have been already sent, but not yet acknowledged, and the remaining frames have not been sent yet. When an acknowledgment arrives for a frame in the sending window that has been already sent, this frame and all preceding frames are removed from the window as acknowledgments are accumulative. Simultaneously, the window is shifted forward, such that it again contains N frames. As a result, more frames can be sent. Acknowledgments that fall outside the window are discarded. If a sent frame is not acknowledged for a long time, it usually means that either this frame or an acknowledgment for it has been lost. To ensure the progress of the protocol, such a frame is eventually resent. Many different policies for sending and resending of frames exist [Tan96], which take into account, e.g., the efficient allocation of resources and the need to avoid network congestion. Here we abstract from such details of the transmission policy and specify only those restrictions on protocol’s behaviors that are needed to ensure its safety property.

2. Receiving window

During the execution, the receiving window is usually a mix of sequence numbers corresponding to frames that have been accepted out of order and sequence numbers corresponding to “empty spaces”, i.e. frames that are still expected. When a frame arrives with a sequence number corresponding to some empty space, it is accepted, i.e. inserted in the window, otherwise it is discarded. At any time, if the first element of the receiving window is a frame, it can be delivered to the receiving host, and the window is shifted by one. The sequence number of the last delivered frame can be sent back to the sender to acknowledge the frame (for convenience reasons, in this version we acknowledge delivered frames instead of accepted frames). Not every frame must be acknowledged; it is possible to deliver a few frames in a row and then acknowledge only the last of them. If the receiver does not deliver any new frames for a long time, it may resend the last acknowledgment to ensure the progress of the protocol.

Communication procedure

In the beginning of communication between the sender and receiver, the sending window and the receiving window are empty. The sender is starting to send data frames to the receiver via the frame channel. On the other side, the receiver is waiting for receiving data frames from the network. Whenever a new packet arrives at the sender from the network layer, the next highest sequence number according to the sending window is given, and the upper edge of the sending window is advanced by one. The sender puts the packet and the sequence number with some other control information into a frame, and then sends the frame to the frame channel. After transmitting a frame, the sender starts a new timer running for the corresponding to this frame in the sending window in our model. The timeout period of the timers must be chosen to allow enough time for the frame to get to the receiver, for the receiver to process it in the worst case, and for the acknowledgement frame to propagate back to the sender.

Performance parameters

A number of parameters affect the performance of the SW protocol. Here we conclude some key-parameters in our model.

Packet size

The size of the embedded packet in a frame. A packet is the unit of information exchanged between the network layer and the data link layer in the same machine, or between network layer peers. In our model, we give an assumption that the packet size is fixed.

Maximum window size

Window size is the number of the unacknowledged frames in the sending window or in the receiving window. The sender and the receiver are of the same maximum window size w in our model. Each of the sender and the receiver needs w buffers to hold the unacknowledged frames.

Timeout period A timer will go off within the timeout period.

Bandwidth

It is the maximum amount of data passing the channel at a given time. Usually, it depends on the medium capacity of the communication channels itself.

Process time of a packet

It is the time it takes for a packet to send/receive to/from the channel, so Ts=S/B.

Channel delay and round trip time

Channel delay is the time it takes for data to travel across the channel. Round trip time is the time it takes for data to travel across the channel from the sender to the receiver and then back.

Probability of packets loss

It is the probability of packets loss in the data frame channel or in the acknowledgement frame channel. In our model, we will study various situations such as packets lossless and different probabilities of packets loss (e.g. 1%, 2% or 5%).

2.2 RELATING SEQUENCE NUMBERS AND WINDOW SIZE

For data link channels we need K ≥ 2 ∗ N to ensure the unambiguous recognition of sequence numbers. However, for transport channels this condition is not sufficient. Indeed, suppose that window size N = 1 and we use K = 2 sequence numbers, so we only have sequence numbers 0 and 118. Suppose the sender sends the first two frames f0 and f1 to the receiver, which are success fully accepted, delivered and acknowledged. Suppose, however, that f0 has been duplicated in the frame channel and subsequently reordered with f1, so the channel still contains frame f0 with sequence number 0. The receiver now has a window with an empty space and sequence number 0, so it can receive frame f0 for the second time, violating the safety property. In this case, the error is caused by the combination of message reordering and duplication; a similar erroneous scenario can be constructed using reordering and loss.

This simple example clearly shows that we need additional restrictions on the protocol to recognize sequence numbers correctly. Traditional approaches introduce a stronger restriction on K, which essentially has the form K ≥ 2∗N + f(Rmax, Lmax), where Rmax is the maximum transmission rate of the sender, Lmax is the maximum message lifetime, and f is some function. As we already explained in the introduction, such dependence between the range of sequence numbers and the maximum transmission rate is undesirable.

This is why in our protocol we only require K ≥ 2 ∗ N, but introduces some timing restrictions on the transmission and acknowledgment policies (explained below) to ensure that frames and acknowledgments are not received more than once.

2.3 TIMING RESTRICTIONS

In our protocol, the sender is allowed to reuse sequence number 0 and all subsequent sequence numbers only after more than Lmax time units have passed since the receipt of the acknowledgment with the maximum sequence number K − 1. This is necessary to ensure that when sequence number 0 is resent, all “old” acknowledgments, i.e. those for frames preceding the current frame, are already removed from the acknowledgment channel (because their timeouts expired), and cannot be mistaken for “new” acknowledgments, i.e. those for the current frame and its successors. Similarly, the receiver is allowed to accept sequence number 0 (or any subsequent sequence numbers) only after more than Lmax time units have passed since the delivery of a frame with the maximum sequence number K − 1. This is necessary to ensure that all “old” frames have been removed from the frame channel and cannot be mistaken for “new” frames. To implement these restrictions, our protocol keeps two variables tackmax and tdelmax, expressing the time when we received an acknowledgment for sequence number K − 1, and delivered a frame with sequence number K − 1, respectively.

We were surprised to discover during the verification that these restrictions are not quite sufficient. It is the acknowledgment for the maximum sequence number K − 1 that causes the problem. In the initial version of the protocol, acknowledgments for a particular frame could be resent at any time. Suppose that between the receipt of an acknowledgment for sequence number K − 1 and the sending of sequence number 0 by the sender, the acknowledgment for sequence number K − 1 is resent by the receiver. Then this acknowledgment may still be in the channel at the time when sequence number K − 1 is sent Verification and Improvement of the Sliding 1. As a result, this “old” acknowledgment may be mistaken for a newly sent acknowledgment.

So, the sender will think that a frame with sequence number K − 1 is acknowledged, whereas in fact it could have been lost. We constructed a (lengthy) scenario in which such incorrect receipt of acknowledgments eventually leads to incorrect receipt of frames and violation of the safety property. To fix this error, in the revised version of the protocol the acknowledgment with sequence number K − 1 must be sent immediately after the corresponding frame is delivered, and it cannot be resent. Considering that acknowledgments can be lost, this results in a possibility of deadlock. We are not very concerned about this, since any reasonable implementation of the SW protocol also does not allow resending acknowledgments at any time (only if there is a strong suspicion that the original message has been lost). In our protocol, we prefer to abstract away from such implementation details. However, we also constructed a modification of our protocol (presented below) that does not suffer from this deadlock problem.

Possible improvement.

The simplest way to prevent the acknowledgment with sequence number K − 1 from being accepted again is to introduce the additional waiting period for the sender. Before the sender resends sequence number K−1, it should wait for more than Lmax time units after accepting the acknowledgment with sequence number K − 2. This ensures the elimination of all “old” acknowledgments with sequence number K −1. As a result, it becomes possible to acknowledge a particular frame with sequence number K − 1 more than once and this resolves the deadlock problem. However, it is obvious that this additional waiting period greatly reduces the performance of the protocol. We specified this modification of our protocol in PVS, but we did not verify it for two reasons. Firstly, it is not clear whether the degradation in performance is justified. In a complex distributed system, it is not reasonable to avoid deadlock at any cost. It may be more efficient to allow a deadlock in some rare situations, and to use an additional protocol to resolve it. Secondly, this additional waiting period would make the verification of the protocol even more complex without adding much theoretical value to it.

2.4 FORMAL SPECIFICATION

Formally, in our approach a protocol is defined by the notion of a state, representing a snapshot of the state-of-affairs during protocol execution, and a set of actions. For the SW protocol, we have actions of sender and receiver, and a delay action. Our timing model can be considered a simplified version of timed automata, in which there is only one clock (called time) that is never reset. Actions are specified by a precondition and an effect predicate which relates the states before and after action execution. First we define the data structure of the protocol. For the sender, the window “slides” over the infinite input sequence input. We do not specify the nature of the frames in the input sequence. Variable first denotes the first frame in the sending window, ftsend is the first frame that has not been sent yet, and we always have first ≤ ftsend ≤ first+N. Thus, at any moment of time, frames with indices from first to ftsend−1 (if any) have been sent but not yet acknowledged, and frames with indices from ftsend to first+N −1 (if any) are in the sending window but not sent yet. Variable tackmax expresses the time when we received the acknowledgment with the maximum sequence number K − 1 for the last time. As a time domain Time, we take the set of non-negative real numbers.

Sender:

1) input: sequence [Frames],

2) first: nat,

3) ftsend: nat,

4) tackmax: Time

For the receive r, output is the finite output sequence, rwindow is the receiving window with N elements (which are either frames or empty spaces, denoted by ε), lastdel is the last delivered sequence number, acklastdel is a Boolean variable which tells whether we are allowed to send the acknowledgment for lastdel to the sender, and variable tdelmax expresses the time when we delivered the frame with the maximum sequence number K −1 for the last time (the importance of variables acklastdel and tdelmax is explained in subsection 2.3).

Receiver:

1) output: finite sequence [Frames],

2) rwindow: {0, 1, . . . N − 1} −→ (snumber: {0, 1 . . . K − 1}),

3) lastdel: {0, 1, . . . K − 1},

4) acklastdel: bool,

5) tdelmax: Time

The frame channel and the acknowledgment channel are represented by its contents, namely a set of frame messages and a set of acknowledgment messages, respectively. Besides a sequence number and possibly a frame, in our model each message includes its timeout, i.e. the latest time when it must be removed from the channel. When a message is sent, we assign as its timeout the current time plus Lmax, where Lmax is the maximum message lifetime. Note that timeout is only used to model maximum message lifetime, it cannot be used by the recipient of a message.

Frame Message:

1) snumber: {0, 1, . . . K − 1},

2) frame: Frames,

3) timeout: Time

AckMessage:

1) snumber: {0, 1, . . . K − 1},

2) timeout: Time

The complete state of the protocol consists of the sender, the receiver and the two channels fchannel and achannel, together with the variable time, indicating the current time. The initial state of the protocol is defined in a rather obvious way, i.e. 0 is assigned to most fields.

State:

1) sender: Sender,

2) receiver: Receiver,

3) fchannel FrameMessage,

4) achannel AckMessage,

5) time: Time

There are seven atomic actions in our protocol: one general (Delay), three for the sender (Send, Resend and Receiveack) and three for the receiver (Receive, Sendack and Deliver). Due to space limitations, we only give an informal description of these actions. The full specification of the protocol can be found in the PVS files, available via [URL]. In the rest of the paper, operator mod K gives a remainder to a modulus K. Note that actions for sending and receiving messages are nondeterministic. Actions for sending messages (Send, Resend and Sendack) either add a message to the channel (which models its successful sending) or let the channel unchanged (which models loss of a message). Actions for receiving messages Receiveack and Receive) either remove a message from the channel (which models its “normal” reception) or let the channel unchanged (which models duplication of a message). The reordering of messages is modeled by representing both channels by unordered sets.

Also note that the sender and the receiver are “input enabled” (e.g., as in I/O automata of Lynch; they are always willing to receive a message from the channel. This is necessary to ensure that all messages can be received before their timeouts expire. If certain conditions are met, the received message is accepted, changing the state of the sender (receiver), otherwise it is discarded.

2.4.1 THE DELAY ACTION

Action Delay (t) expresses the passing of t units of time. The precondition of this action expresses that time cannot be advanced above the minimal time-out value in channels. Hence, any message in a channel must be removed, and E. de Vink channel before its timeout expires. The effect predicate expresses that the new state equals the old state except for the value of time which is incremented by t.

2.4.2 ACTIONS OF THE SENDER

1. Send.

This action sends the first frame that has not been sent yet, i.e. the frame with index ftsend, and ftsend mod K is included into the message as its sequence number. The precondition of this action expresses that sequence number 0 can be reused only after more than Lmax time units have passed since the last acknowledgment of sequence number K − 1, and only if 0 is the first sequence number in the window, i.e. if ftsend mod K = 0, then we require 1) time > tackmax + Lmax and 2) first = ftsend.

2. Resend (i).

This action resends a frame that has already been sent but not yet acknowledged, i.e. a frame with index i such as i ≥ first and i < ftsend.

3. Receiveack (am).

This action receives acknowledgment message am and checks whether snumber(am) lies within the sending window. If so, the frames with sequence numbers up to snumber(am) are removed from the window and the window is shifted accordingly, and if snumber(am) = K−1, then the current time is assigned to the variable tackmax. Otherwise, the message is discarded.

2.4.3 ACTIONS OF THE RECEIVER

1. Receive (fm).

This action receives frame message fm and checks whether snumber (fm) corresponds to some empty space in the receiving window. If so, it accepts the message if more than Lmax time units have passed since the last delivery of a frame with sequence number K − 1. The exact formalization of this requirement is subtle because frames can be accepted and delivered in different order; it is defined by giving a restriction on the position of snumber(fm) in the window in addition to the timing restriction time > tdelmax + Lmax .If these conditions for acceptance are satisfied, then the frame from the message is inserted into the corresponding place in the window; otherwise the message is discarded.

2. Sendack.

This action sends an acknowledgment for the last delivered frame, i.e. the frame with sequence number lastdel. If lastdel = K − 1, it changes the value of variable acklastdel to false. The precondition of Sendack requires acklastdel to be true, and this prevents the acknowledgment for K − 1 from being resent.

3. Deliver.

The precondition of this action requires that the first element of the receiving window is a frame. If it is the case, the frame is appended to the output sequence and removed from the window, i.e. the window is shifted by one. Also, the sequence number of the frame is assigned to lastdel, if this Verification and Improvement of the Sliding Window Protocol 123 sequence number is K−1, then the current time is assigned to tdelmax, and acklastdel becomes equal to true. In addition to the preconditions of individual actions, we also specify an additional assertion expressing that each delivery of the sequence number K −1 is immediately followed by action Sendack acknowledging this sequence number.