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

[Hans Boehm]

On Sat, 25 Aug 2007, Doug Lea wrote:

> Hans Boehm wrote:
>>
>>> Unsuccessful locking and unlocking operations, and reentrant locking/unlocking
>>> operations, do not require any memory synchronization effects."
>>>
>> Doug -
>>
>> My concern with this formulation is that, if you don't allow
>> spurious failures for all lock types, I don't see how it guarantees
>> sequential consistency for race-free programs.
>>
>
> I don't get the connection. "Unsuccessful locking" above doesn't
> say why the (try)Lock fails, just that it does.
> In these failure cases, the outcome below would be allowed.
> Am I missing some problem surrounding the fact that it is allowed?
Consider the example, where l1 is a lock type that does not allow
spurious failures, and x is Java volatile, with suitable syntactic
adjustments.  Assume that l1 is locked only on this one occasion by
thread 1.

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.

But this example is race free, and I think the outcome is allowed
in Java.

If surious failures are allowed, then this example becomes SC.  All
of thread 2 can be scheduled before thread 1, and r3 can still be
"failure" because the trylock may have spuriously failed.

Hans

>
>> The example that motivates this:
>>
>>>> Consider the following (variant of a well-known) example,
>>> where x is
>>>> atomic (initially zero, SC ops only) and l1 is initially unlocked:
>>>>
>>>> Thread 1:
>>>>         x.store(1);
>>>>         l1.lock();
>>>>
>>>> Thread 2:
>>>>         r2 = trylock();  // fails
>>>>         r3 = x.load();   // yields 0
>>
>
>
>
> -- 
> cpp-threads mailing list
> cpp-threads at decadentplace.org.uk
> http://www.decadentplace.org.uk/cgi-bin/mailman/listinfo/cpp-threads
>