A Formal Model for the Deferred Update Replication Technique.

Database replication is a technique employed to enhance both performance and availability of database systems. The Deferred Update Replication DUR technique offers strong consistency i.e. serializability and uses an optimistic concurrency control with a lazy replication strategy relying on atomic broadcast communication. Due to its good performance, DUR has been used in the construction of several database replication protocols and is often chosen as a basic technique for several extensions considering modern environments. The correctness of the DUR technique, i.e. if histories accepted by DUR are serializable, has been discussed by different authors in the literature. However, a more comprehensive discussion involving the completeness of DUR w.r.t. serializability was lacking. As a first contribution, this paper provides an operational semantics of the DUR technique which serves as foundation to reason about DUR and its derivatives. Second, using this model the correctness of DUR w.r.t. serializability is shown. Finally, we discuss the completeness of DUR w.r.t. serializability and show that for any serializable history there is an equivalent history accepted by DUR. Moreover, we show that transactions aborted by DUR could not be accepted without changing the order of already committed transactions.