Virtual partition algorithm in a nested transaction environment and its correctness

In this paper, we present a formal description of the virtual partition alg orithm in a nested transaction environment and prove its correctness. We mo del the virtual partition algorithm in a nested transaction environment usi ng the I/O automaton model. The formal description is used to construct a c omplete correctness proof that is based on standard assertional techniques and on a natural correctness condition, and takes advantage of the modulari ty that arises from describing the algorithm as nested transactions. Our pr esentation and proof treat issues of data replication entirely separately f rom issues of concurrency control. Moreover, we have identified that the vi rtual 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 con sensus 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 serializ ability theorem. We have shown that not all classes of replication algorith ms can be proven in the way Goldman has presented the proof of Gifford's qu orum consensus algorithm. (C) 2001 Elsevier Science Inc. All rights reserve d.