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

Doug Lea dl at cs.oswego.edu
Sun Aug 26 00:52:04 BST 2007


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?

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





More information about the cpp-threads mailing list