## Transactional memory with data invariants

Tim Harris, Simon Peyton-Jones. Transactional memory with data invariants. March 2006. TRANSACT '06, to appear.

This paper introduces a mechanism for asserting invariants that are maintained by a program that uses atomic memory transactions. The idea is simple: a programmer writes check E where E is an expression that should be preserved by every atomic update for the remainder of the programâ€™s execution. We have extended STM Haskell to dynamically evaluate check statements atomically with the userâ€™s updates: the result is that we can identify precisely which update is the first one to break an invariant.

The STM approach is sometimes described as being "like A and I" from ACID database transactions; that is, atomic blocks provide
atomicity and isolation, but do not deal explicitly with consistency or durability. This paper attempts to include â€œCâ€ as well, by showing how to define dynamically-checked data invariants that must
hold when the system is in a consistent state.

While the basic idea is straightforward, the discussion of the design decisions in section 3.5-3.7 is an interesting exploration of the design space.

The implementation technique and operational semantics are the main contributions.

Previous draft discussed here.