On the Correctness of Orphan Elimination Algorithms.
Abstract
In a distributed system, node crashes and network delays can result in orphaned computations: computations that are still running but whose results are no longer needed. Several algorithms have been proposed to detect and eliminate such computations before they can see inconsistent states of the shared, concurrently accessed data. This paper analyzes two orphan elimination algorithms that have been proposed for nested transaction systems describes the algorthms formally, and presents complete detailed proofs of correctness. The author's proofs are remarkably simple, and slow that the fundamental concepts underlying the two algorithms are quite similar. In addition, it is shown formally that the algorithms can be used in combination with any correct concurrency control technique, thus providing formal justification for the informal claims made by the algorithm' designers. The results are a significant advance over eariler work in the area, in which it was extremely difficult to state and prove comparable results.
Document Details
- Document Type
- Technical Report
- Publication Date
- May 01, 1987
- Accession Number
- ADA182175
Entities
People
- Maurice Herlihy
- Michael Merritt
- Nancy Lynch
- William Weihl
Organizations
- Massachusetts Institute of Technology