The UDP Calculus: Rigorous Semantics for Real Networking
Network programming is notoriously hard to understand: one has to deal with a variety of protocols (IP, ICMP , UDP, TCP etc.), concurrency, pac ket loss, host failure, timeouts, the complex sockets interface to the protocols, and subtle portability issues. Moreover, the behavioural properties of operating systems and the network are not well documented.
A few of these issues have been addressed in the process calculus and distributed algorithm communities, but there remains a wide gulf between what has been captured in semantic models and what is required for a precise understanding of the behaviour of practical distributed programs that use these protocols.
In this paper we demonstrate (in a preliminary way) that the gulf can be bridged. We give an operational model for socket programming with a substantial fraction of UDP and ICMP,including loss and failure. The model has been validated by experiment against actual systems. It is not tied to a particular programming language,but can be used with any language equipped with an operational semantics for system calls — here we give such a language binding for an OCaml fragment. We illustrate the model with a few small network programs.
KeywordsSystem Call Real Networking Operational Semantic Process Calculus Library Call
Unable to display preview. Download preview PDF.
- [AD99]T. Arts and M. Dam. Verifying a distributed database lookup manager written in Erlang. In World Congress on Formal Methods (1), pages 682–700, 1999.Google Scholar
- [AP94]R. Amadio and S. Prasad. Localities and failures. In Foundations of Software Technology and Theoretical Computer Science, LNCS 880. Springer, 1994.Google Scholar
- [Bak95]F. Baker. Requirements for IP version 4 routers. Internet Engineering Task Force, June 1995. http://www.ietf.org/rfc.html.
- [BCMG01]K. Bhargavan, S. Chandra, P. J. McCann, and C. A. Gunter. What packets may come: Automata for network monitoring. In Proc. POPL 2001, January 2001.Google Scholar
- [BH00]M. Berger and K. Honda. The two-phase commit protocol in an extended — calculus. In Proceedings of the 7th International Workshop on Expressiveness in Concurrency, EXPRESS’ 00, 2000.Google Scholar
- [Bia94]E. Biagioni. A structured TCP in standard ML. In Proc. SIGCOMM, 1994.Google Scholar
- [Bra89]R. Braden. Requirements for internet hosts-communication layers, STD 3, RFC 1122. IETF, October 1989. http://www.ietf.org/rfc.html.
- [FGL+96]C. Fournet, G. Gonthier, J.-J. L-evy, L. Maranget, and D. R-emy. A calculus of mobile agents. In Proc. CONCUR’ 96, LNCS 1119. Springer, August 1996.Google Scholar
- [GLV00]S. J. Garland, N. Lynch, and M. Vaziri. IOA reference guide, December 2000. http://nms.lcs.mit.edu/~garland/IOA/.
- [Hay98]M. Hayden. The Ensemble System. PhD thesis, Cornell University, January 1998. Technical Report TR98-1662.Google Scholar
- [HT91]K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proceedings of ECOOP’ 91, LNCS 512, pages 133–147, July 1991.Google Scholar
- [IEE00]IEEE. Information Technology-Portable Operating System Interface (POSIX)-Part xx: Protocol Independent Interfaces (PII), P1003.1g. 2000.Google Scholar
- [INM87]INMOS. Occam2 Reference Manual. Prentice-Hall, 1987.Google Scholar
- [L+00]X. Leroy et al. The Objective-Caml System, Release 3.00. INRIA, April 27 2000. http://caml.inria.fr/ocaml/.
- [Lyn96]_ N. A. Lynch. Distributed algorithms. Morgan Kaufmann, 1996.Google Scholar
- [Mul93]S. J. Mullender. Distributed Systems. ACM Press, 1993.Google Scholar
- [Pos80]J. Postel. User Datagram Protocol, STD 6, RFC 768. Internet Engineering Task Force, August 1980. http://www.ietf.org/rfc.html.
- [Pos81]J. Postel. Internet Protocol, STD 6, RFC 791. Internet Engineering Task Force, September 1981. http://www.ietf.org/rfc.html.
- [PT00]B. C. Pierce and D. N. Turner. Pict: A programming language based on the pi-calculus. In Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000.Google Scholar
- [Rep91]J. Reppy. CML: A higher-order concurrent language. In Proc. Programming Language Design and Implementation (PLDI), pages 293–259, June 1991.Google Scholar
- [RH97]J. Riely and M. Hennessy. Distributed processes and location failures. In Automata, Languages and Programming, LNCS 1256. Springer, 1997.Google Scholar
- [Sew97]P. Sewell. On implementations and semantics of a concurrent programming language. In Proceedings of CONCUR’ 97, LNCS 1243, pages 391–405, 1997.Google Scholar
- [SSW01]A. Serjantov, P. Sewell, and K. Wansbrough. The UDP calculus: Rigorous semantics for real networking. Technical Report 515, Computer Laboratory, University of Cambridge, 2001. http://www.cl.cam.ac.uk/users/pes20/Netsem.
- [Ste94]W. R. Stevens. TCP/IP Illustrated: The Protocols, volume 1 of Addison-Wesley Professional Computing Series. Addison-Wesley, 1994.Google Scholar
- [Ste98]W. R. Stevens. UNIX Network Programming, Networking APIs: Sockets and XTI, volume 1. Prentice Hall, second edition, 1998.Google Scholar
- [Swi01]The SwitchWare project. http://www.cis.upenn.edu/~switchware, 2001.
- [TLK96]B. Thomsen, L. Leth, and T.-M. Kuo. A Facile tutorial. In Proceedings of CONCUR’ 96, LNCS 1119, pages 278–298. Springer-Verlag, August 1996.Google Scholar