Concurrency Control for Resilient Nested Transactions.
Abstract
A formal framework is developed for providing correctness of algorithms which implement nested transactions. In particular, a simple action tree data structure is defined, which describes the ancestor relationships among executing transactions and also describes the views which different transactions have of the data. A generalization of serializability to the domain of nested transactions with failures is defined. A characterization is given for this generalization of serializability, in terms of absence of cycles in an appropriate dependency relation on transactions. A slightly simplified version of Moss' locking algorithm is presented in detail, and a careful correctness proof is given. The style of correctness proof appears to be quite interesting in its own right. The description of the algorithm, from its initial specification to its detailed implementation, is presented as a series of event-state algebra levels, each of which simulates the previous one in a straightforward way. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 1983
- Accession Number
- ADA132501
Entities
People
- Nancy Lynch
Organizations
- Massachusetts Institute of Technology