@jonmsterling What do you mean by powerdomain semantics?
Then I'm curious which departure from that you think makes that model an oversimplification: more lax memory models, fairness constraints on the scheduler, something else I'm not thinking of, or some combination?
@robryk Indeed, the issue is that sequential consistency is not a realistic constraint. Since the 1980s, there has been a discussion of “true concurrency” in the community that aims to reduce the idea of two things happening at the same time to causality — in particular, events are partially ordered by a causality relation, and two compatible events that are not causally related to each other are considered to be concurrent. This story also involves nondeterminism, but this is *on top* of the concurrency — in particular, a single execution of the program involves some things happening concurrently, but branching causes there to be many possible (non-deterministic) concurrent executions. So in the 'true concurrency' story, nondeterminism explains branching rather than concurrency.
Do you mean explicit branches in code when you say branching? If so, I'm somewhat confused: I can get nondeterministic behaviour from a concurrent system with no explicit branches (example: thread A does write(false to x); write(true to x); thread B does return read(x);).
(I agree that interleaving of operations is not a correct way to describe an execution of a concurrent program and that (even though for many memory models one can use a linear order on something other than operations) a partial order where each thread is totally ordered and which satisfies some other memory-model-specific requirements is both a correct and natural representation of an execution.)
@robryk When I say “branching” I mean not only explicit program branching, but also the implicit one — when you read(x), this introduces branches for all possible values of x.
But yes, I agree with your example and other comments.
@robryk Nondeterminism is usually interpreted in the "powerdomain monad" -- where the effect allows you to flip a coin, basically.
People used to use this to interpret concurrency, by nondeterministically interleaving all the effects performed by different threads.