Formalization and correctness of a concurrent linear hash structure algorithm using nested transactions and I/O automata

被引：2

作者：

Kumar Madria, Sanjay ^{[1
]}

Maheshwari, S.N. ^{[2
]}

Chandra, B. ^{[3
]}

机构：

[1] Department of Computer Science, University of Missouri-Rolla, Rolla, MO 65409-0350, United States

[2] Department of Computer Science and Engineering, Indian Institute of Technology, Hauz Khas, New Delhi, India

[3] Department of Mathematics, Indian Institute of Technology, Hauz Khas, New Delhi, India

来源：

Data and Knowledge Engineering | 2001年 / 37卷 / 02期

关键词：

Algorithms - Automata theory - Automation - Client server computer systems - Concurrency control - Data structures - Theorem proving;

D O I：

10.1016/S0169-023X(01)00005-2

中图分类号：

学科分类号：

摘要：

In this paper, we formalize and prove the correctness of a nested transaction version of the concurrency control algorithm using a linear hash structure. Nested transactions allow increased parallel execution of transactions, and handle transaction aborts in our system. We present our nested transaction model in a linear hash structure environment using a well-known I/O automaton model. We have modeled both the buckets and the transactions as I/O automata. In our algorithm, the locks have been considered at both key and vertex level. These locks have been implemented in a nested transaction environment using Moss's two phase locking algorithm and the locking protocols of the linear hash structure algorithm with a lock coupling technique. We have proved that our linear hash structure algorithm in a nested transaction environment is 'serially correct'. We have discussed briefly the client-server architecture for the implementation of our system. © 2001 Elsevier Science B.v.

引用

页码：139 / 176