Received-SPF: pass (google.com: domain of linux-kernel+bounces-195788-linux.lists.archive=gmail.com@vger.kernel.org designates 2604:1380:40f1:3f00::1 as permitted sender) client-ip=2604:1380:40f1:3f00::1;
Message-ID: <905ec2b5-3fad-f3bc-4801-2186225145e1@huaweicloud.com>
Date: Thu, 30 May 2024 20:33:18 +0200
Precedence: bulk
MIME-Version: 1.0
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:102.0) Gecko/20100101
 Thunderbird/102.13.0
Subject: Re: [RFC][PATCH 0/4] tools/memory-model: Define more of LKMM in
 ,tools/memory-model
Content-Language: en-US
References: <12050799-e7e5-a7be-44c6-7b4832d56419@huaweicloud.com>
To: "Paul E. McKenney" <paulmck@kernel.org>
Cc: stern@rowland.harvard.edu, 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, jonas.oberhauser@huaweicloud.com
From: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
In-Reply-To: <12050799-e7e5-a7be-44c6-7b4832d56419@huaweicloud.com>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit

It seems I did something wrong when I imported to my email client the 
original email from Jonas and I removed most people form the recipient 
list. Thus, I am sending again my last email.

Sorry for the inconvenience.

	Hernan


-------- Forwarded Message --------
Subject: Re: [RFC][PATCH 0/4] tools/memory-model: Define more of LKMM in
Date: Thu, 30 May 2024 09:54:09 +0200
From: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>, paulmck@kernel.org
CC: stern@rowland.harvard.edu, parri.andrea@gmail.com, will@kernel.org

On 5/29/2024 4:19 PM, Jonas Oberhauser wrote:
> Thanks for checking the results!
> 
>> The issue is probably that there are sill a few hardcoded tags in the 
>> code, like "noreturn" [3]. I am still not to sure what the best 
>> solution would be for those.
>>
>>      Hernan
> 
> IMHO the best thing to do with noreturn for the time being would be to 
> allow __atomic_op{NORETURN}(...), but that may require bigger changes in 
> herd (does it?).
>

I already added support for his.

I also removed the hardcoded memory orderings in the CAS events. Now we 
can specify both orderings as __cmpxchg{mo-pass,mo-fail}(X,V,W)

If I apply the patch below on top of the series, I get all correct results.

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


> Do you have a more or less full list of the other hardcoded things?

I think this is what still remains hardcoded
- "srcu-lock" -> seems to be used to decide some value written by the 
memory events representing lock/unlock. Not yet sure what to do with this.
- a few "once" -> mostly related to AtomicAddUnless and return 
operations. I think we can replace those with macros. This is my next goal.
- "rb_dep" -> It seems "deref" and "lderef" are replaced by a load 
followed by a fence. The code doing the replacement states "Cannot do 
this with a macro, by lack of sequencing expression operator".

	Hernan