The Queen's Award for Technological Achievement 1990

The award cites the development of occam, which is the first commercially available language to take seriously the problem of programming MIMD parallel machines. Occam goes out of its way to be clear and simple, being designed to be very little more than an implementation of Tony Hoare's CSP. The intellectual leverage gained from the simplicity and elegance of the semantics of occam, is instrumental in the success of the project.

The most tangible commercial success is the design of the floating point arithmetic unit in the T800 transputer. The work was done by Geoff Barrett and David Shepherd, both of whom came to Oxford as students on the MSc in Computation, and both of whom went on to work for INMOS Ltd in Bristol. At the time the work was done Geoff was in Oxford doing his doctoral research in the Programming Research Group, and David was designing chips for INMOS.

When the T800 transputer was designed it was decided that in parallel with an informal development, supported by months of testing against other FPUs, a team would set about a formal development of a correct-by-design unit. In this context "correct" means conforming to the IEEE Standard 754, and a big first step was to decide exactly what the specification required. The IEEE document is partly reliant on the meaning of natural language requirements; Geoff Barrett's recasting of the Standard into the Z specification language [1] is unambiguous and serves as the touchstone for the correctness of the T800 FPU.

The microcode of the T800 FPU was documented in a restricted subset of occam. Using the occam transformation system developed in Oxford [2], David Shepherd demonstrated that this code was equivalent to a more naturally expressed occam program which had been shown to meet the Z specification. The transformation system builds on the simple semantics of occam, as expressed by Bill Roscoe and Tony Hoare in [3], allowing essentially mechanical proof that two programs -- like the specification of the FPU and the implementing microcode -- have the same effect.

There is a very readable non-technical summary of this work in an article in New Scientist [4]. The work is also described in an article published in the Oxford Magazine [5].

References

[1]

Geoff Barrett, Formal Methods applied to a Floating Point Number System, Programming Research Group Technical Monograph PRG-58, Oxford University Computing Laboratory, January 1987.
Also in IEEE Trans Soft Eng, May 1988. pp 611-621.

[2]

Michael Goldsmith, The Oxford occam Transformation system (documentation), Programming Research Group, Oxford University Computing Laboratory, 1988.

[3]

A W Roscoe and C A R Hoare, The Laws of occam Programming, Programming Research Group Technical Monograph PRG-53, Oxford University Computing Laboratory, February 1986.

[4]

David Shepherd and Greg Wilson, Making Chips that Work, New Scientist, No 1664, 13 May 1989. pp 61-64.

[5]

Geraint Jones, Sharp as a Razor: A Queen's Award for the Computing Laboratory, Oxford Magazine, No 59, Summer 1990.