Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model

[Jonas Oberhauser]

Am 7/29/2024 um 3:30 PM schrieb Hernan Ponce de Leon:
> On 7/12/2024 10:06 AM, Hernan Ponce de Leon wrote:
> > On 6/10/2024 10:38 AM, Hernan Ponce de Leon wrote:
> > > On 6/8/2024 3:00 AM, Alan Stern wrote:
> > > > On Wed, Jun 05, 2024 at 09:58:42PM +0200, Jonas Oberhauser wrote:
> > > > > Am 6/4/2024 um 7:56 PM schrieb Alan Stern:
> > > > > > Just to clarify: Your first step encompasses patches 1 - 3, and the
> > > > > > second step is patch 4.  The first three patches can be applied 
> > > > > > now, but
> > > > > > the last one needs to wait until herd7 has been updated.  Is this all
> > > > > > correct?
> > > > >
> > > > > Exactly.
> > > >
> > > > With regard to patch 4, how much thought have you and Hernan given to
> > > > backward compatibility?  Once herd7 is changed, old memory model files
> > > > will no longer work correctly.
> > >
> > > Honestly, I did not think much about this (at least until Akira 
> > > mentioned in my PR). My hope was that changes to the model could be 
> > > back-ported to previous kernel versions. However that would not work 
> > > for existing out-of-tree files.
> > >
> > > My question is: is compatibility with out-of-tree files really a 
> > > requirement? I would argue that if people are using outdated models, 
> > > they may get wrong results anyway. This is because some of the 
> > > changes done to lkmm during the last few years change the expected 
> > > result for some litmus tests.
> > >
> > > Hernan
> >
> > I pushed some new changes to the code for backward compatibility [1]. 
> > The series also needs the patch at the bottom to properly deal with 
> > the ordering of failing CAses and non-returning operations. With it, 
> > all litmus tests return the correct result (the script needs to pass 
> > option -lkmm-legacy false to herd).
>
> I have been playing around with an alternative to this.
>
> Rather than implementing this as an "option", I can implemented it as a 
> "model variant (*)" and add this to the model

How exactly do these model variants get selected?

I was thinking that another good approach could be to have a new generic 
C model which doesn't know anything about LKMM. I believe this would be 
specified in the header of the .litmus files?


> flag ~empty (if "lkmmlatest" then 0 else _)
>    as new-lkmm-models-require-variant-lkmmlatest
>
> If the user forgets to set the variant for the new model, herd7 will 
> flag the executions showing that something is off.
>
> To be fully backward compatible, we would need to backport this to old 
> models
>
> flag ~empty (if "lkmmlatest" then 1 else _)
>    as new-lkmm-models-require-variant-lkmmlatest

should this be then _ else 0  ? or what does the _ do here?

I also don't think we can backport things to old models

> If the user (wrongly) sets the variant for an old model, the the 
> executions will be flagged.
>
> Any thoughts?
>
> Hernan
>
> (*) This trick seems to be used for some arm models
>
> https://github.com/herd/herdtools7/blob/master/herd/libdir/arm-models/mixed/ec.cat#L66C1-L67C67