dblp.uni-trier.de www.dagstuhl.de www.uni-trier.de

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
@inproceedings{DBLP:conf/vldb/AmmannJR95,
  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        = {http://www.vldb.org/conf/1995/P218.PDF},
  crossref  = {DBLP:conf/vldb/95},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

Abstract

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.


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 CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML

References

[AAS93]
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) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[AJR95]
...
[BHG87]
Philip A. Bernstein, Vassos Hadzilacos, Nathan Goodman: Concurrency Control and Recovery in Database Systems. Addison-Wesley 1987, ISBN 0-201-10715-5
Contents CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[BR92]
B. R. Badrinath, Krithi Ramamritham: Semantics-Based Concurrency Control: Beyond Commutativity. ACM Trans. Database Syst. 17(1): 163-199(1992) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[CR94]
Panos K. Chrysanthis, Krithi Ramamritham: Synthesis of Extended Transaction Models Using ACTA. ACM Trans. Database Syst. 19(3): 450-491(1994) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[DE90]
Weimin Du, Ahmed K. Elmagarmid: Quasi Serializability: a Correctness Criterion for Global Concurrency Control in InterBase. VLDB 1989: 347-355 CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[FO89]
Abdel Aziz Farrag, M. Tamer Özsu: Using Semantic Knowledge of Transactions to Increase Concurrency. ACM Trans. Database Syst. 14(4): 503-525(1989) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[GM83]
Hector Garcia-Molina: Using Semantic Knowledge for Transaction Processing in Distributed Database. ACM Trans. Database Syst. 8(2): 186-213(1983) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[GMS94]
Hector Garcia-Molina, Kenneth Salem: Services for a Workflow Management System. IEEE Data Eng. Bull. 17(1): 40-44(1994) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[Her87]
Maurice Herlihy: Extending Multiversion Time-Stamping Protocols to Exploit Type Information. IEEE Trans. Computers 36(4): 443-448(1987) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[HW91]
Maurice Herlihy, William E. Weihl: Hybrid Concurrency Control for Abstract Data Types. J. Comput. Syst. Sci. 43(1): 25-61(1991) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[JM87]
Sushil Jajodia, Catherine Meadows: Mutual Consistency in Decentralized Distributed Systems. ICDE 1987: 396-404 CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[KS88]
Henry F. Korth, Gregory D. Speegle: Formal Model of Correctness Without Serializability. SIGMOD Conference 1988: 379-386 CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[KS94]
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) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[LMWF94]
...
[Lyn83]
Nancy A. Lynch: Multilevel Atomicity - A New Correctness Criterion for Database Concurrency Control. ACM Trans. Database Syst. 8(4): 484-502(1983) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[OG76]
Susan S. Owicki, David Gries: Verifying Properties of Parallel Programs: An Axiomatic Approach. Commun. ACM 19(5): 279-285(1976) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[SLJ88]
Lui Sha, John P. Lehoczky, E. Douglas Jensen: Modular Concurrency Control and Failure Recovery. IEEE Trans. Computers 37(2): 146-159(1988) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[Spi89]
...
[SSV92]
Dennis Shasha, Eric Simon, Patrick Valduriez: Simple Rational Guidance for Chopping Up Transactions. SIGMOD Conference 1992: 298-307 CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[Wei84]
...
[Wei88]
William E. Weihl: Commutativity-Based Concurrency Control for Abstract Data Types. IEEE Trans. Computers 37(12): 1488-1505(1988) CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML
[WR92]
Helmut Wächter, Andreas Reuter: The ConTract Model. Database Transaction Models for Advanced Applications 1992: 219-263 CiteSeerX Google scholar pubzone.org BibTeX bibliographical record in XML

Last update Mon Sep 17 22:00:57 2012 CET by the DBLP TeamThis material is Open Data Data released under the ODC-BY 1.0 license — See also our legal information page