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

[Doug Lea]

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.)

It does seem a little crazy though to prohibit an implementation of
tryLock from guaranteeing lack of spurious failure.

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.

-Doug