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, packet 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 b...

• Type: Conference
• Year: 2001
• Where: TACS
• Authors: Andrei Serjantov, Peter Sewell, Keith Wansbrough
• Keywords: Particular Programming Language, Practical Distributed Programs, Software Engineering, Subtle Portability Issues, TACS 2001