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

[Peter Dimov]

Boehm, Hans wrote:
> The real question here is what it means to be "shared between
> threads". Clearly people (including ordinary programmers to the
> extent they deal with threads at all) routinely to the following:
>
> 1. initialize data structure S
> 2. Fork threads
> 3. Read S in multiple threads without locking
>
> I would argue that it's unreasonable to outlaw this in a coding
> standard.  It's pervasive, and it's exactly what you want people
> to do.

Of course not. Immutable data is obviously safe.

> Thread 1:
> while (!self_destruct_left);
> self_destruct_right = true;
> blow_up_port_side_of_ship();
>
> Thread 2:
> while (!self_destruct_right);
> self_destruct_left = true;
> blow_up_starboard_side_of_ship();

[...]

> If we use atomics instead, with unordered semantics, I think the
> ship is allowed to blow up immediately, under all proposals.  That's
> slightly weird, I think.

Right, because we explicitly granted the compiler and the hardware freedom 
to reorder the load and the store. Presumably we had our reasons for that. 
:-) (In practice the hardware will probably insert an implicit hoist-store 
barrier after the conditional branch and the compiler won't reorder the 
atomics. But in theory they could.)

> If we use acquire loads for the loop tests, I think nothing is
> precluded, and the ship is still allowed to blow up immediately.
> (I assume that acquire loads can be paired with ordinary stores.)
> There is no happens-before cycle.  I'm not sure whether that's
> worse than the preceding example or not.

I see a happens-before cycle here. The load from self_destruct_left (sdl) 
happens after the store to self_destruct_left because it sees the stored 
value of 'true'. The store to sdr happens after the load from sdl because an 
'acquire' constraint is hoist-load+hoist-store, and the hoist-store part 
imposes ordering.

A similar happens-before cycle occurs with unordered loads and release (or 
just sink-load) stores, or with intervening #loadStores.

Anyway. Your example is interesting, but it doesn't answer my question: why 
is SC for SC-race-free worth the significantly increased complexity of the 
specification? Why can't we just get away with declaring "intent", as you 
believe Posix does, without actually expressing this intent in a formal way? 
Everyone will still be free to implement "the spirit" for the cases that 
matter, they just won't be prohibited from not supporting it and sticking to 
the letter. (And my guess is that anyone not willing to support "the spirit" 
won't support it fully even if it's codified into the letter.)

Of course since you're going to do the actual work, it is your judgment 
about the cost/benefit that matters and not mine. I'm just curious. :-)