Commutativity-Based Locking for Nested Transactions

Abstract

A new model is introduced for reasoning about atomic transactions. This model allows careful statement of the correctness conditions to be satisfied by transaction-processing algorithms, as well as clear and concise description of such algorithms. It also serves as a framework for rigorous correctness proofs. A new algorithm is introduced for general commutativity- based locking in nested transaction systems. This algorithm and a previously- known read-update locking algorithm are presented and proved correct using the new model. The proofs are based on Serializability Theorem and a new dynamic atomicity condition for data objects. Keywords: Data loses, Input output automata.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1988
Accession Number
ADA200980

Entities

People

  • Alan Fekete
  • Bill Weihl
  • Michael Merritt
  • Nancy Lynch

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Energy and Power Technologies
  • Human Systems
  • Weapons Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Automata
  • Boundaries
  • Classification
  • Computer Programming
  • Construction
  • Control Systems
  • Database Management Systems
  • Databases
  • Decomposition
  • Failure Mode And Effect Analysis
  • Information Processing
  • Information Systems
  • Language
  • Military Research
  • Programming Languages
  • User Interface

Fields of Study

  • Computer science

Readers

  • Database Systems and Applications
  • Mathematical Modeling and Probability Theory.