A Hierarchical Proof of an Algorithm for Deadlock Recovery in a System Using Remote Procedure Calls

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-...

Full description

Saved in:
Bibliographic Details
Main Author: Troxel, Gregory D
Format: Report
Language:English
Subjects:
ALGORITHMS
AUTOMATA
Computer Programming and Software
DEADLOCK RECOVERY
INPUT OUTPUT MODELS
RECOVERY
SAFETY
SYSTEMS MANAGEMENT
USER NEEDS
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.