Using Formal Methods to Reason about Semantics-Based Decompositions of Transactions
Paul Ammann, Sushil Jajodia, Indrakshi Ray · 1995
Many researchers have investigated the process of decomposing transactions into smaller pieces to increase concurrency. The focus of the research is typically on implementing a decomposition supplied by the database application developer, with relatively little attention to what constitutes a desirable decomposition and how the developer should obtain such a decomposition. In this paper, we argue that the decomposition process itself is worthy of attention. A decomposition generates a set of proof obligations that must be satisfied to show that a particular decomposition correctly models the original collection of transactions. We introduce the notion of semantic histories to formulate and prove the necessary properties. Since the decomposition impacts not only the atomicity of transactions, but isolation and consistency properties as well, we present a technique based on formal methods that allows these properties to be surrendered in a carefully controlled manner.