Specifying & Reasoning about Extended Transaction Models:
The ACTA Framework


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.


Panos Chrysanthis and Krithi Ramamritham, ``Synthesis of Extended Transaction Models Using ACTA.'' ACM Transactions on Database Systems, 19(3):450-491, September 1994.

Panos Chrysanthis and Krithi Ramamritham. "ACTA: The SAGA Continues." Database Transaction Models for Advanced Applications, A. K. Elmagarmid Ed., Morgan Kaufmann Publishers, 1992.

Panos Chrysanthis (PhD Thesis) "A Framework for Modeling and Reasoning about Extended Transactions", Computer Science Technical Report 91-90

Panos Chrysanthis and Krithi Ramamritham. ``A Formalism for Extended Transaction Models," Proceedings of the Seventeenth International Conference on VLDB, pp. 103-111, September 1991.

Panos Chrysanthis and Krithi Ramamritham. ``ACTA: A Framework for Specifying and Reasoning about Transaction Structure and Behavior," Proceedings of the 1990 ACM SIGMOD International Conference on Management of Data, pp. 194-203, May 1990. (Also, included in Readings in Database Systems, Second Edition, M. Stonebraker Editor, Morgan Kaufmann, 1994.)

Back to the Database Systems Home Page

Comments or questions on this page: panos@cs.pitt.edu
Last Update: 23 June 95