Database Concurrency Control

We have completed an extensive case study in the area of concurrency control and recovery for databases. This project produced a long series of papers . These describe formally just about all of the standard concurrency control and abort recovery algorithms for databases, and provide 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 the I/O automaton model. Nearly all of the results of these papers are summarized in the book . This work provides a mathematical theory that allows careful reasoning about concurrency control and abort recovery algorithms. The theory contains a good deal of modularity -- it breaks down the system descriptions and the proofs into manageable, reusable pieces. It distills the essential information from hundreds of research papers arising in the dataase systems community, removing the system-dependent details and only presenting what it essential for the algorithms to work correctly. The algorithms and specifications can serve as guidelines for designers of database systems, and as an economical means for more mathematically-inclined readers to learn the key ideas behind such systems. One aspect of practical concurrent database systems that is not included in our treatment is the possibility of processor crashes that lose information. Partial treatments of this topic, in styles compatible with our work, appear in papers by Kuo and Fekete and Kuo, and in the notes for the MIT graduate course on [Principles of Computer Systems].

TOC / LCS / MIT Last modified: Fri Nov 7 01:33:02 1997	Comments?