VERIFICATION OF CONCURRENCY CONTROL ALGORITHMS FOR DISTRIBUTED DATABASE SYSTEMS

This dissertation is concerned with effective verification of concurrency control algorithms in distributed database systems.;In order to verify the serializability of the output histories produced by a concurrency control algorithm, a computational model based on the event ordering approach is proposed. Events are identified for each algorithm and the causal relationship among those events is captured by a set of causal rules. Then a graphical structure called the causal graph is used to represent the ordering of the events. From the causal graph, the ordering of the events that are related to node and transaction processing can be represented by two subgraphs. Using the causal rules and these two subgraphs, strategies for verifying the class of output histories of an algorithm are identified for several known classes in the hierarchy. Exemplary algorithms are analyzed using the causal model to demonstrate the methodology. This causal model can also be used to verify other operational aspects of the algorithms such as deadlock possibility and reliability.;The causal model is compared to Petri-net-like model by applying both modeling techniques to one of the exemplary algorithms. It is argued that the causal model is more suitable for verifying the serializability of histories than Petri-net-like models. Finally, future research problems which may lead to better understanding of distributed concurrency control algorithms are identified.;First, the behavior of concurrent user activities in a distributed database system is modeled as a sequence of atomic accesses to the distributed database; this sequence is called the history. User atomic accesses are further grouped into transactions. Then, the notion of serializability, that a history is equivalent to the effect of a serial execution of all user transactions, is used as the correctness criterion for the histories that are generated by concurrency control algorithms. By examining the serializability of many possible histories in a distributed database system, a hierarchy of classes of serializable histories is identified. This hierarchy is proposed as the base for verifying concurrency control algorithms. The correctness of an algorithm is shown by verifying that every possible output history is in a known class.