Commutativity-based locking for nested transactions (Q753480)

The authors present a new model for describing and reasoning about transaction-processing algorithms (TPA). The main contributions of this approach are: handling of nested transactions (NT), integration of concurrency control (CC) and recovery algorithms. The authors provide an explicit operational model for transactions and for other components of a system; more events are included in this model than in the ``classical'' work (separate events are considered for: the request by a transaction to perform an access to an object; the invocation of the access at the object; the completion of the access at the object; the decision by the system that the access is to be committed rather than aborted; the report to the transaction of the results of the access); many properties become easy to express, at the natural cost of some complexity of such a detailed model. The first major contribution is a comprehensive model for NT systems. Rigorous proofs of a wide variety of TPA become possible in this uniform framework. Most previous approaches to CC are generalized to encompass NT and type-specific CC algorithms. The other important contribution is a new CC and recovery algorithm for abstract data types in an NT system; it generalizes a previous algorithm developed by Weihl. Commutativity properties of operations are used to achieve high level of concurrency (concurrency is further increased by using the results of operations, in addition to their names and arguments, in checking for conflicts). An important theorem (analogous to th ``absence of cycles'' condition), stating a general sufficient condition for a TPA to be correct, is given. An interesting condition on individual objects, called dynamic atomicity (DA), is defined; the useful property is that as long as all objects in the system are dynamic atomic, transactions will appear atomic. Since the algorithm presented by the authors, when applied to a single object, ensures DA, it can be used at some objects of the system, and other algorithms at other objects (the system structure considered consists of many objects, with CC and recovery performed independently at each object). \(Moss'\) read-update locking algorithm for NT is proved to ensure DA (most popular variations of two-phase locking also do so). The sections of the paper present successively: NT, related work; the general model (input-output automata - which constitute the formal foundation of the work; correctness of an NT system; the serializability theorem); the new algorithm and \(Moss'\) algorithm (DA; properties of operations - commutativity; correctness of the two algorithms).