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, ...