Virtual Partition Algorithm in a Nested Transaction Environment and its Correctness

Abstract

In this paper, we present a formal description of the virtual partition algorithm in a nested transaction environment and prove its correctness. We model the virtual partition algorithm in a nested transaction environment using the I/O automaton model. The formal description is used to construct a complete correctness proof that is based on standard assertional techniques and on a natural correctness condition, and takes advantage of the modularity that arises from describing the algorithm as nested transactions. Our presentation and proof treat issues of data replication entirely separately from issues of concurrency control. Moreover, we have identified that the virtual partition algorithm cannot be proven correct in the sense of Goldman's work [ACM Trans. Database Syst. 19(4) (1994) 537] on Gifford's quorum consensus algorithm using the serializability theorem defined by Fekete et al. [Atomic Transactions, Morgan-Kaufmann, USA, 1994]. Thus, we have stated a weaker notion of correctness conditions, which we call the reorder serializability theorem. We have shown that not all classes of replication algorithms can be proven in the way Goldman has presented the proof of Gifford's quorum consensus algorithm. © 2001 Elsevier Science Inc.

Department(s)

Computer Science

Keywords and Phrases

Data replication; Nested transaction; Quorum consensus; Reorder serializability; Virtual partition algorithm

International Standard Serial Number (ISSN)

0020-0255

Document Type

Article - Journal

Document Version

Citation

File Type

text

Language(s)

English

Rights

© 2024 Elsevier, All rights reserved.

Publication Date

01 Sep 2001

Link to Full Text

Share

 
COinS