[cpp-threads] sequential consistency for race-free programs

[Peter Dimov]

Boehm, Hans wrote:
> I'm trying to make another pass over the strawman proposal.  Thinking
> about this, I think I've ended up with somewhat contradictory goals.
> My wish-list:
>
> 1) Data-race-free programs (based on the sequentially-consistent
> interpretation) have sequentially consistent semantics, at least if
> they use "ordinary" synchronization primitives. [...]

> Now reconsider Bill's example:
>
>>> Initially x = y = 0
>>>
>>> Thread 1:
>>> r1 = x
>>> if (r1) y = 1
>>>
>>> Thread 2:
>>> r2 = y
>>> if (r2) x = 1

Why is it important to make the example above well-defined? Even with 
important-sounding variable names as "launch_all_missiles", it still seems 
terribly contrived to me.

The "data-race-free" rule, as taught to programmers, is simple: an ordinary 
variable that is shared between threads shall never be accessed without a 
lock. This example violates the rule. Why should it be defined? Is it even 
possible for a non-expert to write correct data-race-free code that doesn't 
adhere to the rule? I'm inclined to answer "no".