[Haskell] ANNOUNCE: STM invariants and exceptions
Tim Harris (RESEARCH)
tharris at microsoft.com
Tue Oct 10 06:44:43 EDT 2006
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
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
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,
More information about the Haskell