In this paper, we present, formalize and prove the correctness of recovery algorithm for our open and safe nested transaction model using I/O automaton model. Our nested transaction model uses the notion of a recovery point subtransaction in the nested transaction tree. It introduces a prewrite operation before each write operation to increase the potential concurrency. Our transaction model is termed as "open and safe" as prewrites allow early reads (before database writes on disk) without cascading aborts. The systems restart and buffer management operations are modelled as nested transactions to exploit possible concurrency during restart. Each non-access transaction, object, and the scheduler is modeled as I/O automaton. Each of these automata is specified with the help of some pre-and post-conditions. These pre-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 gives a better understanding of our recovery algorithm.
Assertional Reasoning for Concurrent and Communicating BPEL-like Programs
