Re: [PATCHv2 3/4] tools/memory-model: Define effect of Mb tags on RMWs in tools/...

[Jonas Oberhauser]

Am 6/5/2024 um 6:28 AM schrieb Boqun Feng:
> On Tue, Jun 04, 2024 at 06:04:40PM +0200, Jonas Oberhauser wrote:
> > Herd7 transforms successful RMW with Mb tags by inserting smp_mb() fences
> > around them. We emulate this by considering imaginary po-edges before the
> > RMW read and before the RMW write, and extending the smp_mb() ordering
> > rule, which currently only applies to real po edges that would be found
> > around a really inserted smp_mb(), also to cases of the only imagined po
> > edges.
> >
> > Reported-by: Viktor Vafeiadis <viktor@xxxxxxxxxxx>
> > Suggested-by: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> > Signed-off-by: Jonas Oberhauser <jonas.oberhauser@xxxxxxxxxxxxxxx>
> > ---
> >   tools/memory-model/linux-kernel.cat | 10 ++++++++++
> >   1 file changed, 10 insertions(+)
> >
> > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat
> > index adf3c4f41229..d7e7bf13c831 100644
> > --- a/tools/memory-model/linux-kernel.cat
> > +++ b/tools/memory-model/linux-kernel.cat
> > @@ -34,6 +34,16 @@ let R4rmb = R \ Noreturn	(* Reads for which rmb works *)
> >   let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb]
> >   let wmb = [W] ; fencerel(Wmb) ; [W]
> >   let mb = ([M] ; fencerel(Mb) ; [M]) |
> > +	(*
> > +	 * full-barrier RMWs (successful cmpxchg(), xchg(), etc.) act as
> > +	 * though there were enclosed by smp_mb().
> > +	 * The effect of these virtual smp_mb() is formalized by adding
> > +	 * Mb tags to the read and write of the operation, and providing
> > +	 * the same ordering as though there were additional po edges
> > +	 * between the Mb tag and the read resp. write.
> > +	 *)
> > +	([M] ; po ; [Mb & R]) |
> > +	([Mb & W] ; po ; [M]) |
>
> I couldn't help suggestting:
>
> 	([M] ; po ; [Mb & domain(rmw)]) |
> 	([Mb & range(rmw)] ; po ; [M]) |
>
> , it's a bit more clear to me, but maybe the comment above is good
> enough?

Hm, maybe clarity is in the eye of the beholder in this case.

Actually looking at your suggestion makes me think of smp_store_mb(), 
which although represented as Once;F[Mb] could be (mis)understood also 
as Mb&W. And it indeed does the same thing
  ([Mb & W] ; po ; [M])
would suggest.

(btw I think it is confusing that smp_store_mb is not strictly stronger 
than smp_store_release. Of course there are places where you want a 
relaxed store followed by an mb, but usually the mb versions are 
strictly stronger.).

Best wishes,
  jonas