A Theory of Timestamp-Based Concurrency Control for Nested Transactions

In this paper we present a rigorous framework for analyzing concurrency control and recovery algorithms for nested transactions. We describe general sufficient conditions for ensuring correctness, and apply these conditions to timestamp-based concurrency control algorithms. We define a local correctness property for individual objects, local static atomicity, that affords useful modularity, both in decomposing proofs and in building systems.