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

[Jonas Oberhauser]

On 2/27/2023 6:57 PM, Joel Fernandes wrote:
> On Mon, Feb 27, 2023 at 9:39 AM Jonas Oberhauser
> <jonas.oberhauser@xxxxxxxxxxxxxxx> wrote:
> > On 2/26/2023 5:23 PM, Joel Fernandes wrote:
> > > On Fri, Feb 24, 2023 at 02:52:51PM +0100, Jonas Oberhauser wrote:
> > > > [...]
> > > Alternatively can be the following appended diff? Requires only single 'int'
> > > in ->ppo then and prevents future similar issues caused by sub relations.
> > > Also makes clear that ->ppo can only be CPU-internal.
> > I had thought about going in that direction, but it doesn't prevent
> > future similar issues, at best makes them less likely.
> Making less likely still sounds like a win to me.
>
> > For example, you could have an xfence that somehow goes back to the
> > original thread, but to a po-earlier event (e.g., like prop).
> >
> > Given that to-r and to-w are unlikely to ever become become inconsistent
> > with po, I am not sure it even really helps much.
> I am not sure I understand, what is the problem with enforcing that
> ppo is only supposed to ever be -int ? Sounds like it makes it super
> clear.

You could go further and do ... & po.

But it would still make me feel that it's a plaster used to hold 
together a steampipe.
It reminds me a bit of college when some of my class mates passed the 
nightly tests in the programming lab by doing
"if input == (the input of the specific test case they were having 
problem with) return (value expected by testcase)".
Or making everything atomic so that tsan does not complain about data 
races anymore.

If there's something in one of these relations tying together events of 
different threads, is it intentional or a bug?
I prefer to be very conscious about what is being tied together by the 
relations.

I'd rather take Boqun's suggestion to add some "debug/testing" flags to 
see if a litmus test violates a property assumed by LKMM.

Yet I think the ideal way is to have a mechanized proof that LKMM 
satisfies these properties and use that to avoid regressions.


> > Personally I'm not too happy with the ad-hoc '& int' because it's like
> So, with the idea I suggest, you will have fewer ints so you should be happy ;-)

haha : ) An alternative perspective is that the &int now covers more 
cases of the relation ; )


> > adding some unused stuff (via ... | unused-stuff) and then cutting it
> > back out with &int, unlike prop & int which has a real semantic meaning
> > (propagate back to the thread). The fastest move is the move we avoid
> > doing, so I rather wouldn't add those parts in the first place.
> >
> > However fixing the fence relation turned out to be a lot trickier, both
> > because of the missed data race and also rmw-sequences, essentially I
> > would have had to disambiguate between xfences and fences already in
> > this patch. So I did this minimal local fix for now and we can discuss
> > whether it makes sense to get rid of the '& int' once/if we have xfence etc.
> I see. Ok, I'll defer to your expertise on this since you know more
> than I. I am relatively only recent with even opening up the CAT code.

Enjoy : )

jonas