Formalization and Correctness of a Concurrent Linear Hash Structure Algorithm using Nested Transactions and I/O Automata

Abstract

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.

Department(s)

Computer Science

Keywords and Phrases

Client-server; I/O automaton model; Linear hash structure; Lock-coupling; Nested transaction; Serially correct

International Standard Serial Number (ISSN)

0169-023X

Document Type

Article - Journal

Document Version

Citation

File Type

text

Language(s)

English

Rights

© 2024 Elsevier, All rights reserved.

Publication Date

01 May 2001

Link to Full Text

Share

 
COinS