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.

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

Link to Full Text

Share

 
COinS