Sliding Window Protocol

INTRODUCTIONS TO SLIDING WINDOW PROTOCOL :

• The Sliding Window (SW) protocol has been widely used in many popular communication protocols. The protocol can ensure a correct data transfer over very poor quality communication channels where the packets may be duplicated, lost, or re-ordered .A number of parameters affects the performance characteristics of the SW protocol. Usually, these performance characteristics cannot be determined analytically. However, we need to study these key performance characteristics and to identify optimal parameter settings in the early design phases when parameter settings in the early design phases when designing an adaptive algorithm or novel protocols for specific computing environments. Such information is helpful for the designer to work out a product. In this paper we introduce the sliding window protocol generally, describe the communication procedure of the protocol, and conclude some related parameters affecting the overall performance of the system. In order to estimate the performance of the SW protocol systematically, as an exercise, an abstract executable performance model of the protocol using go back n is created in POOSL. The model allows us to present and analyze some performance characteristics. These performance characteristics include the throughput (the bandwidth utilization) of the protocol and the delay of the acknowledgement. Some key-parameters such as the window size, the timeout period, the round trip time, the packet size, and the probability of packets loss are investigated in several network environments and different parameter settings as well.

• A simple performance analysis is also presented in the same the well-known Sliding Window protocol caters for the reliable and efficient transmission of data over unreliable channels that can lose, reorder and duplicate messages. Despite the practical importance of the protocol and its high potential for errors, it has never been formally verified for the general setting. We try to fill this gap by giving a fully formal specification and verification of an improved version of the protocol. The protocol is specified by a timed state machine in the language of the verification system PVS. This allows a mechanical check of the proof by the interactive proof checker of PVS. Our modeling is very general and includes such important features of the protocol as sending and receiving windows of arbitrary size, bounded sequence numbers and channels that may lose, reorder and duplicate messages.

• Reliable transmission of data over unreliable channels is an old and well-studied problem in computer science. Without a satisfactory solution, computer networks would be useless, because they transmit data over channels that often lose, duplicate, or reorder messages. One of the most efficient protocols for reliable transmission is the Sliding Window (SW) protocol. Many popular communication protocols such as TCP and HDLC are based on the SW protocol.

• Communication protocols usually involve a subtle interaction of a number of distributed components and have a high degree of parallelism. This is why their correctness is difficult to ensure, and many protocols turned out to be erroneous. One of the most promising solutions to this problem is the use of formal verification, which requires the precise specification of the protocol in some specification language and a formal proof of its correctness by mathematical techniques.

• Formal verification is especially useful when it uses some form of mechanical support, such as a model checker or an interactive theorem prover. However, formal verification of communication protocols is notoriously difficult. Even verification of a version of the Alternating Bit protocol (Which is one of the simplest communication protocols), namely the Bounded Retransmission Protocol of Philips Electronics turned out to be nontrivial. The use of model checking for verification of the BRP is problematic due to the infinite state space of the protocol (caused by unbounded ness of the message data, the retransmission bound, and the file length). In only restricted versions of the protocol could be model-checked; the manually derived constraints have been checked by parametric model-checking in revealing a small error. More general correctness proofs by theorem provers also encounter many technical difficulties.
  

• Despite the practical significance of the Sliding Window protocol, the work on its formal verification had only a limited success so far. Stunning only gave an informal manual proof for his protocol. A semi-formal manual proof is also presented in. A more formal, but not fully automated proof for the window size of one is given in, and for the arbitrary window size in. Some versions of the protocol have been model-checked for small parameter values. The combination of abstraction techniques and model-checking in allowed verifying the SW protocol for a relatively large window size of 16 (which is still a few orders less than a possible window size in TCP). Almost all of these verifications assume data link channels, which can only lose messages. The protocols for such channels, called data link protocols, are important (they include, e.g., HDLC, SLIP and PPP protocols), but they are only used for transmission of data over relatively short distances. The verification of sliding window protocols for more general transport channels, which can also reorder and duplicate messages. Such channels are already considered in the original paper on the SW protocol by Stenning.

• The protocols for such channels (called transport protocols), such as TCP, can transmit data over very large networks such as the Internet. Note that an SW protocol does not exist for all types of transport channels. As shows, for a fully asynchronous system and channels that can both lose and reorder messages, it is impossible to design an efficient transmission protocol that uses bounded sequence numbers. A similar result is proved for systems that can both reorder and duplicate messages. In unbounded sequence numbers are assumed for verification of the SW protocol for transport channels. This makes the verification rather simple, because it is known that the repetition of sequence numbers is the main source of errors for SW protocols.

• Unfortunately, transmission protocols that use unbounded sequence numbers are usually not practical. Because of the impossibility results mentioned above, a SW protocol for transport channels with bounded sequence numbers can only be designed for systems, in which each message in a channel has a maximum lifetime1. Such a SW protocol is a part of the TCP protocol, which operates over 1 Such protocols can also be designed for untimed systems which limit the reordering of messages but such systems seem to be only of theoretical interest.

• Verification and Improvement of the Sliding Window Protocol transport channels with a given maximum packet lifetime. The theoretical basis of that protocol is presented .TCP uses 232 sequence numbers, which is enough to represent 4 gigabytes of data. The transmission mechanism of TCP uses a complicated timing mechanism to implement sequence numbers in such a way that their periodical repetition does not cause ambiguity. It often requires the sender and the receiver to synchronize on the sequence numbers they use. Such synchronization is provided by the three-way handshake protocol, which is not a part of the SW protocol and correctness of which is not easy to ensure. In general, the transmission mechanism of TCP seems too complicated and too specific for TCP to serve as a good starting point for verification of SW protocols for transport channels. Another approach is chosen. Shankar presents a version of the SW protocol for transport channels with the maximum packet lifetime, which does not require any synchronization between the sender and the receiver, and also does not impose any restrictions on the transmission policy. However, the range of sequence numbers, required to ensure the correctness of his protocol, depends on the maximum transmission rate of the sender. In the case of TCP, his protocol would only work correctly if the sender did not send into the channel more than some 30 megabytes of data per second (if we take 120 seconds for the maximum packet lifetime in TCP, as in). Such restriction may not be practical for modern networks, which are getting faster every year. Indeed, the range of sequence numbers in a large industrial protocol like TCP is fixed. Therefore, if the available transmission rate at some point exceeds our expectations, we would need to re-design the whole protocol to allow for faster transmission, which may be costly. In this paper, we present a new version of the SW protocol for transport channels.

• In our opinion, it combines some of the best features of the transmission mechanism of TCP and Shankar’s protocol. We do not require any synchronization between the sender and the receiver. Maximum packet lifetime and appropriate transmission and acknowledgment policies are used to ensure the correct recognition of sequence numbers. These policies are rather simple; roughly speaking, they require the sender (receiver) to stop and wait for the maximum packet lifetime after receiving acknowledgment for (delivering) the maximum sequence number, respectively. Unlike some previous works the range of sequence numbers used by our protocol does not depend on the transmission rate of the sender. Therefore, between the required periods of waiting, the sender may transmit data arbitrarily fast, even if the range of sequence numbers is fixed2, e.g. as in TCP. If implemented for TCP, our protocol would allow transmitting files up to 4 gigabytes arbitrarily fast.

• Even for relatively simple communication protocols, manual formal verification is so lengthy and complicated that it can easily be erroneous. This is why we need some form of mechanical support. Our protocol highly depends on com- 2 Of course, the average transmission rate of our protocol over the long run does depend on the range of sequence numbers, because the fewer sequence numbers the protocol has, the more often it has to stop and wait after the maximum number.

• Hence completely automatic verification is not feasible for us. This is why we use an interactive theorem prover. We have chosen PVS because we have an extensive experience with it and successfully applied the tool to verification of several complicated protocols. PVS, which is based on higher-order logic, has a convenient specification language and is relatively easy to learn and to use. The rest of the paper is organized as follows.