Contact: Jeremy Martin
Oxford University Computing Services
13 Banbury Road
Oxford
OX2 6NN
United Kingdom
Phone: 01865 273236
Email: jeremy.martin@oucs.ox.ac.uk
ABSTRACT
It is a difficult
task to produce software which is guaranteed never to fail, but
it is a vital goal for which to strive in many real-life
situations. The problem is especially complex in the field of
parallel programming, where there are extra things that can go
wrong. A particularly serious problem is Here we consider how
to construct systems which are guaranteed deadlock-free by
design. Design rules, old and new, which eliminate deadlock
are catalogued, and their theoretical foundation
illuminated. Then the development a software engineering tool
is described which proves deadlock-freedom by verifying
adherence to these methods. Use of this tool is illustrated
with several case studies. The thesis concludes with a
discussion of related issues of parallel program
reliability.
The thesis can be viewed in its entirety as a single gzipped PostScript file (thesis.ps.gz, 151 pages, 286K) or each chapter can be viewed individually. A list of the chapters is given below with the title of the chapter, the original page numbers in the gzipped PostScript documents, the page count and the absolute page ranges.