Re: LKMM: Making RMW barriers explicit

[Alan Stern]

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

Alan