A Hierarchical Proof of an Algorithm for Deadlock Recovery in a System Using Remote Procedure Calls
Abstract
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 I/O Automata model of Lynch and Tuttle. First, correctness conditions for the problem are given in terms of I/O 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 user's 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1990
- Accession Number
- ADA222116
Entities
People
- Gregory D. Troxel
Organizations
- Massachusetts Institute of Technology