Technical reports

The UDP calculus:
rigorous semantics for real networking

Andrei Serjantov, Peter Sewell, Keith Wansbrough

July 2001, 70 pages

DOI: 10.48456/tr-515

Abstract

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 protability 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.

Full text

PS (0.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-515,
  author =	 {Serjantov, Andrei and Sewell, Peter and Wansbrough, Keith},
  title = 	 {{The UDP calculus: rigorous semantics for real networking}},
  year = 	 2001,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-515.ps.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-515},
  number = 	 {UCAM-CL-TR-515}
}