Abstract

Deadlock detection is a fundamental problem in a distributed system and has been extensively studied in the past few years. Many distributed deadlock detection/resolution alg·orithms have been proposed, but most of them either have not given a correctness proof or have given an informal proof by using intuitive operational arguments. Informal arguments are prone to errors and many of the published algorithms have been fouud to be incorrect. In trying to avoid this situation, the development of a formal approach to the algorithm correctness proof is required.

In this work, a formal resource deadlock model with global and local clocks is presented and the definition of deadlock is formally specified. A formal approach which uses the deadlock specification for algorithm correctness verification is proposed. A novel feature of the proposed approach is that it abstracts the system state and process behavior by predicates, and uses the predicates to prove the desired properties of the algorithm. Examples of applying the proposed approach to different algorithms demonstrate that the proposed deadlock model offers a paradigm for the formal verification of most distributed probe-based deadlock detection algorithms.

Few of the algorithms proposed in the literature address the issue of handling process failures in a distributed system. This work also proposes a new fault-tolerant distributed deadlock detection algorithm which integrates a priority-based probe algorithm with a PMC-based diagnosis model.

Department(s)

Computer Science

Comments

The first Author is a Graduate Student.

This report is substantially the Ph.D. dissertation of the first author, completed Summer 1994.

Report Number

CSc-94-15

Document Type

Technical Report

Document Version

Final Version

File Type

text

Language(s)

English

Rights

© 1994 University of Missouri - Rolla, All rights reserved

Publication Date

1 June, 1994

Download

Share

 
COinS