Nancy Lynch, Michael Merritt, William Weihl, and Alan Fekete. Atomic Transactions. Morgan Kaufmann Publishers, 1994. Table of Contents (postscript) To order, please contact Morgan Kaufmann Publishers.
This book contains a description of just about all of the standard concurrency control and abort recovery algorithms for databases, together with specifications of their required behavior and complete correctness proofs. The setting includes nested transactions and arbitrary data types. Everything is done formally, in terms of I/O automata.