Validation in STM transactions nested with orElse

Question

This commentary page describes a lot of the fine details of STM in GHC, but I'd like clarity on a couple points.

First, is a nested transaction invalidated when variables accessed in the parent change?

For instance we have in thread A:

takeTMVar a `orElse` takeTMVar b `orElse` takeTMVar c

Say that while A is executing the nested transaction takeTMVar b, another thread B does a putTMVar a (); can thread A successfully complete its nested transaction, or is it invalidated (this would strike me as wrong)?

A second point which I think I understand but wouldn't mind reassurance on: in the case where the entire top-level transaction described above for A is retried and finally blocks, is it correct that A will be awoken when any of a, b, or c change?

Finally as a bonus, do the semantics of the transaction above change if we (or library authors) change orElse to infixr?

Answer 1

I don't think "nested" is the right term to describe this. These are three alternate transactions; none is nested within another. In particular, exactly one of the three is going to happen and be committed -- but which one happens is not deterministic. This one sentence should be enough to answer all three questions, but just to be sure, let's carefully say for each:

1. There's no guarantee. Maybe takeTMVar b will complete and commit; or maybe it will be pre-empted and takeTMVar a will be woken up and complete. But they won't both complete, that's for sure.

2. Yes, that's correct: all three TMVars can wake this thread up.

3. The semantics don't change: whenever several of them can commit, the left-most one will. (In particular, the paper describing STM says, "The orElse function obeys useful laws: it is associative and has unit retry.".)

4. (from your question in the comments) The semantics of STM on page 8 of the linked paper really does guarantee that the left-most successful transaction is the one that succeeds. So: if thread A is executing takeTMVar b (but has not yet committed) and thread B executes and commits a write to a, and nothing else happens afterwards, you can be sure that thread A will be restarted and return the newly written value from a. The "nothing else happens afterwards" part is important: the semantics makes a promise about what happens, but not about how the implementation achieves it; so if, say, another thread took from a immediately (so that the takeTMvar a is still going to retry), a sufficiently clever implementation is allowed to notice this and not restart thread A from the beginning of the transaction.