The pursuit of buffer tolerance

Photograph of Bill Roscoe

Bill Roscoe

(Oxford)

Process algebras such as CSP use handshaken communication on channels. Other models of interaction such as dataflow use buffered channels, and frequently real systems contain some quantity of buffering that may well be nondeterministic. CSP can model these things by the insertion of extra processes onto channels, but the resulting systems tend to have very large state spaces. A network is said to be buffer tolerant if the addition of buffering on one or more channels does not affect its satisfaction of some specification. This is a desirable property since it means that verifying a buffer-free implementation proves it for versions with buffers in.

In this talk I will give formal definitions of buffer tolerance and identify classes of network in which it is automatically true. An important sort of component of buffer tolerant networks are processes which act as monotonic functions on their input streams. I will identify a remarkable finitary test for this property.
Tuesday 7th December 2004, 14:00
Robert Recorde Room
Department of Computer Science