EPSRC grant EP/C510712, 2005-2008

Peter Sewell, Keith Wansbrough, Richard Gibbens, Michael Norrish.

The existing global information infrastructure is extremely complex. It rests on network protocols (TCP, UDP, IP, with their Sockets API) which provide the low-level services of byte-stream and asynchronous datagram communication; higher-level middleware layers, providing directories, messaging, failure detection, resource allocation, etc, and programming languages for writing both middleware and applications. The sum is very poorly understood. Consequently, the construction of distributed infrastructure is still a matter of craft, requiring a great deal of specialised experience and painful testing. There has been much (essential) theoretical work on idealised models, but, with some exceptions, it remains far removed from the intricacies of real systems. Our poor grasp of the foundations carries a great risk that the infrastructure we build today will be inadequate for the future: brittle, unreliable, and inefficient.

To remedy this state of affairs, we will develop mathematical models of the behaviour of the network protocols and the Sockets API, as they are deployed, that precisely describe both normal behaviour and the many failure and error cases. Our models will be expressed with a higher-order-logic proof assistant (HOL). We aim to make them readily usable by middleware designers and implementors, validating the models against the deployed implementations and drawing feedback from the community. We will integrate the models with programming language semantics, thereby supporting automated reasoning about executable distributed programs, and will use them as a basis for pre-hoc design work for future protocols, especially proposals for congestion control based on resource pricing.

We will thereby establish techniques for rigorous semantic modelling of real systems, and demonstrate their feasibility and benefits.

[Validate this page.]