Model for concurrency in nested transactions systems

A model for database concurrency control permits nested transactions. In this model, transactions may execute subtransactions, giving rise to tree-structured computations. A serializability theory is developed for this model, which can be used to prove the correctness of concurrency control algorithms for nested transactions and for multilevel database systems. The theory is based on an abstract model of computation that allows arbitrary operations and parallel and even nondeterministic programs. Axioms are presented that express the basic properties that programs that manage or access data need to satisfy and are used to derive proof techniques. The proof techniques are illustrated by applying them to several well-known concurrency control problems.