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

[Hans Boehm]

On Sat, 25 Aug 2007, Doug Lea wrote:

>> Specifically, trylock may return "I did not lock" even though the
>> lock was free.  (Spuriously locking when the lock was not free
>> would be ... bad.)
>>
>
> Notice though that the concept of a lock being free is itself
> different across different kinds of locks.
>
> Inside lock implementations, you sometimes have a choice
> about whether you want to allow a given tryLock to succeed.
> For example, with pure FIFO/fair locks, you might decide to return
> false from tryLock if the lock is momentarily free but some other
> thread should get it first. Digressing a little:
> We don't actually do this in Java ReentrantLock etc. We debated it.
> Either way is a bit arbitrary, but specifically exempting
> tryLock from fairness rules seems slightly preferable, so that's
> what we do, and document.
>
> A better case in point is read-write locks, where tryLock will fail
> or succeed according to reader/writer/FIFO preference criteria.
>
> These sorts of considerations led us to explicitly not require memory
> effects for failed tryLocks. Pasting from java.util.concurrent.locks.Lock:
>
>
> "All Lock implementations must enforce the same memory synchronization semantics
> as provided by the built-in monitor lock, as described in  The Java Language
> Specification, Third Edition (17.4 Memory Model):
>
>     * A successful lock operation has the same memory synchronization effects
> as a successful Lock action.
>     * A successful unlock operation has the same memory synchronization effects
> as a successful Unlock action.
>
> 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.

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

Seems to be easy to translate to Java by making x volatile.  It is
race-free since all operations are synchronization operations.  But the
indicated outcome is clearly not sequentially consistent.

Hans