JISE

    In this paper, we formalize and prove the correctness of a concurrency control algorithm for an open and safe nested transaction using I/O automaton model. The model uses the notion of a recovery point subtransaction in the nested transaction tree. Our nested transaction model uses a prewrite operation before an actual write operation to increase the concurrency. It is termed “open and safe” as prewrites allow early reads (before database writes on disk) without cascading aborts. In our model we have also modeled the buffer management operations as nested transactions, and the concurrency control algorithm controls their executions. Non-access subtransactions, objects and the scheduler are modeled as I/O automata with the help of some pre and post conditions. These conditions capture the operational semantics and behavior of each automaton during the execution of transactions. While modeling we also take into account log activities, which occur during the execution of transactions. We also briefly sketch the recovery algorithm. The correctness proof shows that the concurrency control algorithm for our model is serially correct. Our proof makes use of assertional reasoning and provides many interesting invariant, thus gives a better understanding of our transaction model and the concurrency control algorithm. While proving correctness, we mapped our system to that of Moss’s two phase locking system to show the relationships between the two algorithms.