The orElse function obeys useful laws: it is associative and
has unit retry:
M1 ‘orElse‘ (M2 ‘orElse‘ M3)
= (M1 ‘orElse‘ M2) ‘orElse‘ M3
retry ‘orElse‘ M = M
M ‘orElse‘ retry = M
Haskell aficionados will recognize that STM may thus be an
instance of MonadPlus.
3. 5. exceptions
The STM monad supports exceptions just like the IO monad,
and in much the same way as (say) C#. Two new primitive functions, catch and throw, are required; their types are given in
Figure 1. The question is: how should transactions and exceptions interact? For example, what should this transaction do?
atomic (do
{ n <- readTVar v_n
; lim <- readTVar v_lim
; writeTVar v_n (n + 1)
; if n > lim
then throw
(AssertionFailed ”Urk”)
else if (n == lim) then retry
else return ()
; ... write data into buffer...})
The programmer throws an exception if n > lim, in which
case the. . .write data. . . part will clearly not take place. But
what about the write to v_n from before the exception was
thrown?
Concurrent Haskell encourages programmers to use exceptions for signalling error conditions, rather than for normal control flow. Built-in exceptions, such as divide-by-zero,
also fall into this category. For consistency, then, in the above
program we do not want the programmer to have to take account of the possibility of exceptions, when reasoning that
if v_n is (observably) written then data is written into the
buffer. We, therefore, specify that exceptions have abort semantics: if an atomic transaction throws an exception, then
the transaction must be validated as if it had completed
normally; however, no changes are committed. If validation
succeeds, then the exception is propagated; but if validation fails, then the throwing of the exception may have been
based on an inconsistent view of memory, so the exception
is discarded and the transaction is re-executed from scratch.
Abort semantics make it much easier to reason about invariants: the programmer only has to worry about the invariant
being preserved when the transaction commits; exceptions
raised during the transaction always restore the invariant, by
definition.
Our use of exceptions to abort atomic blocks is a free design choice. In other languages, especially in ones where exceptions are used more frequently, it might be appropriate
to distinguish exceptions that cause the enclosing atomic
block to abort from exceptions that allow it to commit before they are propagated.
Notice the difference between calling throw and calling
retry. The former signals an error, and aborts the transaction; the latter only indicates that the transaction is not yet
ready to run, and causes it to be re-executed when the situation changes.
An exception can carry a value out of the STM world. For
example, consider
atomic (do
{ s <- readTVar svar
; writeTVar svar ”Wuggle”
; is length s < 10 then
throw (AssertionFailed s)
else . . .})
Here, the external world gets to see the exception value holding the string s that was read out of the TVar. However, since
the transaction is aborted before the exception propagates,
its write to svar is not externally observable. One might
argue that it is wrong to allow even reads to “leak” from an
aborted transaction, but we do not agree. The values carried
by an exception can only represent a consistent view of the
heap (or validation would fail, and the transaction would
re-execute without propagating the exception), and it is almost impossible to debug an error condition that only says
“something bad happened” while deliberately discarding
all clues to what the bad thing was. The basic transactional
guarantees are not threatened.
What if the exception carries a TVar allocated in the
aborted transaction? A dangling pointer would be unpleasant. To avoid this we refine the semantics of exceptions to
say that a transaction that throws an exception is aborted
so far as its write effects are concerned, but its allocation effects are retained; after all, they are thread-local. As a result,
the TVar is visible after the transaction, in the state it had
when it was allocated. Cases like these are tricky, which is
why we developed a full formal semantics. 9
Concurrent Haskell also provides asynchronous
exceptions which can be thrown into a thread as a signal—
typical examples are error conditions like stack overflow,
or when a master thread wishes to shut down a helper. If
a thread is in the midst of an STM transaction, then the
transaction log can be discarded without externally visible
effects.
What if an exception is raised inside orElse? We considered a design in which, if the first alternative throws an
exception, we could discard its effects and try the second
alternative instead. But that would invalidate the beautiful
identify which makes retry a unit for orElse and would
also make orElse asymmetric in its treatment of exceptions (discarded from the first alternative but propagated by
the second). We, therefore, chose that exceptions do propagate from the first alternative: the second alternative is examined only if the first one calls a retry.
What about catching an exception within an atomic
block? Consider this example: