The Design and Construction of Deadlock-Free Concurrent Systems

PhD Thesis by J.M.R. Martin, University of Buckingham, UK, 1996

Contact: Jeremy Martin
Oxford University Computing Services
13 Banbury Road
United Kingdom
Phone: 01865 273236

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 (, 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.

Thesis prepared for WWW by Dave Beckett.