FRAMEWORK FOR UNDERSTANDING DISTRIBUTED (DEADLOCK DETECTION) ALGORITHMS.

Distributed algorithms tend to be difficult to understand and even more difficult to prove correct. Using distributed deadlock detection as a running example, this paper presents a framework for stating, understanding, and proving the correctness of, distributed algorithms for decision problems. The framework consists of a series of complexity levels. To simplify the initial levels, we treat the data structure of the algorithm as a database, and use the database notions of views and transaction atomicity. For each complexity level, we state theorems that need to be proved for each algorithm. The framework is illustrated using several existing deadlock detection algorithms. Finally, it is shown that the framework suggests new algorithms using the best features of several existing algorithms.