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

[Jonas Oberhauser]

Am 5/29/2024 um 4:07 PM schrieb Alan Stern:
> On Wed, May 29, 2024 at 02:37:30PM +0200, Jonas Oberhauser wrote:
> > Am 5/28/2024 um 7:58 PM schrieb Boqun Feng:
> > > This may not be trivial. Note that cmpxchg() is an expression (it has a
> > > value), so in .def, we want to define it as an expression. However, the
> > > C-like multiple-statement expression is not supported by herd parser, in
> > > other words we want:
> > >
> > > 	{
> > > 		__fence{mb-successful-rmw};
> > > 		int tmp = __cmpxchg{once}(...);
> > > 		__fence{mb-successful-rmw};
> > > 		tmp;
> > > 	}
> >
> > Oh, you're right. Then probably the rule I was violating is that
> > value-returning macros can not be defined with {} at all.
> >
> > 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)))



Best wishes,
  jonas