A Hierarchical Proof of an Algorithm for Deadlock Recovery in a System Using Remote Procedure Calls
MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE
Pagination or Media Count:
An algorithm for detecting and recovering from deadlock in a system using remote procedure calls is presented, along with a proof of correctness. The proof uses the IO Automata model of Lynch and Tuttle. First, correctness conditions for the problem are given in terms of IO Automata. Next, a high- level graph-theoretic representation of the algorithm is shown to be correct. then a lower-level formulation of the algorithm, taking into account its distributed nature, is shown to be equivalent to the higher-level representation, and thus correct. In giving the correctness conditions, we introduce client automata, which model the behavior of the users program, and allow almost all details of this user program to be suppressed at both specification and proof time. To simplify the proof of the high-level version of the algorithm, safety properties are proved with a simplified version of the algorithm. Then, the algorithm is transformed to the full version, and it is argued that the safety properties hold for the transformed version. A new technique that can be used either for expanding the number of algorithms to which a proof applies or for simplifying the proof that a lower-level algorithm solves the same problem as a high-level one is presented.
- Computer Programming and Software