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?

Titi

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.

Giotto

I might not understand your point 1; to be clear my use of TMVar was just the first example I could think of that was a simple transaction with retry (i.e. the specific interaction of takes and puts and what calls retry isn't important). What I'm really trying to get at in my first question is whether there is contention between subtransactions in different threads operating on different TVars. If that doesn't make sense I'll try to clarify after I eat something – Titi

also "nested" is the language used in the linked commentary – Titi

Oh, I see what you mean! So I understand that only one of the orElse branches will succeed; I want to know whether in A, after we've moved on from the first branch, another thread (B) can invalidate As transaction by touching a TVar which we use in the first branch – Titi

@Titi I've added some text. Hopefully I've understood your question this time. – Giotto

Thanks a lot, Daniel. On the last point I had to write a painful test program to convince myself, but that does seem to be correct. I'm still trying to wrap my head around it, but this really seems like the wrong behavior to me: what good does it do to have both the left and right branches of the orElse having the same view of the world since the alternatives are completely isolated from each other? Having the branches be individually atomic would be a much more useful property I think. As is it becomes very easy to get starvation by composing a few orElses. Thoughts? – Titi

@Titi I think the reason it's done this way is that the other kind of orElse can be programmed up just by having two threads. Have them write to a shared TVar and retry if they discover the other one wrote first. The thread that loses the race will get garbage collected. – Giotto