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

From: Hernan Ponce de Leon
Date: Mon Jul 29 2024 - 11:54:13 EST

On 7/29/2024 5:44 PM, Jonas Oberhauser wrote:


Am 7/29/2024 um 5:19 PM schrieb Hernan Ponce de Leon:
On 7/29/2024 4:45 PM, Jonas Oberhauser wrote:


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?

Yes, my bad.


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

IIRC I have seen (non lkmm related) patches being backported to stable kernel versions. Why can't we do this for lkmm if backward compatibility is really a requirement? Otherwise I don't see a way of preventing developers to use old models with the new option (since I plan to keep the "old variant" as default, this would have to be done on purpose, but still).

I don't think this is a problem. If the old version is the default, and we define it in the .cfg file for the tree version of LKMM, then it will work correctly for both the old and new versions. People playing around with Memory Models should be careful enough not to intentionally break the model by passing bogus options.

The same was true for my implementation using the lkmm-legacy option rather than the model variant, but this was still considered to break backward compatibility.

https://github.com/herd/herdtools7/pull/865#issuecomment-2229930493


Of course, defining a new syntax identifier and putting it in all headers would be more robust. But it's more work and I would only do that if we really got rid of all the LKMM specifics.

Have fun,
  jonas