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
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 PDF or 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 PDF documents, the page count and the absolute page ranges.

• Frontispiece (PDF, 24K)
  i-ix (10 pages, 1-10)
• Introduction: PDF, 22K and HTML, 10K
  1-4 (4 pages, 11-14)
• Chapter 1. CSP and Deadlock (PDF, 171)
  5-33 (29 pages, 15-43)
• Chapter 2. Design Rules for Deadlock Freedom (PDF, 184K)
  34-61 (28 pages, 44-71)
• Chapter 3. A Tool for Proving Deadlock-Freedom (PDF, 238K)
  62-105 (44 pages, 72-115)
• Chapter 4. Engineering Applications (PDF, 104K)
  106-123 (18 pages, 116-133)
• Conclusions and Directions for Future Work (PDF, 46K)
  124-129 (6 pages, 134-139)
• References (PDF, 23K)
  130-133 (4 pages, 140-143)
• Appendix A: Partial Orders (PDF, 23K)
  134-135 (2 pages, 144-145)
• Appendix B: Graphs and Digraphs (PDF, 48K)
  136-141 (6 pages, 146-151)