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

In this paper, we formalize and prove the correctness of a nested transacti on version of the concurrency control algorithm using a linear hash structu re. Nested transactions allow increased parallel execution of transactions, and handle transaction aborts in our system. We present our nested transac tion model in a linear hash structure environment using a well-known I/O au tomaton 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 en vironment using Moss's two phase locking algorithm and the locking protocol s of the linear hash structure algorithm with a lock coupling technique. We have proved that our linear hash structure algorithm in a nested transacti on environment is 'serially correct'. We have discussed briefly the client- server architecture for the implementation of our system. (C) 2001 Elsevier Science B.V. All rights reserved.