Messages in this thread | | | From | Luc Maranget <> | Date | Wed, 26 Feb 2020 10:46:37 +0100 | Subject | Re: More on reader-writer locks |
| |
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
| |