## 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.

## Comment viewing options

### Comments?

I am not sure I like the fact that people stop commenting on papers that come up for discussion...

### Don't panic

The paper is great, but I believe most of the people who care already commented on its draft appearance.

It would be good, though, if somebody could summarize the changes since that draft.

### True, my message was a

True, my message was a general rebuke, not specific to this paper...