From mboxrd@z Thu Jan 1 00:00:00 1970 From: paulmck@kernel.org Subject: [PATCH lkmm tip/core/rcu 07/10] tools/memory-model: Add an exception for limitations on _unless() family Date: Wed, 15 Apr 2020 11:49:42 -0700 Message-ID: <20200415184945.16487-7-paulmck@kernel.org> References: <20200415183343.GA12265@paulmck-ThinkPad-P72> Return-path: In-Reply-To: <20200415183343.GA12265@paulmck-ThinkPad-P72> Sender: linux-kernel-owner@vger.kernel.org To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, kernel-team@fb.com, mingo@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, "Paul E . McKenney" List-Id: linux-arch.vger.kernel.org From: Boqun Feng According to Luc, atomic_add_unless() is directly provided by herd7, therefore it can be used in litmus tests. So change the limitation section in README to unlimit the use of atomic_add_unless(). Cc: Luc Maranget Acked-by: Andrea Parri Reviewed-by: Joel Fernandes (Google) Signed-off-by: Boqun Feng Signed-off-by: Paul E. McKenney --- tools/memory-model/README | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/tools/memory-model/README b/tools/memory-model/README index fc07b52..b9c562e 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -207,11 +207,15 @@ The Linux-kernel memory model (LKMM) has the following limitations: case as a store release. b. The "unless" RMW operations are not currently modeled: - atomic_long_add_unless(), atomic_add_unless(), - atomic_inc_unless_negative(), and - atomic_dec_unless_positive(). These can be emulated + atomic_long_add_unless(), atomic_inc_unless_negative(), + and atomic_dec_unless_positive(). These can be emulated in litmus tests, for example, by using atomic_cmpxchg(). + One exception of this limitation is atomic_add_unless(), + which is provided directly by herd7 (so no corresponding + definition in linux-kernel.def). atomic_add_unless() is + modeled by herd7 therefore it can be used in litmus tests. + c. The call_rcu() function is not modeled. It can be emulated in litmus tests by adding another process that invokes synchronize_rcu() and the body of the callback -- 2.9.5 From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail.kernel.org ([198.145.29.99]:45914 "EHLO mail.kernel.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1416863AbgDOStt (ORCPT ); Wed, 15 Apr 2020 14:49:49 -0400 From: paulmck@kernel.org Subject: [PATCH lkmm tip/core/rcu 07/10] tools/memory-model: Add an exception for limitations on _unless() family Date: Wed, 15 Apr 2020 11:49:42 -0700 Message-ID: <20200415184945.16487-7-paulmck@kernel.org> In-Reply-To: <20200415183343.GA12265@paulmck-ThinkPad-P72> References: <20200415183343.GA12265@paulmck-ThinkPad-P72> Sender: linux-arch-owner@vger.kernel.org List-ID: To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, kernel-team@fb.com, mingo@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, "Paul E . McKenney" Message-ID: <20200415184942.OrclyB9fD61ujO2CxwxFUiCZvtsKP54-7jTubvrX_ng@z> From: Boqun Feng According to Luc, atomic_add_unless() is directly provided by herd7, therefore it can be used in litmus tests. So change the limitation section in README to unlimit the use of atomic_add_unless(). Cc: Luc Maranget Acked-by: Andrea Parri Reviewed-by: Joel Fernandes (Google) Signed-off-by: Boqun Feng Signed-off-by: Paul E. McKenney --- tools/memory-model/README | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/tools/memory-model/README b/tools/memory-model/README index fc07b52..b9c562e 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -207,11 +207,15 @@ The Linux-kernel memory model (LKMM) has the following limitations: case as a store release. b. The "unless" RMW operations are not currently modeled: - atomic_long_add_unless(), atomic_add_unless(), - atomic_inc_unless_negative(), and - atomic_dec_unless_positive(). These can be emulated + atomic_long_add_unless(), atomic_inc_unless_negative(), + and atomic_dec_unless_positive(). These can be emulated in litmus tests, for example, by using atomic_cmpxchg(). + One exception of this limitation is atomic_add_unless(), + which is provided directly by herd7 (so no corresponding + definition in linux-kernel.def). atomic_add_unless() is + modeled by herd7 therefore it can be used in litmus tests. + c. The call_rcu() function is not modeled. It can be emulated in litmus tests by adding another process that invokes synchronize_rcu() and the body of the callback -- 2.9.5