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

[Jonas Oberhauser]

Am 5/28/2024 um 4:01 PM schrieb 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.

> Hmmm, this raises another question: Shouldn't the R event for a failed
> cmpxchg_release count as marked?  

Yes.

> At the moment it's not clear how such
> events will be tagged.

If by "at the moment" you mean the current herd7, then (as mentioned in 
the cover letter) this patch does not work at all with the current herd7 
because IIUC in fact ACQUIRE and RELEASE tags will be replaced by Once 
in all cases (so smp_store_release would be a store Once ...).

However, in a hypothetical version of herd7 which just leaves all the 
syntactic tags intact, we would get R & RMW & RELEASE, which would not 
be in the Release set (by nature of failing and being a read) but would 
be Marked (by nature of having a syntactic RELEASE tag).

> Perhaps the best thing to do is add RMW to
> this list, which would make domain(rmw) and range(rmw) unnecessary.


That's also a good idea.

> And then we probably don't need to keep MB

That's correct, although as a failsafe I would probably keep it anyways 
- it doesn't harm, but it may prevent a gotcha.

Have fun,
  jonas