[cpp-threads] D2335 (sequential consistency proof) revision

[Boehm, Hans]

[Copied Doug explicitly, since I'd like his reaction, particularly since
it also suggests a corresponding change to JSR166.]

Re: handling of trylock in the memory model:

> From:  Lawrence Crowl
> The reasoning is that if SC is a strong goal, then we need to 
> provide the mechanisms to make it achievable.  An alternate 
> approach is to disallow this use of the trylock.
> 
Here's another possible way out of this.  I'm not 100% sure this is
correct yet, but it seems like it on first glance:

We allow trylock and timedlock to fail spuriously, even if the lock was
never held.

The cause of all the problems with trylock and timedlock are that they
see a "write" (lock) that didn't happen before it.  I think this removes
that problem, since a failed trylock can no longer be abused as a read;
it conveys no information.

For any reasonable trylock-based code I have written or can think of,
this doesn't matter.  If the trylock fails, the code either eventually
retires, or proceeds in a way that's safe without the lock.

This has no actual implementation impact, in that implementations that
never fail spuriously are fine.  The programmer is just not allowed to
rely on that behavior.  This is purely a way to characterize "bad" uses
of trylock to the programmer.

If we do this, I believe we no longer need acquire semantics for a
failed trylock.  I think that also applies to Java, which is why it
might be an attractive change there.

Would everyone be OK with this?

Hans