To ensure correctness, most transaction processing systems execute at the SERIALIZABLE isolation level, and hence each transaction retains its read and write locks until it completes, These long term locks significantly reduce the number of transactions that can be executing concurrently and hence the throughput.
Art Bernstein and I, together with Wai-Hong Leung and David Gerstl, have been pursuing an approach in which we divide each transaction into steps and release all read and write locks between steps, thus increasing the throughput. Since the interleaved execution of steps from different transactions might lead to incorrect executions, we have proposed a new correctness criterion, weaker than serializability, that guarantees only that each transaction satisfy sits specification. Based on this correctness criterion, we analyze each transaction at design time to determine those interleavings that can lead to incorrect executions. Then we use a new type of concurrency control, an assertional concurrency control, to schedule the execution of steps and ensure that only correct executions take place.
To evaluate our approach, we first implemented the assertional concurrency control within the Ingres database management system. Then we made throughput measurements using the TPC-C Benchmark Transactions, a commonly used set of transaction benchmarks. We found that the assertional concurrency control achieved up to an 80\% increase in transaction throughput, particularly in applications with database hotspots and long running transactions
Now we plan to extend these ideas in a number of directions, including performing transactions on the Web.
The Concurrency Factory is a computer aided software engineering tool for designing concurrent systems. The Factory was developed as a collaborative project between Stony Brook and the University of North Carolina. Scott Smolka and I have been the Stony Brook PIs. A number of students have contributed.
The basic idea of the factory is to model a concurrent system as a network of communicating finite state machines. These machines can be drawn graphically and then simulated. The most novel part of the system is model checking, whereby the designer can use a formal language to express some property s/he would like the concurrent system to have, and the model checker part of the factory checks whether the system has that property.
I am particularly interested in two problems: