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

[Doug Lea]

Sorry for the slow-motion replies. Swamped.

Boehm, Hans wrote:
>> 
>> It does seem a little crazy though to prohibit an 
>> implementation of tryLock from guaranteeing lack of spurious failure.
> Perhaps my mind has been warped by trying to generate proofs of SC
> behavior.  But it no longer seems weird to me at all.  The fundamental
> problem is that a failed trylock (and a strong CAS) is fundamentally a
> load operation, since it gives you an indication of the value it saw.
> Thus without spurious failure, and with no ordering on failure, you are
> effectively providing an unordered load operation, which can't be SC.

> You are reading the value of a write that did not necessarily
> happen-before the read.  No synchronization operations shopuld do that.
> 

A failed tryLock might act as an acquire only wrt some aspect of
lock-state that is unrelated to anything
user-visible. So in that sense a failed tryLock cannot be
guaranteed to be a "synchronization operation" at all.

I still like this way of explaining it, but ...

> 
> For lock, I think what I'm proposing is not all that different from what
> you suggest.  I'd have the trylock specification allow spurious failure,
> with a nonbinding note in the standard recommending that implementors
> aggressively minimize or eliminate the cases in which it can occur.  I
> don't know of any otherwise useful code that would fail as a result of a
> spurious trylock failure.  But lots of code may perform very
> suboptimally if this were to occur regularly.
> 

... I do think this is OK. I don't think there's any
difference between it and our (Java) approach of keeping failure
conditions opaque (at top level anyway) and saying that failed
tryLocks are not synchronization operations.

It's reminiscent of the options for spec'ing
spurious wakeups for monitor waits. (Although I think
the main moral of that one is that people will complain
for decades about allowing them at all, so maybe it
is not worth the agony :-)

-Doug