Re: LKMM: Making RMW barriers explicit

[Boqun Feng]

On Thu, May 23, 2024 at 09:38:05PM -0400, Alan Stern wrote:
> On Thu, May 23, 2024 at 08:14:38AM -0700, Boqun Feng wrote:
> > Besides, I'm not sure this is a good idea. Because the "{mb}, {once},
> > etc" part is a syntax thing, you write a cmpxchg(), it should be
> > translated to a cmpxchg event with MB tag on. As to failed cmpxchg()
> > doesn't provide ordering, it's a semantics thing, as Jonas showed that
> > it can be represent in cat file. As long as it's a semanitc thing and we
> > can represent in cat file, I don't think we want herd to give a special
> > treatment.
> 
> I don't really understand the distinction you're making between 
> syntactic things and semantic things.  For most instructions there's no 

Syntax is how the code is written, and semantic is how the code is
executed (in each execution candidate). So if we write a cmpxchg{mb}(),
and in execution candiates, it could generates a read{MB} event and a
write{MB} event (succeed case), or a read{MB} event (fail case), "{MB}"
here doesn't mean it's a full barrier, it only means the event comes
from a no suffix API. Here "{MB}" only has syntactic meaning (no
semantic meaning).

> problem, because the instruction does just one thing.  But a cmpxchg 
> instruction can do either of two things, depending on whether it 
> succeeds or fails, so it makes sense to tell herd7 how to represent 
> both of them.
> 
> > What you and Jonas looks fine to me, since it moves the semantic bits
> > from herd internal to cat file.
> 
> Trying to recognize failed RMW events by looking for R events with an mb 
> tag that aren't in the rmw relation seems very artificial.  That fact 

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.

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

Regards,
Boqun

> Alan