APPLYING FORMAL METHODS TO SEMANTIC-BASED DECOMPOSITION OF TRANSACTIONS

In some database applications the traditional approach of serializabil ity, in which transactions appear to execute atomically and in isolati on on a consistent database state, fails to satisfy performance requir ements. Although many researchers have investigated the process of dec omposing transactions into steps to increase concurrency, such researc h typically focuses on providing algorithms necessary to implement a d ecomposition supplied by the database application developer and pays r elatively little attention to what constitutes a desirable decompositi on or how the developer should obtain one. We focus on the decompositi on itself. A decomposition generates proof obligations whose discharge ensures desirable properties with respect to the original collection of transactions. We introduce the notion of semantic histories to form ulate and prove the necessary properties, and the notion of successor sets to describe efficiently the correct interleavings of steps. The s uccessor set constraints use information about conflicts between steps so as to take full advantage of conflict serializability at the level of steps. We propose a mechanism based on two-phase locking to genera te correct stepwise serializable histories.