Accession Number : ADA182178

Title :   Data Replication in Nested Transaction Systems.

Descriptive Note : Technical rept.,

Corporate Author : MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE

Personal Author(s) : Goldman,Kenneth J

PDF Url : ADA182178

Report Date : May 1987

Pagination or Media Count : 79

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.

Descriptors :   *ALGORITHMS, *INPUT OUTPUT MODELS, PROGRAMMING LANGUAGES, THESES, DISTRIBUTED DATA PROCESSING, DATA BASES

Subject Categories : Computer Systems

Distribution Statement : APPROVED FOR PUBLIC RELEASE