An Equational Theory for Transactions

Abstract. Transactions are commonly described as being ACID: Allor-nothing, Consistent, Isolated and Durable. However, although these words convey a powerful intuition, the ACID properties have never been given a precise semantics in a way that disentangles each property from the others. Among the benefits of such a semantics would be the ability to trade-off the value of a property against the cost of its implementation. This paper gives a sound equational semantics for the transaction properties. We define three categories of actions, A-actions, I-actions and D-actions, while we view Consistency as an induction rule that enables us to derive system-wide consistency from local consistency. The three kinds of action can be nested, leading to different forms of transactions, each with a well-defined semantics. Conventional transactions are then simply obtained as ADI-actions. From the equational semantics we develop a formal proof principle for transactional programs, from which we...

• Type: Conference
• Year: 2003
• Where: FSTTCS
• Authors: Andrew P. Black, Vincent Cremet, Rachid Guerraoui, Martin Odersky
• Keywords: Equational Semantics, FSTTCS 2003, Semantics, Sound Equational Semantics