The ability of transactions to mask the effects of concurrency and failures makes them appropriate building blocks for emerging advanced applications such as design environments. Several extensions have been proposed to the transaction model adopted in traditional database systems in order to support the functional and performance requirements of these complex systems. Often, however, given a particular extended transaction model, its properties as well as its scope of applicability are unclear.
To facilitate the formal description of transaction properties in an extended transaction model, we have developed ACTA, a comprehensive transaction framework. Specifically, using ACTA, one can specify and reason about the nature of interactions between extended transactions in a particular model. ACTA characterizes the semantics of interactions (1) in terms of different types of dependencies between transactions (e.g., commit dependency and abort dependency) and (2) in terms of transactions' effects on objects (their state and concurrency status, i.e., synchronization state). Through the former, one can specify relationships between significant (transaction management) events, such as begin, commit, abort, delegate, split, and join, pertaining to different transactions. Also, conditions under which such events can occur can be specified precisely. Transactions' effects on object's state and status are specified by associating a view and a conflict set with each transaction and by stating how these are affected when significant events occur. A view of a transaction specifies the state of objects visible to that transaction while the transaction's conflict set contains those operations with respect to which conflicts need be considered.
The framework is capable of accommodating complex objects, as well as semantics-based multi-level concurrency control and recovery techniques. It has the potential to characterize transaction models that associate different semantics with the notions of visibility, consistency, recovery, and permanence. Its ability to capture the semantics of previously proposed transaction models is indicative of its generality. The reasoning capabilities of this framework have also been tested by using the framework to study the properties of new models derived either by combining existing transaction models or by extending existing transaction models using the ACTA formalism. In addition, ACTA can be used to show the correctness of a particular implementation of a transaction model by first formalizing the properties of the specific mechanisms used in the implementation and then showing that they will maintain the correctness properties of the model.
Back to the Database Systems Home Page