Fifo Channels from Unreliable Channels

  • A. Udaya Shankar


Fifo, lossy, and LRD connection-less channels were presented in the previous chapter. This chapter presents a distributed program that implements a connection-less fifo channel between two addresses a1 and a2, given an unreliable, i.e., lossy or LRD, connection-less channel connecting the two addresses. Henceforth we omit the “connection-less” qualifier when referring to these channels. The program has a component system at each address, which accepts messages from its local user, transfers them over the unreliable channel to the remote component system, which then delivers them in order to the remote user. Figure 5.1 illustrates the configuration. In computer networking, such a program is referred to as a data transfer protocol [4, 9, 10]. Following this terminology, we refer to the distributed program as DtpDist and the program of each component system as Dtp, where “dtp” is short for data transfer protocol. We refer to the messages exchanged between the dtp users as “data blocks”, and reserve the term “messages” for the messages exchanged between the dtp systems; the former would be sent inside the latter.


Sequence Number Data Block Local User Atomic Step Remote User 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    M. Allman, V. Paxson, E. Blanton, TCP congestion control. Technical report, RFC 5681, Internet Engineering Task Force, 2009.
  2. 2.
    D. Belsnes, Single-message communication. IEEE Trans. Commun. 24(2), 190–194 (1976). doi:10.1109/TCOM.1976.1093283CrossRefGoogle Scholar
  3. 3.
    D. Chkliaev, J. Hooman, E.P. de Vink, Verification and improvement of the sliding window protocol, in TACAS 2003, ed. by H. Garavel, J. Hatcliff. Lecture Notes in Computer Science (Springer, Berlin/New York, 2003), pp. 113–127Google Scholar
  4. 4.
    D. Comer, Principles, Protocols, and Architectures. Internetworking with TCP/IP, vol. 1, 4th edn. (Prentice-Hall, Englewood Cliffs, 2000)Google Scholar
  5. 5.
    D.E. Knuth, Verification of link-level protocols. BIT 21(1), 31–36 (1981)MathSciNetMATHGoogle Scholar
  6. 6.
    M. Mathis, J. Mahdavi, S. Floyd, A. Romanow, TCP selective acknowledgement options. Technical report, RFC 2018, Internet Engineering Task Force, 1996.
  7. 7.
    A.L. Oláh, Design and analysis of transport protocols for reliable high-speed communications. Ph.D. thesis, University of Twente, Enschede, the Netherlands, 1997.
  8. 8.
    A.L. Oláh, S.M. Heemstra de Groot, Alternative specification and verification of a periodic state exchange protocol. IEEE/ACM Trans. Netw. 5(4), 525–529 (1997). doi:10.1109/90.649467.
  9. 9.
    L.L. Peterson, B.S. Davie, Computer Networks: A Systems Approach, 3rd edn. (Morgan Kaufmann Publishers Inc., San Francisco, 2003)Google Scholar
  10. 10.
    A.U. Shankar, Verified data transfer protocols with variable flow control. ACM Trans. Comput. Syst. 7(3), 281–316 (1989). doi:10.1145/65000.65003.
  11. 11.
    A.U. Shankar, S.S. Lam, A stepwise refinement heuristic for protocol construction. ACM Trans. Program. Lang. Syst. 14(3), 417–461 (1992). doi:10.1145/129393.129394. Earlier version appeared in Stepwise Refinement of Distributed Systems, LNCS 430, Springer-Verlag, 1990

Copyright information

© Springer Science+Business Media New York 2013

Authors and Affiliations

  • A. Udaya Shankar
    • 1
  1. 1.Department of Computer ScienceUniversity of MarylandCollege ParkUSA

Personalised recommendations