Re: [RFC][PATCH 4/4] tools/memory-model: Distinguish between syntactic and semantic tags

[Alan Stern]

On Tue, May 28, 2024 at 02:49:38PM +0200, Jonas Oberhauser wrote:
> > > +let Mb = MB \ FailedRMW
> > > >>   (* Compute marked and plain memory accesses *)
> > > -let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
> > > +let Marked = (~M) | IW | ONCE | RELEASE | ACQUIRE | MB | domain(rmw) | range(rmw) |
> > 
> > The new MB term isn't needed, because MB tags on memory accesses are
> > filtered out unless the access also belongs to domain(rmw) | range(rmw).
> > 
> > Alan
> 
> 
> Thanks for all the notes.
> I think on this one is needed though under the assumption that herd7 would
> no longer know internally to replace the MB with ONCE in case
> of failure.

And I was wrong because failed RMW instructions are filtered out of Mb, 
not out of MB.

Hmmm, this raises another question: Shouldn't the R event for a failed 
cmpxchg_release count as marked?  At the moment it's not clear how such 
events will be tagged.  Perhaps the best thing to do is add RMW to 
this list, which would make domain(rmw) and range(rmw) unnecessary.

And then we probably don't need to keep MB -- unless smp_store_mb()'s 
definition ever gets reduced to __store{MB}(X,V).

Alan