On the Correctness of Orphan Elimination Algorithms.

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