Commutativity-Based Locking for Nested Transactions

Abstract
A new model is introduced for reasoning about atomic transactions. This model allows careful statement of the correctness conditions to be satisfied by transaction-processing algorithms, as well as clear and concise description of such algorithms. It also serves as a framework for rigorous correctness proofs. A new algorithm is introduced for general commutativity- based locking in nested transaction systems. This algorithm and a previously- known read-update locking algorithm are presented and proved correct using the new model. The proofs are based on Serializability Theorem and a new dynamic atomicity condition for data objects. Keywords: Data loses, Input output automata.

This publication has 0 references indexed in Scilit: