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

Select your preferred way to display the comments and click "Save settings" to activate your changes.

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