Re: LKMM: Making RMW barriers explicit

[Alan Stern]

On Fri, May 24, 2024 at 07:34:06AM -0700, Boqun Feng wrote:
> On Fri, May 24, 2024 at 10:14:25AM -0400, Alan Stern wrote:
> [...]
> > > Not really, RMW events contains all events generated from
> > > read-modify-write primitives, if there is an R event without a rmw
> > > relation (i.e there is no corresponding write event), it's a failed RWM
> > > by definition: it cannot be anything else.
> > 
> > Not true.  An R event without an rmw relation could be a READ_ONCE().  
> 
> No, the R event is already in the RWM events, it has come from a rwm
> atomic.

Oh, right.  For some reason I was thinking that an instruction could 
belong to only one set, R or RMW.  But that doesn't make sense.

> > Or a plain read.  The memory model uses the tag to distinguish these 
> > cases.
> > 
> > > > that it would work is merely an artifact of herd7's internal actions.  I 
> > > > think it would be much cleaner if herd7 represented these events in some 
> > > > other way, particularly if we can tell it how.
> > > > 
> > > > After all, herd7 already does generate different sets of events for 
> > > > successful (both R and W) and failed (only R) RMWs.  It's not such a big 
> > > > stretch to make the R events it generates different in the two cases.
> > > > 
> > > 
> > > I thought we want to simplify the herd internal processing by avoid
> > > adding mb events in cmpxchg() cases, in the same spirit, if syntactic
> > > tagging is already good enough, why do we want to make herd complicate?
> > 
> > Herd7 already is complicated by the fact that it needs to handle 
> > cmpxchg() instructions in two ways: success and failure.  This 
> > complication is unavoidable.  Adding one extra layer (different tags for 
> > the different ways) is an insignificant increase in the complication, 
> > IMO. And it's a net reduction when you compare it to the amount of 
> > complication currently in the herd7 code.
> > 
> > Also what about cmpxchg_acquire()?  If it fails, it will generate an R 
> > event with an acquire tag not in the rmw relation.  There is no way to 
> > tell such events apart from a normal smp_load_acquire(), and so the .cat 
> > file would have no way to know that the event should not have acquire 
> > semantics.  I guess we would have to rename this tag, as well.
> 
> No,
> 
> 	let read_of_rmw = (RMW & R) 
> 	let fail_read_of_rmw = read_of_rmw / dom(rmw)
> 	let fail_cmpxchg_acquire = fail_read_of_rmw & [Acquire]
> 
> gives you all the failed cmpxchg_acquire() apart from a normal
> smp_load_acquire().

Yes, I see.  Using this approach, no further changes to herd7 or the 
def file would be needed.  We would just have to add 'mb to the 
Accesses enumeration and to the list of tags allowed for an RMW 
instruction.

Question: Since R and RMW have different lists of allowable tags, how 
does herd7 decide which tags are allowed for an event that is in both 
the R and RMW sets?

Alan