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. > 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(). Regards, Boqun > > Alan
