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

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: