Simulation of advanced transaction models using GOLOG

Abstract

We propose a logical framework for describing, reasoning about, and simulating transaction models that relax some of the ACID (Atomicity-Consistency-Isolation-Durability) properties of classical transactions. Such extensions, usually called advanced transaction models (ATMs), have been proposed for dealing with new database applications involving long-lived, endless, and cooperative activities. Our approach appeals to non-Markovian theories, in which one may refer to past states other than the previous one. We specify an ATM as a suitable non- Markovian theory of the situation calculus, and its properties, including the relaxed ACID properties, as formulas of the same calculus. We use our framework to formalize classical and closed nested transactions. We first formulate each ATM and its properties as a theory of a certain kind and formulas of the situation calculus, respectively. We then define a legal database log as one whose actions are all possible and in which all the Commit and Rollback actions must occur whenever they are possible. After that, we show that the known properties of the ATM, including the (possibly relaxed) ACID constraints, are properties of legal logs and logical consequences of the theory corresponding to that ATM. Finally, we show how to use such a specification as a background theory for transaction programs written in the situation calculus based programming language GOLOG.