Communication Protocols

One of the application case studies currently being pursued by the TDS Group involves communication protocols. Among the projects are:

Smith and Lynch worked out carefully an impossibility result for the at-most-once fast delivery problem that the T/TCP improvement of TCP is designed to solve. This result establishes the problem cannot be solved if the client and server do not have accurate clocks.

Smith is working with Lynch and Clark on a verification of basic TCP, to be extended to a verification of a new optimization of TCP known as T/TCP.

Lampson, Lynch and Soegaard-Anderson completed a study of two protocols for at-most-once message delivery in unreliable networks: the five-packet interchange protocol used in TCP, ISO TP-4 and elsewhere, and a clock-based protocol invented by Liskov, Shrira and Wroclawski. The study involved a unified presentation of the two protocols, as implementations of a common high-level "generic protocol"; it is not at all obvious that the two protocols have enough in common to be described in this way. Complete proofs are given, using invariants and forward and backward simulations (timed and untimed). This work appears in Jorgen's thesis [1] and complete tech report; a summary appears in FORTE 93 and also in Mullender book, latest edition [2].

Gawlick has produced a collection of non-greedy algorithms for admission control and routing in various common types of networks. Some of these algorithms are of mainly theoretical interest, but others have been engineered for practical use, and have led to several patents. Optimality results, using competitive analysis, have also been proved.

Kleinberg, Attiya, and Lynch have proved tradeoff upper and lower bounds for the time required for establishing a connection and the time required for quiescence, in connection management protocols. This study includes results for both the asynchronous model and various models with partial timing information. The results appeared in ISTCS95.

[1] Joergen Soegaard-Andersen. Correctness of Protocols in Distributed Systems. PhD thesis, Department of Computer Science, Technical University of Denmark, Lyngby, Denmark, December 1993. ID-TR: 1993-131.

[2] Butler W. Lampson. Reliable Messages and Connection Establishment In Sape Mullender, editor, Distributed Systems, chapter 10, pages 251-281. ACM Press and Addison-Wesley, 1993, second edition.

TOC / LCS / MIT Last modified: Mon Nov 2 17:05:35 1998	Comments?