Re: More on reader-writer locks

[Luc Maranget]

Hi all,

As far as I understand there is a contradiction between having a "platonic"
implementation of locks (Ã la lock.cat) and a concrete one (for ordinary locks
lock -> load acquire, unlock -> store release, + loop [difficult for herd]
or filter clause).

So if reader/writer locks are catified in a platonic way, we cannot
use various atomic primitives. Instead, we give them an abstract semantics
based upon some axiomatisation of their semantics, using cat means.
Such an axionatisation  does not seem straightforward because,
by constrast with locks, there is an integer count
hiddden, and not a simple boolean as for ordinary locks

Some idea would be first to partition reader crtical sections,
and then for each such partition, order elements of the partition and
writer critical section. For one such choice there are still many possible
rf relations...

--Luc

rf relation 
> On Tue, 25 Feb 2020, Luc Maranget wrote:
> 
> > Hi,
> > 
> > As far as I can remember I have implemented atomic_add_unless in herd7.
> 
> Luc, have you considered whether we can use atomic_add_unless and
> cmpxchg to implement reader-writer locks in the LKMM?  I don't think we
> can handle them the same way we handle ordinary locks now.
> 
> Let's say that a lock variable holds 0 if it is unlocked, -1 if it is 
> write-locked, and a positive value if it is read-locked (the value is 
> the number of read locks currently in effect).  Then operations like 
> write_lock, write_trylock, and so on could all be modeled using 
> variants of atomic_add_unless, atomic_dec, and cmpxchg.
> 
> But will that work if the reads-from relation is computed by the cat 
> code in lock.cat?  I suspect it won't.
> 
> How would you approach this problem?
> 
> Alan