lkmm.lists.linux.dev archive mirror
 help / color / mirror / Atom feed
From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
To: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>,
	Alan Stern <stern@rowland.harvard.edu>
Cc: paulmck@kernel.org, parri.andrea@gmail.com, will@kernel.org,
	peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com,
	dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr,
	akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org,
	urezki@gmail.com, quic_neeraju@quicinc.com, frederic@kernel.org,
	linux-kernel@vger.kernel.org, lkmm@lists.linux.dev
Subject: Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model
Date: Mon, 29 Jul 2024 16:45:58 +0200	[thread overview]
Message-ID: <00f58d20-f92d-461e-beac-b307905cab3b@huaweicloud.com> (raw)
In-Reply-To: <eb9548de-e66e-3dcd-9136-8702a5bc2934@huaweicloud.com>



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



  reply	other threads:[~2024-07-29 15:02 UTC|newest]

Thread overview: 7+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <20240604152922.495908-1-jonas.oberhauser@huaweicloud.com>
     [not found] ` <88c1ebc8-4805-4d1d-868a-889043899979@rowland.harvard.edu>
     [not found]   ` <bbc3bd10-3bf5-4b1a-a275-dd328c42e307@huaweicloud.com>
     [not found]     ` <f93f140b-13bc-4d00-adee-46cc1c016480@rowland.harvard.edu>
     [not found]       ` <4792c9e7-2594-3600-5d82-4cb1443fe670@huaweicloud.com>
2024-07-12  8:06         ` [PATCHv2 0/4] tools/memory-model: Define more of LKMM in tools/memory-model Hernan Ponce de Leon
2024-07-29 13:30           ` Hernan Ponce de Leon
2024-07-29 14:45             ` Jonas Oberhauser [this message]
2024-07-29 15:19               ` Hernan Ponce de Leon
2024-07-29 15:44                 ` Jonas Oberhauser
2024-07-29 15:53                   ` Hernan Ponce de Leon
2024-07-29 16:05                     ` Jonas Oberhauser

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=00f58d20-f92d-461e-beac-b307905cab3b@huaweicloud.com \
    --to=jonas.oberhauser@huaweicloud.com \
    --cc=akiyks@gmail.com \
    --cc=boqun.feng@gmail.com \
    --cc=dhowells@redhat.com \
    --cc=dlustig@nvidia.com \
    --cc=frederic@kernel.org \
    --cc=hernan.poncedeleon@huaweicloud.com \
    --cc=j.alglave@ucl.ac.uk \
    --cc=joel@joelfernandes.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=lkmm@lists.linux.dev \
    --cc=luc.maranget@inria.fr \
    --cc=npiggin@gmail.com \
    --cc=parri.andrea@gmail.com \
    --cc=paulmck@kernel.org \
    --cc=peterz@infradead.org \
    --cc=quic_neeraju@quicinc.com \
    --cc=stern@rowland.harvard.edu \
    --cc=urezki@gmail.com \
    --cc=will@kernel.org \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).