[10ren]

I believe race conditions can still occur in pure message-passing languages, like Erlang (Joe Armstrong says so in Programming Erlang, p.173). This doesn't get much press, perhaps because it's much easier to get right than shared-memory, and because not that many people are actually doing it yet.

Does Spin address this issue?

[tophercyll]

You can build message passing code that suffers from race conditions. In practice, though, it's almost always obvious if you're about to do something dangerous.

On p.173 Joe writes:

  When we say things such as this:
    Pid = register(...),
    on_exit(Pid, fun(X) -> ..),
  there is a possibility the process dies in the gap between these two statements.

Regarding process death, we allow multiple inter-process relationships to be specified at spawn time. Hence any number of processes may be configured to observe a newly-spawned process before it has even started. Additionally, all children are linked to (die with) their parent, which both eliminates the risk of orphaned processes and has other benefits.

So in Spin you wouldn't be tempted to write something like above (probably not Erlang either?).