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

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

Last update Mon Sep 17 22:00:57 2012 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page