Formalization and proof of correctness of the crash recovery algorithm foran open and safe nested transaction model

In this paper, we present, formalize and prove the correctness of recovery algorithm for our open and safe nested transaction model using I/O automato n model. Our nested transaction model uses the notion of a recovery point s ubtransaction in the nested transaction tree. It introduces a prewrite oper ation before each write operation to increase the potential concurrency. Ou r transaction model is termed as "open and safe" as prewrites allow early r eads (before database writes on disk) without cascading aborts. The systems restart and buffer management operations are modelled as nested transactio ns to exploit possible concurrency during restart. Each non-access transact ion, object, and the scheduler is modeled as I/O automaton. Each of these a utomata is specified with the help of some pre-and post-conditions. These p re- and post-conditions capture the operational semantics and the behavior of each automaton during recovery operations. Our proof technique makes use of assertional reasoning and provide many interesting invariant, thus give s a better understanding of our recovery algorithm.