article

Free access

Synthesis of extended transaction models using ACTA

Editor: Won Kim Authors:

Panos K. Chrysanthis,

Krithi RamamrithamAuthors Info & Claims

ACM Transactions on Database Systems (TODS), Volume 19, Issue 3

Pages 450 - 491

https://doi.org/10.1145/185827.185843

Published: 01 September 1994 Publication History

PDF eReader

Abstract

ACTA is a comprehensive transaction framework that facilitates the formal description of properties of extended transaction models. Specifically, using ACTA, one can specify and reason about (1) the effects of transactions on objects and (2) the interactions between transactions. This article presents ACTA as a tool for the synthesis of extended transaction models, one which supports the development and analysis of new extended transaction models in a systematic manner. Here, this is demonstrated by deriving new transaction definitions (1) by modifying the specifications of existing transaction models, (2) by combining the specifications of existing models, and (3) by starting from first principles. To exemplify the first, new models are synthesized from atomic transactions and join transactions. To illustrate the second, we synthesize a model that combines aspect of the nested- and split-transaction models. We demonstrate the latter by deriving the specification of an open-nested-transaction model from high-level requirements.

References

[1]

BADRINATH, B., AND RAMAMRITHAM, K 1992. Semantics-based concurrency control: Beyond commutativity ACM Trans. Database Syst. 17, I (Mar.)

Digital Library

Google Scholar

[2]

BERNSTEIN, P. A, HADZILACOS, V., AND GOODMAN, N 1987. Concurrenc' ControZ and Recovery in Database Systems. Addlson-Wesley, Readmg, Mass

Digital Library

Google Scholar

[3]

BUCHMANN, A, Oz,su, M T., }ylORMICK, M, GEORGOKOPOULOS, O., AND MANOLA, F. A. 1992. A transaction model for active dlstnbuted object systems. In Database Transaction Models for Advanced Appltcatlons, A. K. Elmagarmid, Ed. Morgan Kaufmann, San Mateo, Calif, 123-158.

Digital Library

Google Scholar

[4]

BUKHRE8, O. A, CHEN, J, DU, W., ELIvlAGARMID, A. K., AND PEZZOLI, R. 1993. Interbase: An execution environment for heterogeneous software systems. IEEE Comput. 28, 8 (Aug.), 57-69.

Digital Library

Google Scholar

[5]

CHRY8ANTHIS, P. K. 1991. ACTA, a framework for modeling and reasoning about extended transactions. Ph.D. thesis, Dept. of Computer and Information Science, Umv of Massachusetts, Amherst.

Google Scholar

[6]

CHRYSANTH{S, P K., AND RAMAMRITHAM, K. 1992. ACTA: The SAGA continues, m Database Transactwtz Models for Advanced Applwatzons. Morgan Kaufmann, San Mateo, Calif.

Digital Library

Google Scholar

[7]

CHRYSANTHIS, P. K., AND RAMAMRiTHAM, K. 1991a. A umfying framework for transactions in competitwe and cooperative environments. IEEE Bull. Offme Knowl Eng. 4 (Feb,), 3 21.

Digital Library

Google Scholar

[8]

CHRYSANTHIS, P. K., AND RAMAMRITHAM, K. 1991b. A formalism for extended transaction models. In ProceedLngs of t/le 17th Internattonal Corlference on Very Large Data Bases VLDB Endowment.

Digital Library

Google Scholar

[9]

CHR~SANTmS, P. K., AND RA~i~4R~THAM, K. 1990, ACTA: A framework for specifymg and reasonmg about transaction structure and behavior. In Proceedmgs of the ACM SIGMOD illterlzatmnal Conference on Management o/Data. ACM, New York, 194-203.

Digital Library

Google Scholar

[10]

C, HRYSANTHIS, P. K, RAGHURAM, S., AND RAMAMRITHAM~ K. 1991 Extracting concurraney from objects: A methodology. In Proceedmgs of the ACM SIGMOD International Co~zference on Management of Data. ACM, New York, 108-117.

Digital Library

Google Scholar

[11]

DU, W, AND ELMAOA-Mm, A. K. 1989. Quasi senalizability: A correctness criterion for global concurrency control in InterBase. In Proceedmgs of the 15th Internatmnal Conference on Ve~~ Large Databa,~es. VLDB. Endowment, 347 355

Digital Library

Google Scholar

[12]

ELMAGARMID, A., (ED.) 1992 Database Transactwn Models for Advanced App{~catzons. Morgan Kaufmanm San Mateo, Ca}if

Digital Library

Google Scholar

[13]

FERNANDEZ, M., ANr~ ZnONIK, S. 1989. Transaction groups: A model for controlhng cooperative transactions. In Proceed~ngs of the Workshop on Persistent Oblect Systems: Their Destgn, Imp{ementatmn and Use. 128 138

Digital Library

Google Scholar

[14]

GARCIA-MOLINA, H., AND SALEM, K. 1987. SAGAS. In Proceedings of the ACM SIGMOD International Conference on Management of Data. ACM, New York, 249-259.

Digital Library

Google Scholar

[15]

HERLIHY, M. P., AND WEIHL, W. 1988. Hybrid concurrency control for abstract data types. In Proceedings of the 7th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems. ACM, New York, 201-216.

Digital Library

Google Scholar

[16]

KORTH, H. F., AND SPEEGLE, G. 1988. Formal models of correctness without serializability. In Proceedings of the ACM SIGMOD Internattonal Conference on Management of Data. ACM, New York, 379-386.

Digital Library

Google Scholar

[17]

MOHAN, C., HADERLE, D., LINDSAY, B., PIRAHESH, H., AND SCHWARZ, P. 1992. ARIES: A transaction recovery method supporting fine-granularity locking and partial rollbacks using writeahead logging. ACM Trans. Database Syst. 17, 1, 94-162.

Digital Library

Google Scholar

[18]

Moss, J. E. B. 1981. Nested transactions: An approach to reliable distributed computing. Ph.D. thesis, MIT, Cambridge, Mass.

Google Scholar

[19]

Pu, C., KA~SER, G., AND HUTCHINSON, N. 1988. Split-transactions for open-ended activities. In Proceedings of the 14th International Conference on Very Large Data Bases. VLDB Endowment, 26-37.

Digital Library

Google Scholar

[20]

SCHWARZ, P. M., AND SPECTO~, A. Z. 1984. Synchronizing shared abstract data types. ACM Trans. Comput. Syst. 2, 3 (Aug.), 223-250.

Digital Library

Google Scholar

[21]

SKARRA, A. 1991. Localized correctness specifications for cooperating transactions in an objectoriented database. IEEE Bull. Office Knowl. Eng. 4, I (Feb.), 79 106.

Digital Library

Google Scholar

[22]

SnET~, A., RUSINKIEWJCZ, M., AND KARABAT~S, G. 1992. Polytransactions: A mechanism for management of interdependent data. In Database Transactwn Models for Advanced Applications. Morgan Kaufmann, San Mateo, Cali~

Google Scholar

[23]

STEMPLE, D. W., AND MORRISON, R. 1992. Specifying flexible concurrency control schemes: An abstract operational approach. In Annual Australian Computer Science Conference. Australian Comput. Sct. Commun. 14, 2, 873 892.

Google Scholar

[24]

VEIJALAINE, J., AND ELIASSEN, E. 1992. The S-transaction model. In Database Transaction Models for Advanced Appl~catzons. Morgan Kaufmann, San Mateo, Cali~

Digital Library

Google Scholar

[25]

W~CHTER, H., AND REUTER, A. 1992. The ConTract Model. In Database Transactwn Models for Advanced Appltcatwns. Morgan Kaufmann, San Mateo, Calif.

Digital Library

Google Scholar

[26]

WEIHL, W. 1984. Specification and implementation of atomic data types. Ph.D. thesis, MIT, Cambridge, Mass.

Google Scholar

[27]

WEIHL, W. 1988. Commutat~vity-based concurrency control for abstract data types. IEEE Trans Comput. 37, 12 (Dec.), 1488-1505.

Digital Library

Google Scholar

Cited By

View all

Tao YLi BLi B(2024)On Atomicity and Confidentiality Across Blockchains Under FailuresIEEE Transactions on Knowledge and Data Engineering10.1109/TKDE.2023.325584236:2(766-780)Online publication date: 1-Feb-2024
https://dl.acm.org/doi/10.1109/TKDE.2023.3255842
Sutra PShapiro M(2022)Database Consistency ModelsEncyclopedia of Big Data Technologies10.1007/978-3-319-63962-8_203-2(1-12)Online publication date: 24-May-2022
https://doi.org/10.1007/978-3-319-63962-8_203-2
Reznichenko V(2021)60 Years of DatabasesPROBLEMS IN PROGRAMMING10.15407/pp2021.03.040(040-071)Online publication date: Sep-2021
https://doi.org/10.15407/pp2021.03.040
Show More Cited By

Index Terms

Recommendations

Synthesis of Extended Transaction Models Using ACTA
Alternative correctness criteria for multiversion concurrency control and a locking protocol via freezing
IDEAS '97: Proceedings of the 1997 International Symposium on Database Engineering & Applications

Concurrency control protocols based on multiversions have been used in some commercial transaction processing systems in order to provide the serializable executions of transactions. In the existing protocols, transactions are allowed to read only the ...
Management of Flexible Transactions Using Semantics in Multidatabase Systems
COMPSAC '95: Proceedings of the 19th International Computer Software and Applications Conference

In a multidatabase system where the autonomy of local database systems is an important requirement, the transaction management is a major issue because it is very difficult to have a good concurrency control algorithm without violating local autonomy. ...

Reviews

Reviewer: Özgür Ulusoy

ACTA is presented as a tool to support the development and analysis of extended transaction models. The authors show how the building blocks of ACTA are used for the development of new transaction models in a systematic manner. ACTA is a first-order-logic-based formalism. It allows the specification of the interactions between transactions and the effects of transactions on objects' states. The behavioral properties of transactions are specified in terms of the set of events associated with a transaction model, the semantics of these events (in terms of their effects on objects and other transactions), the view of a transaction, and the conflict set of a transaction. The view of a transaction specifies the state of objects visible to that transaction, and the conflict set of a transaction specifies which conflicts need to be considered for each operation. ACTA can be used to synthesize transaction models either by tailoring existing models or by starting from first principles. Each case is exemplified in the paper. The nested-split transaction model is derived by combining the axiomatic definitions of nested transactions and split transactions. An open-nested transaction model is synthesized starting from first principles. The authors point out that the ACTA formalism can also be used to show the correctness of a particular implementation of a transaction model. This paper should be of great interest to anyone familiar with the transaction concept in database systems. Although the paper is theoretical, it is well written and quite readable for anyone involved in the area.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Database Systems

ACM Transactions on Database Systems Volume 19, Issue 3

Sept. 1994

169 pages

ISSN:0362-5915

EISSN:1557-4644

DOI:10.1145/185827

Editor:
Won Kim
UniSQL Inc., Austin, TX

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 1994

Published in TODS Volume 19, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

168
Total Citations
View Citations
953
Total Downloads

Downloads (Last 12 months)129
Downloads (Last 6 weeks)28

Reflects downloads up to 14 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Tao YLi BLi B(2024)On Atomicity and Confidentiality Across Blockchains Under FailuresIEEE Transactions on Knowledge and Data Engineering10.1109/TKDE.2023.325584236:2(766-780)Online publication date: 1-Feb-2024
https://dl.acm.org/doi/10.1109/TKDE.2023.3255842
Sutra PShapiro M(2022)Database Consistency ModelsEncyclopedia of Big Data Technologies10.1007/978-3-319-63962-8_203-2(1-12)Online publication date: 24-May-2022
https://doi.org/10.1007/978-3-319-63962-8_203-2
Reznichenko V(2021)60 Years of DatabasesPROBLEMS IN PROGRAMMING10.15407/pp2021.03.040(040-071)Online publication date: Sep-2021
https://doi.org/10.15407/pp2021.03.040
Cai SGallina BNyström DSeceleanu C(2021)Specification and automated verification of atomic concurrent real-time transactionsSoftware and Systems Modeling (SoSyM)10.1007/s10270-020-00819-020:2(557-589)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10270-020-00819-0
Shapiro MSutra P(2019)Database Consistency ModelsEncyclopedia of Big Data Technologies10.1007/978-3-319-77525-8_203(591-601)Online publication date: 20-Feb-2019
https://doi.org/10.1007/978-3-319-77525-8_203
Ettazi WHafiddi HNassar M(2018)A Context-Driven Commit Protocol for Enhancing Transactional Services Performance in Pervasive EnvironmentsInternational Journal of Advanced Pervasive and Ubiquitous Computing10.4018/IJAPUC.201810010210:4(14-28)Online publication date: 1-Oct-2018
https://dl.acm.org/doi/10.4018/IJAPUC.2018100102
Cai SGallina BNystrom DSeceleanu C(2018)Specification and Formal Verification of Atomic Concurrent Real-Time Transactions2018 IEEE 23rd Pacific Rim International Symposium on Dependable Computing (PRDC)10.1109/PRDC.2018.00021(104-114)Online publication date: Dec-2018
https://doi.org/10.1109/PRDC.2018.00021
Shapiro MSutra P(2018)Database Consistency ModelsEncyclopedia of Big Data Technologies10.1007/978-3-319-63962-8_203-1(1-11)Online publication date: 19-Feb-2018
https://doi.org/10.1007/978-3-319-63962-8_203-1
Karabatis G(2018)Split TransactionsEncyclopedia of Database Systems10.1007/978-1-4614-8265-9_725(3665-3666)Online publication date: 7-Dec-2018
https://doi.org/10.1007/978-1-4614-8265-9_725
Salem K(2018)SagasEncyclopedia of Database Systems10.1007/978-1-4614-8265-9_724(3273-3273)Online publication date: 7-Dec-2018
https://doi.org/10.1007/978-1-4614-8265-9_724
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract

References

Cited By

Index Terms

Recommendations