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

[Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>]

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

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

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

> 
> Implementation-wise, there are two things that I would like to have:
> 
> - atomic_add_unless implementation is treated different than the rest 
> and it is one of the few remaining cases where memory orderings are 
> hardcoded [2]. I would like to define it in the .def file as
> 
>      atomic_add_unless(X,V,U) __atomic_add_unless{ONCE}(X,V,U)
> 
> - "deref" and "lderef" instructions seems to add a "rb_dep" fence. None 
> of the model files (.cat, .def, .bell) refers to "rb_dep" so this looks 
> useless to me. However, I never checked the details of these 
> dereferencing instruction so I might be missing something. Maybe Paul 
> can clarify.
> 
> Hernan
> 
> [1] https://github.com/herd/herdtools7/pull/865
> [2] https://github.com/herd/herdtools7/issues/868
> 
> 
> diff --git a/tools/memory-model/linux-kernel.def 
> b/tools/memory-model/linux-kernel.def
> index 001366ff3fb4..5a40c2cad39b 100644
> --- a/tools/memory-model/linux-kernel.def
> +++ b/tools/memory-model/linux-kernel.def
> @@ -32,10 +32,10 @@ xchg(X,V)  __xchg{MB}(X,V)
>   xchg_relaxed(X,V) __xchg{ONCE}(X,V)
>   xchg_release(X,V) __xchg{RELEASE}(X,V)
>   xchg_acquire(X,V) __xchg{ACQUIRE}(X,V)
> -cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W)
> -cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W)
> -cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W)
> -cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W)
> +cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
> +cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
> +cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
> +cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(X,V,W)
> 
>   // Spinlocks
>   spin_lock(X) { __lock(X); }
> @@ -63,14 +63,14 @@ atomic_set(X,V) { WRITE_ONCE(*X,V); }
>   atomic_read_acquire(X) smp_load_acquire(X)
>   atomic_set_release(X,V) { smp_store_release(X,V); }
> 
> -atomic_add(V,X) { __atomic_op(X,+,V); }
> -atomic_sub(V,X) { __atomic_op(X,-,V); }
> -atomic_and(V,X) { __atomic_op(X,&,V); }
> -atomic_or(V,X)  { __atomic_op(X,|,V); }
> -atomic_xor(V,X) { __atomic_op(X,^,V); }
> -atomic_inc(X)   { __atomic_op(X,+,1); }
> -atomic_dec(X)   { __atomic_op(X,-,1); }
> -atomic_andnot(V,X) { __atomic_op(X,&~,V); }
> +atomic_add(V,X) { __atomic_op{NORETURN}(X,+,V); }
> +atomic_sub(V,X) { __atomic_op{NORETURN}(X,-,V); }
> +atomic_and(V,X) { __atomic_op{NORETURN}(X,&,V); }
> +atomic_or(V,X)  { __atomic_op{NORETURN}(X,|,V); }
> +atomic_xor(V,X) { __atomic_op{NORETURN}(X,^,V); }
> +atomic_inc(X)   { __atomic_op{NORETURN}(X,+,1); }
> +atomic_dec(X)   { __atomic_op{NORETURN}(X,-,1); }
> +atomic_andnot(V,X) { __atomic_op{NORETURN}(X,&~,V); }
> 
>   atomic_add_return(V,X) __atomic_op_return{MB}(X,+,V)
>   atomic_add_return_relaxed(V,X) __atomic_op_return{ONCE}(X,+,V)
> @@ -127,10 +127,10 @@ atomic_xchg(X,V) __xchg{MB}(X,V)
>   atomic_xchg_relaxed(X,V) __xchg{ONCE}(X,V)
>   atomic_xchg_release(X,V) __xchg{RELEASE}(X,V)
>   atomic_xchg_acquire(X,V) __xchg{ACQUIRE}(X,V)
> -atomic_cmpxchg(X,V,W) __cmpxchg{MB}(X,V,W)
> -atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE}(X,V,W)
> -atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE}(X,V,W)
> -atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE}(X,V,W)
> +atomic_cmpxchg(X,V,W) __cmpxchg{MB,ONCE}(X,V,W)
> +atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{ONCE,ONCE}(X,V,W)
> +atomic_cmpxchg_acquire(X,V,W) __cmpxchg{ACQUIRE,ONCE}(X,V,W)
> +atomic_cmpxchg_release(X,V,W) __cmpxchg{RELEASE,ONCE}(X,V,W)
> 
>   atomic_sub_and_test(V,X) __atomic_op_return{MB}(X,-,V) == 0
>   atomic_dec_and_test(X)  __atomic_op_return{MB}(X,-,1) == 0