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

[Boehm, Hans]

> From:  Doug Lea
> Sent: Monday, August 27, 2007 5:28 PM
> To: C++ threads standardisation
> Cc: Howard Hinnant
> Subject: Re: [cpp-threads] D2335 (sequential consistency 
> proof) revision
> 
> Hans Boehm wrote:
> > 
> > 
> > I claim that there is no way to get r2 = failure and r3 = 0 
> on an SC 
> > execution.  The first statement of thread 2 would have to 
> follow the 
> > last statement of thread 1, and that disallows r3 = 0.
> > 
> 
> Thanks, now I see what you are getting at.
> 
> Another way of saying this is that tryLock has no SC interpretation.
> Or at least no natural one. I did a quick scan through some 
> of the literature on this to check if anyone has ever 
> remarked on this before and didn't see anything. (This didn't 
> arise in JSR133 because Java has no native tryLock. And the 
> Java.util.concurrent Locks don't specifically promise SC.)
This is very similar to the example form my PPoPP paper that uses
ordinary variables instead of volatiles/atomics.  Which is related to
Sarita's DRF(0) vs. DRF(1) distinction.  And I discussed the Java
implications of that with Jeremy.  (There aren't really any because of
the different definition of "race".)  The part that I think both of us
missed is that the issue persists if you use volatiles, with no ordering
on failure for trylock.
> 
> 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.

The two ways out are

- allow spurious failure, or
- guarantee ordering on failure

For trylock, the second adds unpleasant overhead, while the first seems
to precisely prohibit a set of usages (doing things only in response to
another thread acquiring a lock) that I think we all agree are
undesirable.

> 
> The situation is not too different than
>   Thread 1:
>       x.store(1);
>       y.store(1);
>   Thread 2:
>       r2 = if (somePredicate) y.cas(0, 1);
>       r3 = x.load();   // may yield 0 if r2 false
> 
> When the r2 line is a tryLock, we just so happen to know the 
> value of a predicate that might be unknowable with multiple 
> threads. There is probably a larger category of these things 
> that are all only SC if you assume that the predicates are 
> indeed opaque. This suggests some formulation of SC that says 
> that for purposes of analysis, they can spuriously fail.
> Although this does not not necessarily mean the operations 
> should be spec'ed or implemented that way.

I think cas is a little different, in that different variants require
special treatment.  It does seem to me that Java's strong version, and
the C++ version (with an updated reference to the old value as an
argument) can be legitimately used as loads, and really need ordering by
default, even in the failure case.  (That was an earlier thread here.)
Java's weak version clearly doesn't need the ordering, since it can't be
used as a load.

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.

Hans


> 
> -Doug
> 
> 
> 
> --
> cpp-threads mailing list
> cpp-threads at decadentplace.org.uk
> http://www.decadentplace.org.uk/cgi-bin/mailman/listinfo/cpp-threads
>