Using Formal Methods to Reason about Semantics-Based Decompositions of Transactions.

Paul Ammann, Sushil Jajodia, Indrakshi Ray: Using Formal Methods to Reason about Semantics-Based Decompositions of Transactions. VLDB 1995: 218-227
  author    = {Paul Ammann and
               Sushil Jajodia and
               Indrakshi Ray},
  editor    = {Umeshwar Dayal and
               Peter M. D. Gray and
               Shojiro Nishio},
  title     = {Using Formal Methods to Reason about Semantics-Based Decompositions
               of Transactions},
  booktitle = {VLDB'95, Proceedings of 21th International Conference on Very
               Large Data Bases, September 11-15, 1995, Zurich, Switzerland},
  publisher = {Morgan Kaufmann},
  year      = {1995},
  isbn      = {1-55860-379-4},
  pages     = {218-227},
  ee        = {db/conf/vldb/AmmannJR95.html},
  crossref  = {DBLP:conf/vldb/95},
  bibsource = {DBLP,}


Many researchers have investigated the process of decomposing transactionsinto smaller pieces to increase concurrency. The research typically focuses on implementing a decomposition supplied bythe database application developer, with relatively little attention to what constitutes a desirable decomposition and how the developer should obtain such a decomposition. In this paper, we argue that the decomposition process itself warrants attention. A decomposition generates a set of proof obligations that must be satisfied to show that a particular decomposition correctly models the original collection of transactions. We introduce the notion of semantic histories to formulate and prove the necessary properties. Since the decomposition impacts not only the atomicity of transactions, but isolation and consistency as well, we present a technique based on formal methods that allows these properties to be surrendered in a carefully controlled manner.

Copyright © 1995 by the VLDB Endowment. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the VLDB copyright notice and the title of the publication and its date appear, and notice is given that copying is by the permission of the Very Large Data Base Endowment. To copy otherwise, or to republish, requires a fee and/or special permission from the Endowment.

Online Paper

ACM SIGMOD Anthology

CDROM Version: Load the CDROM "Volume 1 Issue 5, VLDB '89-'97" and ... DVD Version: Load ACM SIGMOD Anthology DVD 1" and ... BibTeX

Printed Edition

Umeshwar Dayal, Peter M. D. Gray, Shojiro Nishio (Eds.): VLDB'95, Proceedings of 21th International Conference on Very Large Data Bases, September 11-15, 1995, Zurich, Switzerland. Morgan Kaufmann 1995, ISBN 1-55860-379-4
Contents BibTeX


Divyakant Agrawal, Amr El Abbadi, Ambuj K. Singh: Consistency and Orderability: Semantics-Based Correctness Criteria for Databases. ACM Trans. Database Syst. 18(3): 460-486(1993) BibTeX
Philip A. Bernstein, Vassos Hadzilacos, Nathan Goodman: Concurrency Control and Recovery in Database Systems. Addison-Wesley 1987, ISBN 0-201-10715-5
Contents BibTeX
B. R. Badrinath, Krithi Ramamritham: Semantics-Based Concurrency Control: Beyond Commutativity. ACM Trans. Database Syst. 17(1): 163-199(1992) BibTeX
Panos K. Chrysanthis, Krithi Ramamritham: Synthesis of Extended Transaction Models Using ACTA. ACM Trans. Database Syst. 19(3): 450-491(1994) BibTeX
Weimin Du, Ahmed K. Elmagarmid: Quasi Serializability: a Correctness Criterion for Global Concurrency Control in InterBase. VLDB 1989: 347-355 BibTeX
Abdel Aziz Farrag, M. Tamer Özsu: Using Semantic Knowledge of Transactions to Increase Concurrency. ACM Trans. Database Syst. 14(4): 503-525(1989) BibTeX
Hector Garcia-Molina: Using Semantic Knowledge for Transaction Processing in Distributed Database. ACM Trans. Database Syst. 8(2): 186-213(1983) BibTeX
Hector Garcia-Molina, Kenneth Salem: Services for a Workflow Management System. IEEE Data Eng. Bull. 17(1): 40-44(1994) BibTeX
Maurice Herlihy: Extending Multiversion Time-Stamping Protocols to Exploit Type Information. IEEE Trans. Computers 36(4): 443-448(1987) BibTeX
Maurice Herlihy, William E. Weihl: Hybrid Concurrency Control for Abstract Data Types. J. Comput. Syst. Sci. 43(1): 25-61(1991) BibTeX
Sushil Jajodia, Catherine Meadows: Mutual Consistency in Decentralized Distributed Systems. ICDE 1987: 396-404 BibTeX
Henry F. Korth, Gregory D. Speegle: Formal Model of Correctness Without Serializability. SIGMOD Conference 1988: 379-386 BibTeX
Henry F. Korth, Gregory D. Speegle: Formal Aspects of Concurrency Control in Long-Duration Transaction Systems Using the NT/PV Model. ACM Trans. Database Syst. 19(3): 492-535(1994) BibTeX
Nancy A. Lynch: Multilevel Atomicity - A New Correctness Criterion for Database Concurrency Control. ACM Trans. Database Syst. 8(4): 484-502(1983) BibTeX
Susan S. Owicki, David Gries: Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19(5): 279-285(1976) BibTeX
Lui Sha, John P. Lehoczky, E. Douglas Jensen: Modular Concurrency Control and Failure Recovery. IEEE Trans. Computers 37(2): 146-159(1988) BibTeX
Dennis Shasha, Eric Simon, Patrick Valduriez: Simple Rational Guidance for Chopping Up Transactions. SIGMOD Conference 1992: 298-307 BibTeX
William E. Weihl: Commutativity-Based Concurrency Control for Abstract Data Types. IEEE Trans. Computers 37(12): 1488-1505(1988) BibTeX
Helmut Wächter, Andreas Reuter: The ConTract Model. Database Transaction Models for Advanced Applications 1992: 219-263 BibTeX

Referenced by

  1. Paul Ammann, Sushil Jajodia, Indrakshi Ray: Applying Formal Methods to Semantic-Based Decomposition of Transactions. ACM Trans. Database Syst. 22(2): 215-254(1997)
ACM SIGMOD Anthology - DBLP: [Home | Search: Author, Title | Conferences | Journals]
VLDB Proceedings: Copyright © by VLDB Endowment,
ACM SIGMOD Anthology: Copyright © by ACM (, Corrections:
DBLP: Copyright © by Michael Ley (, last change: Sat May 16 23:46:05 2009