Home

Transactional Memory with data invariants (draft sequel to the STM-Haskell paper)

Transactional memory with data invariants
From the abstract:
This paper introduces a mechanism for asserting invariants that are maintained by a program that uses atomic memory transactions.
The idea is simple: the programmer write always 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 check always 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.
This seems connected to Typed Contracts for Functional Programming by Ralf Hinze, Johan Jeuring, and Andres Löh (noticed on the blog of Dominic Fox).
Maybe this year design-by-contract is the hot subject?

I haven't gotten far enough into either of these papers to have much opinion, but the motivational paragraph at the beginning of the Typed Functional Contracts paper grabbed my attention instantly, and I know I want more STM in my applications, so I look forward to a few enjoyable hours.
By shapr at 2006-03-30 11:04 | Functional | Implementation | Parallel/Distributed | Software Engineering | Theory | other blogs | 40081 reads

Comment viewing options

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

I know I want more STM in my applications

I know I want more STM in my applications

Amen!

Incidentally, it seems that the Azul Systems (the people who are putting tens of cores on one piece of silicon) Java accelerator thingy uses some form of transactional memory to manage the concurrency, but they call it "Optimistic Thread Concurrency".

See: Azul Systems

By genneth at Thu, 2006-03-30 12:46 | login or register to post comments

Chronology

I certainly find this line of research very interesting indeed, though I'm having a bit of time keeping on top of which achievements are to be attributed to which papers. How does this relate to Harris, Marlow, Herlihy & Peyton Jones' Composable memory transactions, which is the one paper I have read carefully? From section 2 it looks like this allows further invariants to be layered upon CMT's system in an orthoganol manner.

In that paper (ie. CMT) there is a claim that Hindley-Milner type inference is important to the results achived there, which, if true, would be an argument against implementing certain kinds of software systems in a dynamically typed language. Does that claim hold up? Has anyone tried to reimplement these ideas in a dynamically typed language?

By Charles Stewart at Thu, 2006-03-30 15:51 | login or register to post comments

This paper comes after CMT

This paper comes after CMT and builds directly on it. It adds a single construct to the CMT design.

On the issue of Hindley-Milner's importance I would say that types in general play an important role in the CMT paper. The type system is used to ensure that all software memory transactions are otherwise (apart from modifying transactional variables) side-effect free. That way you can easily roll back any transaction which shouldn't be commited. If you want to implement this in a dynamically typed language I suppose you would have to create a sandbox whenever you start an atomic transaction. Any operation which cannot be rolled back would yield an error in the sandbox.

By Josef Svenningsson at Thu, 2006-03-30 17:26 | login or register to post comments

Leaving side-effects at the programmer's whim

Or else the language could end up leaving it completely up to the programmer to decide whether or not the transactional code contains side-effects. Welcome to STM in C. Whoopie.

Is trading "you're using locks: didn't anybody ever teach you how to program without race conditions?!!" for "you're using STM: didn't anybody ever teach you how to program without side-effects?!!" the sad future for users of languages whose designers consider typing or sandboxes to be suboptimal?

By michael-fig at Sat, 2006-04-01 01:07 | login or register to post comments

Yes

Because language designers who consider typing or sandboxes to be suboptimal are wrong when "optimal" includes implementing concurrency without deadlock or race conditions.

By Paul Snively at Sat, 2006-04-01 03:23 | login or register to post comments

Heroic efforts in C

Looking at the stretch that the Gnome people are putting C to, I wouldn't think they'd mind a bit of simple remember-to-be-side-effect-free. I'm not sure if it's an April fools joke. I know I was mostly kidding when I figured out how to do continuations in C...

By genneth at Sat, 2006-04-01 12:49 | login or register to post comments

Moved

The paper seems to have moved now to here: http://research.microsoft.com/~tharris/papers/2006-transact.pdf.

By Neil Madden at Wed, 2006-05-17 12:42 | login or register to post comments