Previous [1] [2] [3] [4] [5] [6] [7] [8] [9] [10]

@

Journal of Information Science and Engineering, Vol.19 No.2, pp.267-282 (March 2003)


A Concurrency Control Algorithm for an Open and Safe Nested Transaction Model: Formalization and Correctness

Sanjay Kumar Madria, S. N. Maheshwari* and B. Chandra+
Department of Computer Science
Universityof Missouri-Rolla
Rolla, MO 65401, U.S.A.
E-mail: madrias@umr.edu
*Department of Computer Science
Indian Institute of Technology, Hauz Khas
New Delhi 110021, India
E-mail: snm@cse.iitd.ernet.in
+Department of Mathematics
Indian Institute of Technology, Hauz Khas
New Delhi 110021, India
E-mail: bchandra@maths.iitd.ernet

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 Mosss two phase locking system to show the relationships between the two algorithms.

Keywords: nested transactions, I/O automaton model, recovery, concurrency, two phase locking

Full Text () Retrieve PDF document (200303_06.pdf)

Received July 2, 2001; revised May 21, 2002; accepted July 11, 2002.
Communicated by Ming-Syan Chen.