| lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
|
Open Source and information security mailing list archives
| ||
|
Message-ID: <d6a76968-d10b-c60b-245a-f58116eca6af@huaweicloud.com>
Date: Fri, 12 Jul 2024 10:06:55 +0200
From: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>
To: Alan Stern <stern@...land.harvard.edu>,
Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc: paulmck@...nel.org, parri.andrea@...il.com, will@...nel.org,
peterz@...radead.org, boqun.feng@...il.com, npiggin@...il.com,
dhowells@...hat.com, j.alglave@....ac.uk, luc.maranget@...ia.fr,
akiyks@...il.com, dlustig@...dia.com, joel@...lfernandes.org,
urezki@...il.com, quic_neeraju@...cinc.com, frederic@...nel.org,
linux-kernel@...r.kernel.org, lkmm@...ts.linux.dev
Subject: Re: [PATCHv2 0/4] tools/memory-model: Define more of LKMM in
tools/memory-model
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).
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
Powered by blists - more mailing lists