AND

We present a new model for describing and reasoning about transaction-processing algorithms. The model provides a comprehensive, uniform framework for rigorous correctness proofs. The model generalizes previous work on concurrency control to encompass nested transactions and type-specific concurrency control algorithms. Using our model, we describe general conditions for a concurrency control algorithm to be correct-i.e., to ensure that transactions appear to be atomic. We also present a new concurrency control algorithm for abstract data types in a nested transaction system. The algorithm uses commutativity proper-ties of operations to allow high levels of concurrency. The results of operations, in addition to their names and arguments, can be used in checking for conflicts, further increasing concurrency. We show, using our general model, that the new algorithm is correct. We also present a read-update locking algorithm due to Moss and prove it correct. The correctness proofs for the algorithms are modular, in the sense that we consider a system structure consisting of many objects, with concurrency control and recovery performed independentl