Data Replication in Nested Transaction Systems.

Abstract

Gifford's basic Quorum Consensus algorithm for data replication is generalized to accommodate nested transactions and transaction failures (aborts). A formal description of the generalized algorithm is presented using the new Lynch-Merritt input-output automaton model for nested transaction systems. This formal description is used to construct a complete (yet simple) proof of correctness that uses standard assertional techniques and is based on a natural correctness condition. Nondeterminism is used in the algorithm description to yield a correctness proof that is independent of any particular programming language or implementation. The presentation and proof treat issues of data replication entirely separately from issues of concurrency control and recovery.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1987
Accession Number
ADA182178

Entities

People

  • Kenneth J. Goldman

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Algorithms
  • Availability
  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Consensus Algorithms
  • Contracts
  • Control Systems
  • Control Theory
  • Data Management
  • Distributed Computing
  • Information Processing
  • Language
  • Military Research
  • Programming Languages
  • Standards

Fields of Study

  • Computer science

Readers

  • Economics
  • Mathematical Modeling and Probability Theory.