Formalization and Proof of Correctness of the Crash Recovery Algorithm for an Open and Safe Nested Transaction Model
Abstract
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.
Recommended Citation
S. K. Madria et al., "Formalization and Proof of Correctness of the Crash Recovery Algorithm for an Open and Safe Nested Transaction Model," International Journal of Cooperative Information Systems, vol. 10, no. 1 thru 2, pp. 1 - 50, World Scientific Publishing, Jan 2001.
The definitive version is available at https://doi.org/10.1142/s0218843001000242
Department(s)
Computer Science
International Standard Serial Number (ISSN)
0218-8430
Document Type
Article - Journal
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 2024 World Scientific Publishing, All rights reserved.
Publication Date
01 Jan 2001