A proof technique for concurrency control and recovery algorithms for replicated databases (Q1097027)

A replicated database is a distributed database in which copies of some data items are stored redundantly at multiple sites. In such a system, an execution of transactions is correct if it is equivalent to a serial execution of those transactions on a one-copy database. It is shown that if transactions see failures and recoveries in a consistent order then the execution is one-copy serializable. The algorithm for available copies creation that uses failure-recovery serialization graph is introduced and proved. The value of failure-recovery serialization graph is demonstrated by its use in proof of correctness of an algorithm for synchronizing access to a replicated database.