Timing UDP: Mechanized semantics for sockets, threads, and failures

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 experimentallyvalidated post-hoc specification of the UDP/ICMP sockets interface;• develop a timed operational semantics with threads, as such programsare 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 nai've heartbeat failure detection.