Abstract
This paper studies the semantics of failure in distributed programming. We present a semantic model for distributed programs that use the standard sockets interface; it covers message loss, host failure and temporary disconnection, and supports reasoning about distributed infrastructure.We consider interaction via the UDP and ICMP protocols. To do this, it has been necessary to: • construct an experimentally validated post-hoc specification of the UDP/ICMP sockets interface; • develop a timed operational semantics with threads, as such programs are typically multithreaded and depend on timeouts; • model the behaviour of partial systems, making explicit the interactions that the infrastructure offers to applications; • integrate the above with semantics for an executable fragment of a programming language (OCaml) with OS library primitives; and • use tool support to manage complexity, mechanizing the model with the HOL theorem prover. We illustrate the whole with a module providing naíve heartbeat failure detection.
Keywords
- Operational Semantic
- Parallel Composition
- Label Transition System
- Internet Protocol Address
- File Descriptor
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.
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
M. K. Aguilera, W. Chen, and S. Toueg. Using the heartbeat failure detector for quiescent reliable communication and consensus in partitionable networks. Theoretical Computer Science, 220(1):3–30, June 1999.
T. Arts and M. Dam. Verifying a distributed database lookup manager written in Erlang. In World Congress on Formal Methods (1), 1999.
F. Baker. Requirements for IP version 4 routers, RFC 1812. Internet Engineering Task Force, June 1995. http://www.ietf.org/rfc.html.
K. Bhargavan, S. Chandra, P. J. McCann, and C. A. Gunter. What packets may come: Automata for network monitoring. In Proc. POPL 2001.
R. Braden. Requirements for internet hosts — communication layers, STD 3, RFC 1122. Internet Engineering Task Force, October 1989.
University of California at Berkeley CSRG. 4.2BSD, 1983.
S. J. Garland, N. Lynch, and M. Vaziri. IOA reference guide, December 2000. http://nms.lcs.mit.edu/~garland/IOA/.
M. J. C. Gordon and T. Melham, editors. Introduction to HOL: a theorem proving environment. Cambridge University Press, 1993.
K. Honda and M. Tokoro. An object calculus for asynchronous communication. In Proceedings of ECOOP’ 91, LNCS 512, pages 133–147, 1991.
[IEE00] IEEE. Portable Operating System Interface (POSIX)-Part xx: Protocol Independent Interfaces (PII), P1003.1g. March 2000.
X. Leroy et al. The Objective-Caml System, Release 3.02. INRIA, July 30 2001. Available http://caml.inria.fr/ocaml/.
N. Lynch and F. Vaandrager. Forward and backward simulations-Part II: Timing-based systems. Information and Computation, 128(1):1–25, 1996.
M. Norrish. C formalised in HOL. PhD thesis, Computer Laboratory, University of Cambridge, 1998.
M. Norrish and K. Slind. A thread of HOL development. Computer Journal, 2002. To appear.
J. Postel. User Datagram Protocol, STD 6, RFC 768. Internet Engineering Task Force, August 1980. http://www.ietf.org/rfc.html.
J. Postel. Internet Protocol, STD 5, RFC 791. Internet Engineering Task Force, September 1981. http://www.ietf.org/rfc.html.
I. Schieferdecker. Abruptly terminated connections in TCP — a verification example. In Proc. COST 247 International Workshop on Applied Formal Methods in System Design, pages 136–145, 1996.
R. Segala, R. Gawlick, J. Søgaard-Andersen, and N. Lynch. Liveness in timed and untimed systems. Inf. and Comp., 141:119–171, 1998.
M. Smith. Formal verification of communication protocols. In FORTE/PSTV’96, pages 129–144, 1996.
A. Serjantov, P. Sewell, and K. Wansbrough. The UDP calculus: Rigorous semantics for real networking. In Proc TACS2001, Sendai, October 2001.
A. Serjantov, P. Sewell, and K. Wansbrough. The UDP calculus: Rigorous semantics for real networking. TR 515, Computer Laboratory, University of Cambridge, July 2001. http://www.cl.cam.ac.uk/users/pes20/Netsem/.
W. R. Stevens. TCP/IP Illustrated Vol. 1: The Protocols. Addison-Wesley, 1994.
W. R. Stevens. UNIX Network Programming Vol. 1: Networking APIs: Sockets and XTI. Prentice Hall, second edition, 1998.
M. VanInwegen. The machine-assisted proof of programming language properties. PhD thesis, University of Pennsylvania, December 1996.
K. Wansbrough, M. Norrish, P. Sewell, and A. Serjantov. Timing UDP: the HOL model, 2001. http://www.cl.cam.ac.uk/users/pes20/Netsem/.
W. Yi. CCS + time = an interleaving model for real time systems. In Proc. ICALP 1991, LNCS 510, pages 217–228, 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wansbrough, K., Norrish, M., Sewell, P., Serjantov, A. (2002). Timing UDP: Mechanized Semantics for Sockets, Threads, and Failures. In: Le Métayer, D. (eds) Programming Languages and Systems. ESOP 2002. Lecture Notes in Computer Science, vol 2305. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45927-8_20
Download citation
DOI: https://doi.org/10.1007/3-540-45927-8_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43363-7
Online ISBN: 978-3-540-45927-9
eBook Packages: Springer Book Archive