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