Home

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.

By Ehud Lamm at 2006-05-24 07:48 | Functional | Parallel/Distributed | other blogs | 4983 reads

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

By Ehud Lamm at Thu, 2006-05-25 07:25 | login or register to post comments

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.

By Andris Birkmanis at Thu, 2006-05-25 08:52 | login or register to post comments

True, my message was a

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

By Ehud Lamm at Thu, 2006-05-25 10:26 | login or register to post comments

Changes...

They seem to have removed the wrapper always :: STM Bool -> STM () around check :: STM a -> STM () and instead make use of assert in the examples of section three. All of the example code now uses semicolons in do{} blocks. There is another, problematic, example demonstrating invariants between state pairs (e.g: requiring that a TVar be non-decreasing).

The list of design choices has been reworded (always, True, etc. are gone) and there is an extended discussion of restricting the side effects of invariants (using phantom types ReadOnly and Full to distinguish restricted and unrestricted STM actions).

A new section (6) discusses predicates over state pairs as introduced in the new example of section 3.3. This discusses two approaches to allowing STM actions to access the state before the transaction being checked began: readTVarOld :: TVar a -> STM a and old :: STM a -> STM a. The former requires that special functions be written specially for invariant checking where the latter takes any old action and runs it with the state from before the current transaction started. The same problems with unrestricted invariants occur here so the phantom types solution comes up again: old :: STM ReadOnly a -> STM e a.

The conclusion has some new comments which may be of interest including a brief discussion of making a distinction similar to that between assertions (for detecting bugs) and triggers (which are part of the programme logic) in databases and the suggestion that some properties not expressible by the current system (those relating more than two states) could be supported by allowing invariants to add new invariants though it hasn't been implemented as it's an open question as to whether or not it'll be useful.

That's all I spotted (though I didn't look at the semantics and implementation sections too hard) and seems to be the bulk of the changes.

By Thomas Sutton at Thu, 2006-05-25 12:01 | login or register to post comments