Re: [PATCH] tools/memory-model: Document herd7 (internal) representation

[Jonas Oberhauser]

Am 5/29/2024 um 4:24 PM schrieb Alan Stern:
> On Wed, May 29, 2024 at 04:17:36PM +0200, Jonas Oberhauser wrote:
> > Am 5/29/2024 um 4:07 PM schrieb Alan Stern:
> > > On Wed, May 29, 2024 at 02:37:30PM +0200, Jonas Oberhauser wrote:
> > > > Given herd's other syntactic limitations, perhaps the best way would be to
> > > > introduce these macros as
> > > >
> > > > 	x = cmpxchg(...) {
> > > > 		__fence{mb-successful-rmw};
> > > >    		x = __cmpxchg{once}(...);
> > > >    		__fence{mb-successful-rmw};
> > > > 	}
> > > >
> > > > since I think x = M(...) is the only way we are allowed to use these macros
> > > > anyways.
> > >
> > > If we did this, how would the .cat file know to ignore the fence events
> > > when the cmpxchg() fails?  It doesn't look like there's anything to
> > > connect the two of them.
> > >
> > > Adding the MB tag to the cmpxchg itself seems like the only way forward.
> > >
> > > Alan
> >
> > Something along these lines:
> >
> >    Mb = Mb | Mb-successful-rmw & (domain((po\(po;po));rmw) |
> > range(rmw;(po\(po;po)))
> >
> > i.e., using the fact that these mb-successful-rmw fences must appear
> > directly next to a possibly failing rmw, and looking for successful rmw
> > directly around them.
> >
> > I suppose we have to distinguish between the before- and after- fences
> > though to make it work for cases like
> >
> > xchg_release();
> > cmpxchg(); // fails
> >
> >
> >                  __xchg_release(...); // is an rmw
> >   		__fence{mb-successful-rmw}; // wrong takes mb semantics
> >     		x = __cmpxchg{once}(...); // fails
> >     		__fence{mb-successful-rmw};
> >
> >
> > So that would leave us with
> >
> >   	x = cmpxchg(...) {
> >   		__fence{mb-before-successful-rmw};
> >     		x = __cmpxchg{once}(...);
> >     		__fence{mb-after-successful-rmw};
> >   	}
> >
> > and in .cat/.bell:
> >
> >    Mb = Mb | Mb-before-successful-rmw & domain((po\(po;po));rmw) |
> > Mb-after-successful-rmw & range(rmw;(po\(po;po)))
>
> It's messy.  Associating the fences directly with the RMW event(s) by
> adding the MB tags is much cleaner, IMO.

I agree.

> Also, does the syntax you are proposing require changes to herd7?  I'm
> not aware that it is currently able to parse that kind of definition.

Indeed, herd7 can't deal with this syntax right now.

   jonas