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