Re: [PATCH v2 2/2] tools/memory-model: Make ppo a subrelation of po

[Jonas Oberhauser]

On 1/31/2023 5:55 PM, Alan Stern wrote:
> On Tue, Jan 31, 2023 at 04:33:25PM +0100, Jonas Oberhauser wrote:
> > More precisely, I would change
> >
> > > 	For each other CPU C', any store which propagates to C before
> > > 	a release fence is executed (including all po-earlier
> > > 	stores executed on C) is forced to propagate to C' before the
> > > 	store associated with the release fence does.
> > Into something like
> >
> >
> >       For each other CPU C', any *external* store which propagates to C
> > before
> >       a release fence is executed as well as any po-earlier
> >       store executed on C is forced to propagate to C' before the
> >       store associated with the release fence does.
> >
> > The difference is that po-later stores that happen to propagate to C before
> > the release fence is executed would no longer be ordered.
> > That should be consistent with the axiomatic model.
> I had to check that it wouldn't affect the (xbstar & int) part of vis,
> but it looks all right.  This seems like a reasonable change.
>
> However, it only fixes part of the problem.  Suppose an external write
> is read by an instruction po-after the release-store, but the read
> executes before the release-store.  The operational model would still
> say the external write has to obey the propagation ordering, whereas the
> formal model doesn't require it.


Ouch. I had only thought about the [W];(xbstar & int);[Release] case, 
but there's also the rfe;(xbstar & int);[Release] case....


> > Any additional concerns/changes for this patch?
> It should give the same data-race diagnostics as the current LKMM.  This
> probably means the patch will need to punch up the definitions of
> *-pre-bounded and *-post-bounded, unless you can think of a better
> approach.
>
> Alan

Seems the 1 thing per patch mentally hasn't yet become ingrained in me. 
Thanks!

jonas