[Haskell] RE: ANNOUNCE: STM invariants and exceptions

[Simon Peyton-Jones]

Great!  Did you add to the user documentation?

Simon

| -----Original Message-----
| From: Tim Harris (RESEARCH)
| Sent: 10 October 2006 11:45
| To: haskell at haskell.org
| Cc: Simon Peyton-Jones; Simon Marlow
| Subject: ANNOUNCE: STM invariants and exceptions
| 
| Hi,
| 
| I've checked a number of changes to the transactional memory support
into GHC head:
| 
| 1. The main change is to add support for dynamically checked data
invariants of the kind described in
| http://research.microsoft.com/~tharris/papers/2006-transact.pdf.
There are two operations: "always
| X :: STM Bool -> STM ()" and "alwaysSucceeds X :: STM a -> STM ()".
Invariants are expressed as
| STM actions which must hold (i) when passed to always/alwaysSucceeds,
and (ii) at the point that
| every subsequent transaction commits.  An invariant passed to "always"
signals failure by returning
| False or by raising an exception.  An invariant passed to
"alwaysSucceeds" signals failure just by raising
| an exception.  Tests conc062 and conc063 try out some corner cases,
and the paper discusses the
| details (what if an invariant calls "retry", what if it updates TVars,
what if it loops, and so on etc...)
| 
| 2. If an atomic block contains "catch X Y" and X raises an exception
then the exception is passed to Y
| after rolling back the effects of X.  Previously we would retain the
effects of X, requiring the
| programmer to manually compensate for the portion of X that had run
before raising the exception.
| Rolling back X seems more consistent with the treatment of exceptions
that propagate out of atomic
| blocks, and the argument that transactional memory can bring
ease-of-programming benefits by
| automating the construction of compensating code for memory
operations.  The post-publication
| version of the "Composable memory transactions" paper has more details
|
http://research.microsoft.com/~tharris/papers/2005-ppopp-composable.pdf.
Test conc061 tests some
| of the corner cases.
| 
| 3. There are some bug-fixes to the implementation of "X `orElse` Y" in
which, under high contention, X
| and Y may not appear to execute against the same view of the heap.
I'm not sure if this problem has
| ever come up in practice!
| 
| We'd love to hear about it if you're using these features,
| 
| Cheers,
| 
| Tim
|