An Equational Theory for Transactions

Transactions are commonly described as being ACID: All-or-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 derive the induction rule for Consistency.

Published in:
Proceedings of Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2003)
LNCS 2914. Extended version in Technical Report IC/2003/26.

Note: The status of this file is: Anyone

 Record created 2006-01-24, last modified 2020-04-20

Download fulltext

Rate this document:

Rate this document:
(Not yet reviewed)