From nobody Tue Dec 16 11:06:41 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 291861FCCFD; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; cv=none; b=Pg+FI739a6yCHw7Ik/SEFjX0/sSZ4Z4VuGWj9U/Ev2boIf7+rS4vAqubS/CBkS9MXldLbsnCni9go4xhCGLV+iLZHF3a4JFPb/KT/l4WtcDNOeJVZ6c4mC4A/W0UTHEoqFY8cJae/Q65ZwiGBbuw313hFXE6FQajjrQkNFWtXHs= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; c=relaxed/simple; bh=01pGRoOVLm7FmVgPZ/DAaMBZsWrBo+heyMml9ojdBqE=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=I3teGjrtouVkBDEKKJMAPe4xdLG4BReN7AX9ytofBbDfkC8yMu5jYIFdwJpi1Z9ybhDn3o5PWB9vuWI1zLXsEcHWlBisEI9F7sjvpwb0LS07klwo6geFUxOplvJhl4ctxu3K2oMPVbKvFVbeguCORmM97t8ncdU2prAHuhzp00c= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=IntIdG5T; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="IntIdG5T" Received: by smtp.kernel.org (Postfix) with ESMTPSA id E25A1C4CED1; Thu, 20 Feb 2025 16:14:04 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1740068045; bh=01pGRoOVLm7FmVgPZ/DAaMBZsWrBo+heyMml9ojdBqE=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=IntIdG5TdZt9kIcE7uowpyd2fPl52hC1g4IeHUPC5ZQs7EIRUl+jdPeCLlM9cHrAW uh5rqBx+TIn0zTEAypeQk1ewg+2w//4/gqtihPpNmfQmwYfsqlHczMRwwRb5O7Idv/ DV8xmW3bx2jQ2dJ5CpRNcDtoQfUK3rgrvH2Wn0WkwDxgGnJAXmw44sFOTBio7OBbiT MUHgqCGlTRAo6QnHLHUfGE8d1rF8aHZxv0jt/lLmlLBl9LOIcZHcFVSOKaLRWvIzht bxX+EktSzAaftCkMtZ1fonMbpBPLrYFLOdNLVm+qheSJzjVIPJ1BZPWagv4nXVYWn8 wyKaQDFEIcmKA== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id 9A69DCE0B34; Thu, 20 Feb 2025 08:14:04 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, lkmm@lists.linux.dev, kernel-team@meta.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, Puranjay Mohan , "Paul E . McKenney" , Daniel Lustig , Joel Fernandes Subject: [PATCH memory-model 1/7] tools/memory-model: Add atomic_and()/or()/xor() and add_negative Date: Thu, 20 Feb 2025 08:13:57 -0800 Message-Id: <20250220161403.800831-1-paulmck@kernel.org> X-Mailer: git-send-email 2.40.1 In-Reply-To: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> References: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Puranjay Mohan Pull-849[1] added the support of '&', '|', and '^' to the herd7 tool's atomics operations. Use these in linux-kernel.def to implement atomic_and()/or()/xor() with all their ordering variants. atomic_add_negative() is already available so add its acquire, release, and relaxed ordering variants. [1] https://github.com/herd/herdtools7/pull/849 Signed-off-by: Puranjay Mohan Acked-by: Andrea Parri Reviewed-by: Boqun Feng Signed-off-by: Paul E. McKenney Cc: Alan Stern Cc: Will Deacon Cc: Peter Zijlstra Cc: Nicholas Piggin Cc: David Howells Cc: Jade Alglave Cc: Luc Maranget Cc: Akira Yokosawa Cc: Daniel Lustig Cc: Joel Fernandes Cc: --- tools/memory-model/linux-kernel.def | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux= -kernel.def index 88a39601f5256..d1f11930ec512 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -65,6 +65,9 @@ atomic_set_release(X,V) { smp_store_release(X,V); } =20 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); } =20 @@ -77,6 +80,21 @@ atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{once}(X,= +,V) atomic_fetch_add_acquire(V,X) __atomic_fetch_op{acquire}(X,+,V) atomic_fetch_add_release(V,X) __atomic_fetch_op{release}(X,+,V) =20 +atomic_fetch_and(V,X) __atomic_fetch_op{mb}(X,&,V) +atomic_fetch_and_relaxed(V,X) __atomic_fetch_op{once}(X,&,V) +atomic_fetch_and_acquire(V,X) __atomic_fetch_op{acquire}(X,&,V) +atomic_fetch_and_release(V,X) __atomic_fetch_op{release}(X,&,V) + +atomic_fetch_or(V,X) __atomic_fetch_op{mb}(X,|,V) +atomic_fetch_or_relaxed(V,X) __atomic_fetch_op{once}(X,|,V) +atomic_fetch_or_acquire(V,X) __atomic_fetch_op{acquire}(X,|,V) +atomic_fetch_or_release(V,X) __atomic_fetch_op{release}(X,|,V) + +atomic_fetch_xor(V,X) __atomic_fetch_op{mb}(X,^,V) +atomic_fetch_xor_relaxed(V,X) __atomic_fetch_op{once}(X,^,V) +atomic_fetch_xor_acquire(V,X) __atomic_fetch_op{acquire}(X,^,V) +atomic_fetch_xor_release(V,X) __atomic_fetch_op{release}(X,^,V) + atomic_inc_return(X) __atomic_op_return{mb}(X,+,1) atomic_inc_return_relaxed(X) __atomic_op_return{once}(X,+,1) atomic_inc_return_acquire(X) __atomic_op_return{acquire}(X,+,1) @@ -117,3 +135,6 @@ atomic_sub_and_test(V,X) __atomic_op_return{mb}(X,-,V) = =3D=3D 0 atomic_dec_and_test(X) __atomic_op_return{mb}(X,-,1) =3D=3D 0 atomic_inc_and_test(X) __atomic_op_return{mb}(X,+,1) =3D=3D 0 atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0 +atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0 +atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0 +atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0 --=20 2.40.1 From nobody Tue Dec 16 11:06:41 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 850222080CC; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; cv=none; b=TNV/Hiirx7WqS01Z6t4uXSrPjk/HqiPE05pHtrDQWZb1K5Xhkp7DaSk8BlR5lf+jq0i4W3eUaFTdrYY1xpPyXUEhr/Y7O9/Lrm5q3s7ZM45NGL4n5Y3CYwBvKDuHqlKdLWY17SMN83+N2QBst+gLuqIQ3cXIbve6ntpvrpMc/hA= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; c=relaxed/simple; bh=21ND8h3aXwqP4GPXt1SePJHjRlQNFlNVkqExdK3K1F0=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=E6O6kN0RLN8PfcXKep1RyjfJiQDPcueX7zjmxwJHMelFHqPYZq+LfhreWjsktT98DaI7R61Y3N79lKtsUwJJs9cZOU0gfu92g19ozIq2xdEAwJ+E05TFMAMCCScap4RIhjKYu0EClrR9o65Iyr7I9L1mDbFlNAuGfC7jzLb+eyE= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=VOi6qfOF; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="VOi6qfOF" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 04429C4CEDD; Thu, 20 Feb 2025 16:14:04 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1740068045; bh=21ND8h3aXwqP4GPXt1SePJHjRlQNFlNVkqExdK3K1F0=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=VOi6qfOFDxyt4RiKck5m0cbAN4YyCEcXk0Dq99Nvh3HkREbKIZp+vpxFze5Woc0z9 EP0/rZL3ou1HejUF0ew497eLDSEt94cCuao4Ilz9PwL9/cfCjGf1KemBADkIgzurvQ kZdSM3G66az9fKE5vbYbHu9pBuxJMRUlHMomL09XO9y9qA9eYs0lxX9SUUn+5gmK+p 49XMflhLA2ud60wKyXr6PuEqaChE0aE+mIySkStOc6qifUQNiSWxmxdofNmuIOcd5O vIFIMumwRjssuimaHYc80CULKSon8FfszG9k94d5c8GnyehLVW3HRHsvQCmCcGmiY8 9bxtrFvbDDaiA== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id 9E5BACE0B9E; Thu, 20 Feb 2025 08:14:04 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, lkmm@lists.linux.dev, kernel-team@meta.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, Puranjay Mohan , "Paul E . McKenney" , Daniel Lustig , Joel Fernandes Subject: [PATCH memory-model 2/7] tools/memory-model: Add atomic_andnot() with its variants Date: Thu, 20 Feb 2025 08:13:58 -0800 Message-Id: <20250220161403.800831-2-paulmck@kernel.org> X-Mailer: git-send-email 2.40.1 In-Reply-To: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> References: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Puranjay Mohan Pull-855[1] added the support of atomic_andnot() to the herd tool. Use this to add the implementation in the LKMM. All of the ordering variants are also added. Here is a small litmus-test that uses this operation: C andnot { atomic_t u =3D ATOMIC_INIT(7); } P0(atomic_t *u) { r0 =3D atomic_fetch_andnot(3, u); r1 =3D READ_ONCE(*u); } exists (0:r0=3D7 /\ 0:r1=3D4) Test andnot Allowed States 1 0:r0=3D7; 0:r1=3D4; Ok Witnesses Positive: 1 Negative: 0 Condition exists (0:r0=3D7 /\ 0:r1=3D4) Observation andnot Always 1 0 Time andnot 0.00 Hash=3D78f011a0b5a0c65fa1cf106fcd62c845 [1] https://github.com/herd/herdtools7/pull/855 Signed-off-by: Puranjay Mohan Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney Cc: Alan Stern Cc: Will Deacon Cc: Peter Zijlstra Cc: Boqun Feng Cc: Nicholas Piggin Cc: David Howells Cc: Jade Alglave Cc: Luc Maranget Cc: Akira Yokosawa Cc: Daniel Lustig Cc: Joel Fernandes Cc: --- tools/memory-model/linux-kernel.def | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux= -kernel.def index d1f11930ec512..a12b96c547b7a 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -70,6 +70,7 @@ 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); } =20 atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V) atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V) @@ -138,3 +139,8 @@ atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) = < 0 atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0 atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0 atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0 + +atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V) +atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V) +atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V) +atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V) --=20 2.40.1 From nobody Tue Dec 16 11:06:41 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 84F6E2066C1; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; cv=none; b=UNtF9rDy7Y60ng0os4IQjqU2H0aDRvzygzpCXNdwys7MMXYSBMGeaA2yf82BNGHLxW1loXf/Bf2k+nuwH0yl+vp0wyd9Yz7J7Vv9mKCUoDtWO2euMpJaoAOzYNsb++yUIc83gYia7wKQbhfz3ViVkk60cRmLXiUwCRYyOZWtqxs= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; c=relaxed/simple; bh=BJSdjddDDDak8tUwLAztoLXgRW0wiWScQgn5daVIRSY=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=tbeKm1bgRk8StSTHpVg9caqIh1kpvTOMB8XlKb65roM8v9cJxKiilkERSH9cFetZdWScgzO53efh5MCI24PI9VLbGWW+AJ/5aq4bNiEHItY/6HcsSYdX67CAYEgpoMsmRn7Q9O1yPtRL7zKuIGQgTsorgOo/4MVWKOGWqLoG9ZA= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=kvDWkGig; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="kvDWkGig" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 0EE4AC4CEE2; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1740068045; bh=BJSdjddDDDak8tUwLAztoLXgRW0wiWScQgn5daVIRSY=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=kvDWkGigx4owex//4esDzuokt/gCIoPWd+QMZ6lDXKZTWjm4qMtjiEKZ/9r4FQVg2 NuUx4F5dBCc3YXFjoIgqtsA52zdlg6JKEcI6PsSINEhqigJ0mraEw8uksgvvfZ7nRu 5qxgUq4Hwx6SFAQ28LXN70FIzVcm9gloG6I5QpOggkCjV+wWcZ7Ld2Za6Uj6z/dMdJ 3dq4sGc2iedKr9zdT2wEdA1PzgnknTD17v+lHsPf/CxpTRfq2oCbcE/SLLSSmnZMdj EHuydveBP+gt/o6SuQnP7fg8AwsHpV4K3tTX00dWC2g7vubgkXGabCFwOdeeqTEOVS JLn82N8pzeE0w== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id A1787CE0BA2; Thu, 20 Feb 2025 08:14:04 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, lkmm@lists.linux.dev, kernel-team@meta.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, Jonas Oberhauser , "Paul E . McKenney" Subject: [PATCH memory-model 3/7] tools/memory-model: Legitimize current use of tags in LKMM macros Date: Thu, 20 Feb 2025 08:13:59 -0800 Message-Id: <20250220161403.800831-3-paulmck@kernel.org> X-Mailer: git-send-email 2.40.1 In-Reply-To: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> References: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Jonas Oberhauser The current macros in linux-kernel.def reference instructions such as __xchg{mb} or __cmpxchg{acquire}, which are invalid combinations of tags and instructions according to the declarations in linux-kernel.bell. This works with current herd7 because herd7 removes these tags anyways and does not actually enforce validity of combinations at all. If a future herd7 version no longer applies these hardcoded transformations, then all currently invalid combinations will actually appear on some instruction. We therefore adjust the declarations to make the resulting combinations valid, by adding the 'mb tag to the set of Accesses and allowing all Accesses to appear on all read, write, and RMW instructions. Signed-off-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Tested-by: Boqun Feng --- tools/memory-model/linux-kernel.bell | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linu= x-kernel.bell index ce068700939c5..dba6b5b6dee01 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -16,10 +16,11 @@ enum Accesses =3D 'once (*READ_ONCE,WRITE_ONCE*) || 'release (*smp_store_release*) || 'acquire (*smp_load_acquire*) || - 'noreturn (* R of non-return RMW *) -instructions R[{'once,'acquire,'noreturn}] -instructions W[{'once,'release}] -instructions RMW[{'once,'acquire,'release}] + 'noreturn (* R of non-return RMW *) || + 'mb (*xchg(),cmpxchg(),...*) +instructions R[Accesses] +instructions W[Accesses] +instructions RMW[Accesses] =20 enum Barriers =3D 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || --=20 2.40.1 From nobody Tue Dec 16 11:06:41 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 84FC8206F0C; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; cv=none; b=kzKRlvI20vVM6GQG6DDwseIIdFTzbyKVZI6vYAUScEXRt9gkFHm2GoSAMJCTnBpzPe7DbzzfLrRYrikYpekVaqKDhfR86WKywkTYg7CH67ETSK2e/Ub+uussx9yFpGYrjkI+Ur4RGtXV0e/+gl7E0UDlCfieL+QiiG2/lnieG7E= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; c=relaxed/simple; bh=+b8V+UTHefEjZ4Z9F9NJkPT29CpP1j9+D+uE5/v1wfo=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=T+rdff9F+X2tgJd25EItUIHu62/WRewImBuc8WIOgHfgQbXXVCoxJnaVnQdSSGxP8BsRadNC7E+20valSaMKwWjdUgjbIVXnH9eqVh4FNc4goDkq2gtpTVLtaFnZwsVN2KnSfPc3oJ7thFW7FTUvGzJ+CTI4UF3XKuOl8CZ5T4w= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=Z3ad2uzf; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="Z3ad2uzf" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 16CFEC4CEE9; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1740068045; bh=+b8V+UTHefEjZ4Z9F9NJkPT29CpP1j9+D+uE5/v1wfo=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=Z3ad2uzfSsY+KEGFG5Kor13n706xTsF8vHl+cu7ig+UxnUhS/xlSCM4ixY1ZRxtjt 2yp7dn+/+N7rN+aL4U0eDQt9Fgx30tIWq1i/yD0laqhj/J8T9fw9Tg31yHMzbDLLWg X49r6m5+hppaHcEvkKODgv92ak4BMeSaXwFazp3PXx7/js3wj+spjieo8SM96elRbv V9P5n+BySjRTcuAIIS41CNo4wm7fW60aFWcRlAXTwKQ2BTb1cyWCzfQLYaJWSgUHVe mmeC/McNTPIl50uBbvR7c1V2bTP67ms04HNji4OXg5L+uYD99KXGWVlH0bvUplt0Ba UgF5STB/hrmPQ== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id A54C1CE0C4A; Thu, 20 Feb 2025 08:14:04 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, lkmm@lists.linux.dev, kernel-team@meta.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, Jonas Oberhauser , "Paul E . McKenney" Subject: [PATCH memory-model 4/7] tools/memory-model: Define applicable tags on operation in tools/... Date: Thu, 20 Feb 2025 08:14:00 -0800 Message-Id: <20250220161403.800831-4-paulmck@kernel.org> X-Mailer: git-send-email 2.40.1 In-Reply-To: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> References: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Jonas Oberhauser Herd7 transforms reads, writes, and read-modify-writes by eliminating 'acquire tags from writes, 'release tags from reads, and 'acquire, 'release, and 'mb tags from failed read-modify-writes. We emulate this behavior by redefining Acquire, Release, and Mb sets in linux-kernel.bell to explicitly exclude those combinations. Herd7 furthermore adds 'noreturn tag to certain reads. Currently herd7 does not allow specifying the 'noreturn tag manually, but such manual declaration (e.g., through a syntax __atomic_op{noreturn}) would add invalid 'noreturn tags to writes; in preparation, we already also exclude this combination. Signed-off-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Tested-by: Boqun Feng --- tools/memory-model/linux-kernel.bell | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linu= x-kernel.bell index dba6b5b6dee01..7c9ae48b94377 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -36,6 +36,17 @@ enum Barriers =3D 'wmb (*smp_wmb*) || 'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*) instructions F[Barriers] =20 + +(* + * Filter out syntactic annotations that do not provide the corresponding + * semantic ordering, such as Acquire on a store or Mb on a failed RMW. + *) +let FailedRMW =3D RMW \ (domain(rmw) | range(rmw)) +let Acquire =3D Acquire \ W \ FailedRMW +let Release =3D Release \ R \ FailedRMW +let Mb =3D Mb \ FailedRMW +let Noreturn =3D Noreturn \ W + (* SRCU *) enum SRCU =3D 'srcu-lock || 'srcu-unlock || 'sync-srcu instructions SRCU[SRCU] --=20 2.40.1 From nobody Tue Dec 16 11:06:41 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 84F0F205E1A; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; cv=none; b=ILGcD17Rvbb4Qs8Uy4ew65/Jej9hcw01+UtYSMDRVusLf/bFZA935vAAOkW/S4DGiW6d6N0GiZgmvAkJf9vWC8hkZYf1Fm37eeHXWvZVjggpZkiUgQ0402MeuthR9dMn6Km80lP7khwSyMN97ufoIhY0AFGGIV6SqRMgEcmbwtk= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; c=relaxed/simple; bh=WmSxWReFRSxg3AIpXyHvnAtwkV29bRIzKRwaPkY52Og=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=XbEfI7PhaVGrNfdE/sqqvjSPIGIHXkq9kkNO0QNWYCKuIt5JvKQDdHo9PDB6ljcGJIuLB87KKkFF9uKChITXD21sSE68TGmtUTf1gT3MonwdQhSo/35CaemXplJIPARfhaM5f0PFMw7YkjOqOHZA3VsbbrhymltC01bPhRqUlj4= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=gZWU+yhr; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="gZWU+yhr" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 27FD5C4CEEC; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1740068045; bh=WmSxWReFRSxg3AIpXyHvnAtwkV29bRIzKRwaPkY52Og=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=gZWU+yhrnnxWMvYCCs273LOHURrt8hQyzlnKBGN+wPxu5MUgxLfkmaA5uE56kDsfe MY/XrJYABDYExWTf10OE2qVpvcOUjv5aXvZBxwsl+MO0JxGTu/rU7J9pSNeO1p+9lb DRwbRn2+c4HxxFDTPdHcIdP1thvx1JYaq1P+O8T+0V8rEfizNH7g4hm2Cseqauu+Rw wPk+syUd7pxLdmSU5mU6NPD84gZ//fwdR4jvFUR4xJG5sSgWMAyeuz0UtKsNU5/34C l0J2owammTBx37a2ftwcLx3P1YIVdvkVuQhX1P8P1YwuOWs2ptzixUEik6H5lJkNf5 wDmBf9KPGFHPA== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id A928ACE0C90; Thu, 20 Feb 2025 08:14:04 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, lkmm@lists.linux.dev, kernel-team@meta.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, Jonas Oberhauser , Viktor Vafeiadis , "Paul E . McKenney" Subject: [PATCH memory-model 5/7] tools/memory-model: Define effect of Mb tags on RMWs in tools/... Date: Thu, 20 Feb 2025 08:14:01 -0800 Message-Id: <20250220161403.800831-5-paulmck@kernel.org> X-Mailer: git-send-email 2.40.1 In-Reply-To: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> References: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Jonas Oberhauser Herd7 transforms successful RMW with Mb tags by inserting smp_mb() fences around them. We emulate this by considering imaginary po-edges before the RMW read and before the RMW write, and extending the smp_mb() ordering rule, which currently only applies to real po edges that would be found around a really inserted smp_mb(), also to cases of the only imagined po edges. Reported-by: Viktor Vafeiadis Suggested-by: Alan Stern Signed-off-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Tested-by: Boqun Feng --- tools/memory-model/linux-kernel.cat | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux= -kernel.cat index adf3c4f412296..d7e7bf13c831b 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -34,6 +34,16 @@ let R4rmb =3D R \ Noreturn (* Reads for which rmb works = *) let rmb =3D [R4rmb] ; fencerel(Rmb) ; [R4rmb] let wmb =3D [W] ; fencerel(Wmb) ; [W] let mb =3D ([M] ; fencerel(Mb) ; [M]) | + (* + * full-barrier RMWs (successful cmpxchg(), xchg(), etc.) act as + * though there were enclosed by smp_mb(). + * The effect of these virtual smp_mb() is formalized by adding + * Mb tags to the read and write of the operation, and providing + * the same ordering as though there were additional po edges + * between the Mb tag and the read resp. write. + *) + ([M] ; po ; [Mb & R]) | + ([Mb & W] ; po ; [M]) | ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | --=20 2.40.1 From nobody Tue Dec 16 11:06:41 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id E1853211292; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068046; cv=none; b=rd0irdzcPMmqJmXu0bPEWik3ewelOBARXI3j34mn/Ow0sS5CHA+5cyESh1BMH7g7svzqdSUHdfRMSAzeBEmB/DzL16bQQT1ukxY8qoNh3JKVxDspgnzpiBdVrG4XdVwcnXaudLEv+I1Cac+DdtapEqR912mhlSR7ECLYGZLsDIw= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068046; c=relaxed/simple; bh=TsvXbj8pt31jepIWyXRjFgkBXvYwvZCcef75PEq5V2U=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=hG9ZKzBAunYhW7AtJW/D5dHntEZ5TanB4XBpKpOmOTcunY3j2UDzH+PsjQ58ed+XjbF4kqAJVohynicaQJ7/81vQGDyVpLFUrBGkfrVXOXZBAMFu65L3hAe92L9zPAv4z0iSCBGuBtU2UNkC/Ls9WnWeUn61OrA9UAtPaqAMYl8= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=WlBavuS7; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="WlBavuS7" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 5A7F8C4CEF4; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1740068045; bh=TsvXbj8pt31jepIWyXRjFgkBXvYwvZCcef75PEq5V2U=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=WlBavuS7Pm6ZbqBJFTktu4nmnnkmz+raAO0fuJW4NlW1+olnLq444kyKFyiOpLeVn ask3aK6su4JZlVdgpDNGZg3DZBa0XuzGwB+v+xuSr1B57Ji5KwDQCWkvv/uDR9xEf4 tcRt1Lb1iX3fk6wRlW6Nb1n2rRRr115ZRoKeEyMxH3Yzd19oQUooY23cENPWJV7Qkl xhkionvIAl2QO6NY/aZo3b116xEuG1Fi6uOwIqRbBGdYunZ3VmMwRaJ+ysNflJPKMQ h6kC08r0C2rjoSR3uD7VtTLNT9PO9HTHLdc8LpReVfI8akMSDowrmKlmjR6V+jpbng hFsFGzWuMpd+A== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id ACFEFCE0D8A; Thu, 20 Feb 2025 08:14:04 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, lkmm@lists.linux.dev, kernel-team@meta.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, Jonas Oberhauser , Hernan Ponce de Leon , "Paul E . McKenney" Subject: [PATCH memory-model 6/7] tools/memory-model: Switch to softcoded herd7 tags Date: Thu, 20 Feb 2025 08:14:02 -0800 Message-Id: <20250220161403.800831-6-paulmck@kernel.org> X-Mailer: git-send-email 2.40.1 In-Reply-To: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> References: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Jonas Oberhauser A new version of herd7 provides a -lkmmv2 switch which overrides the old he= rd7 behavior of simply ignoring any softcoded tags in the .def and .bell files.= We port LKMM to this version of herd7 by providing the switch in linux-kernel.= cfg and reporting an error if the LKMM is used without this switch. To preserve the semantics of LKMM, we also softcode the Noreturn tag on ato= mic RMW which do not return a value and define atomic_add_unless with an Mb tag= in linux-kernel.def. We update the herd-representation.txt accordingly and clarify some of the resulting combinations. Signed-off-by: Hernan Ponce de Leon Signed-off-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Reviewed-by: Boqun Feng Tested-by: Boqun Feng Tested-by: Akira Yokosawa # herdtools7.7.58 --- .../Documentation/herd-representation.txt | 27 ++++++++++--------- tools/memory-model/README | 2 +- tools/memory-model/linux-kernel.bell | 3 +++ tools/memory-model/linux-kernel.cfg | 1 + tools/memory-model/linux-kernel.def | 18 +++++++------ 5 files changed, 30 insertions(+), 21 deletions(-) diff --git a/tools/memory-model/Documentation/herd-representation.txt b/too= ls/memory-model/Documentation/herd-representation.txt index ed988906f2b71..7ae1ff3d3769e 100644 --- a/tools/memory-model/Documentation/herd-representation.txt +++ b/tools/memory-model/Documentation/herd-representation.txt @@ -18,6 +18,11 @@ # # By convention, a blank line in a cell means "same as the preceding line". # +# Note that the syntactic representation does not always match the sets and +# relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell= and +# lock.cat. For example, the po link between LKR and LKW is upgraded to an= rmw +# link, and W[acquire] are not included in the Acquire set. +# # Disclaimer. The table includes representations of "add" and "and" opera= tions; # corresponding/identical representations of "sub", "inc", "dec" and "or",= "xor", # "andnot" operations are omitted. @@ -60,14 +65,13 @@ ----------------------------------------------------------------------= -------- | RMW ops w/o return value | = | ----------------------------------------------------------------------= -------- - | atomic_add | R*[noreturn] ->rmw W*[once] = | + | atomic_add | R*[noreturn] ->rmw W*[noreturn] = | | atomic_and | = | | spin_lock | LKR ->po LKW = | ----------------------------------------------------------------------= -------- | RMW ops w/ return value | = | ----------------------------------------------------------------------= -------- - | atomic_add_return | F[mb] ->po R*[once] = | - | | ->rmw W*[once] ->po F[mb] = | + | atomic_add_return | R*[mb] ->rmw W*[mb] = | | atomic_fetch_add | = | | atomic_fetch_and | = | | atomic_xchg | = | @@ -79,13 +83,13 @@ | atomic_xchg_relaxed | = | | xchg_relaxed | = | | atomic_add_negative_relaxed | = | - | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] = | + | atomic_add_return_acquire | R*[acquire] ->rmw W*[acquire] = | | atomic_fetch_add_acquire | = | | atomic_fetch_and_acquire | = | | atomic_xchg_acquire | = | | xchg_acquire | = | | atomic_add_negative_acquire | = | - | atomic_add_return_release | R*[once] ->rmw W*[release] = | + | atomic_add_return_release | R*[release] ->rmw W*[release] = | | atomic_fetch_add_release | = | | atomic_fetch_and_release | = | | atomic_xchg_release | = | @@ -94,17 +98,16 @@ ----------------------------------------------------------------------= -------- | Conditional RMW ops | = | ----------------------------------------------------------------------= -------- - | atomic_cmpxchg | On success: F[mb] ->po R*[once] = | - | | ->rmw W*[once] ->po= F[mb] | - | | On failure: R*[once] = | + | atomic_cmpxchg | On success: R*[mb] ->rmw W*[mb] = | + | | On failure: R*[mb] = | | cmpxchg | = | | atomic_add_unless | = | | atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once]= | | | On failure: R*[once] = | - | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[on= ce] | - | | On failure: R*[once] = | - | atomic_cmpxchg_release | On success: R*[once] ->rmw W*[relea= se] | - | | On failure: R*[once] = | + | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[ac= quire] | + | | On failure: R*[acquire] = | + | atomic_cmpxchg_release | On success: R*[release] ->rmw W*[re= lease] | + | | On failure: R*[release] = | | spin_trylock | On success: LKR ->po LKW = | | | On failure: LF = | ----------------------------------------------------------------------= -------- diff --git a/tools/memory-model/README b/tools/memory-model/README index dab38904206a0..59bc15edeb8ab 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -20,7 +20,7 @@ that litmus test to be exercised within the Linux kernel. REQUIREMENTS =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D =20 -Version 7.52 or higher of the "herd7" and "klitmus7" tools must be +Version 7.58 or higher of the "herd7" and "klitmus7" tools must be downloaded separately: =20 https://github.com/herd/herdtools7 diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linu= x-kernel.bell index 7c9ae48b94377..8ae47545df978 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -94,3 +94,6 @@ let carry-dep =3D (data ; [~ Srcu-unlock] ; rfi)* let addr =3D carry-dep ; addr let ctrl =3D carry-dep ; ctrl let data =3D carry-dep ; data + +flag ~empty (if "lkmmv2" then 0 else _) + as this-model-requires-variant-higher-than-lkmmv1 diff --git a/tools/memory-model/linux-kernel.cfg b/tools/memory-model/linux= -kernel.cfg index 3c8098e99f41d..69b04f3aad737 100644 --- a/tools/memory-model/linux-kernel.cfg +++ b/tools/memory-model/linux-kernel.cfg @@ -1,6 +1,7 @@ macros linux-kernel.def bell linux-kernel.bell model linux-kernel.cat +variant lkmmv2 graph columns squished true showevents noregs diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux= -kernel.def index a12b96c547b7a..d7279a357cba0 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -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); } =20 -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); } =20 atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V) atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V) @@ -144,3 +144,5 @@ atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V) atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V) atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V) atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V) + +atomic_add_unless(X,V,W) __atomic_add_unless{mb}(X,V,W) --=20 2.40.1 From nobody Tue Dec 16 11:06:41 2025 Received: from smtp.kernel.org (aws-us-west-2-korg-mail-1.web.codeaurora.org [10.30.226.201]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id A4C9F1D63F9; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=10.30.226.201 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; cv=none; b=DZ2Q9JZWxuwwdMHq9WDxCejvcVOfSxf1R4EZr4/kqR0yuUSOEun3RJKaACPH8Mn5P1Tsh2wdcgE55YTHa+PAdp67+LNkH4TCjED+DC8ZJkXxMtdb/O41NcTSoMHVClxrBmnduM/FHKzlrQIFPE7gyyPa5laRZPdGk0Vm9Htig5g= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1740068045; c=relaxed/simple; bh=Ir6n/IUN5eZ6fqNje+Lapg2qN2Ln3avRnjBN51w/tq8=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=WkrKh0dFcJtkWGI2m/KWd0sATXFudVSugZ9f8W75j1gZMkhX44UFLu7MECRhOO0ia7qxnI7xS2imbfMga0KhkFlCzV4xy+kTIbaetgmTmw9msVjeUmHfXU6Vm61RenHt38Kn9BmeWEDjzDkRHZHRDuwaIas9Gyq73YvcnD7GKkE= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b=JMmjgDM6; arc=none smtp.client-ip=10.30.226.201 Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.b="JMmjgDM6" Received: by smtp.kernel.org (Postfix) with ESMTPSA id 5AB0FC4CEF5; Thu, 20 Feb 2025 16:14:05 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1740068045; bh=Ir6n/IUN5eZ6fqNje+Lapg2qN2Ln3avRnjBN51w/tq8=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=JMmjgDM60Ij6GucPXAVvJmvbHP0uyAdllzMMDkdRtACxm54F+8VV1Blx1Gr5ioQOC o5K/n33zHwg/KFIMSeoIXY4mrqv8fQr2y86rdISlgs00fwXCAbIa/FJkO276qTld1N CuiIZCN3oNv/nMR3eeFEa04atXtXbLqSFjVI7DdFAd1n7P7cAp6FHpGJSi9MlRBKV/ 7Ig/2AYfV0UVztBjaMdA/omccH7D03ENPIe2oCqnmyqILI+5Jy47uaWUUFjXHPb6UD h/A0uwPD7EsfdfH24drLm81RA/8i958bvKUVgCCr6i/7viri7Py28UhHeIUMs7JToz osAOL3tKg5INg== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id B05C1CE0D99; Thu, 20 Feb 2025 08:14:04 -0800 (PST) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, lkmm@lists.linux.dev, kernel-team@meta.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, Jonas Oberhauser , "Paul E . McKenney" Subject: [PATCH memory-model 7/7] tools/memory-model: Distinguish between syntactic and semantic tags Date: Thu, 20 Feb 2025 08:14:03 -0800 Message-Id: <20250220161403.800831-7-paulmck@kernel.org> X-Mailer: git-send-email 2.40.1 In-Reply-To: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> References: <8cfb51e3-9726-4285-b8ca-0d0abcacb07e@paulmck-laptop> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" From: Jonas Oberhauser Not all annotated accesses provide the semantics their syntactic tags would imply. For example, an 'acquire tag on a write does not imply that the write is finally in the Acquire set and provides acquire ordering. To distinguish in those cases between the syntactic tags and actual sets, we capitalize the former, so 'ACQUIRE tags may be present on both reads and writes, but only reads will appear in the Acquire set. For tags where the two concepts are the same we do not use specific capitalization to make this distinction. Reported-by: Boqun Feng Signed-off-by: Jonas Oberhauser Reviewed-by: Boqun Feng Tested-by: Boqun Feng Signed-off-by: Paul E. McKenney --- .../Documentation/herd-representation.txt | 44 ++-- tools/memory-model/linux-kernel.bell | 22 +- tools/memory-model/linux-kernel.def | 198 +++++++++--------- 3 files changed, 132 insertions(+), 132 deletions(-) diff --git a/tools/memory-model/Documentation/herd-representation.txt b/too= ls/memory-model/Documentation/herd-representation.txt index 7ae1ff3d3769e..4e19b4f2a476e 100644 --- a/tools/memory-model/Documentation/herd-representation.txt +++ b/tools/memory-model/Documentation/herd-representation.txt @@ -21,7 +21,7 @@ # Note that the syntactic representation does not always match the sets and # relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell= and # lock.cat. For example, the po link between LKR and LKW is upgraded to an= rmw -# link, and W[acquire] are not included in the Acquire set. +# link, and W[ACQUIRE] are not included in the Acquire set. # # Disclaimer. The table includes representations of "add" and "and" opera= tions; # corresponding/identical representations of "sub", "inc", "dec" and "or",= "xor", @@ -32,16 +32,16 @@ ----------------------------------------------------------------------= -------- | Non-RMW ops | = | ----------------------------------------------------------------------= -------- - | READ_ONCE | R[once] = | + | READ_ONCE | R[ONCE] = | | atomic_read | = | - | WRITE_ONCE | W[once] = | + | WRITE_ONCE | W[ONCE] = | | atomic_set | = | - | smp_load_acquire | R[acquire] = | + | smp_load_acquire | R[ACQUIRE] = | | atomic_read_acquire | = | - | smp_store_release | W[release] = | + | smp_store_release | W[RELEASE] = | | atomic_set_release | = | - | smp_store_mb | W[once] ->po F[mb] = | - | smp_mb | F[mb] = | + | smp_store_mb | W[ONCE] ->po F[MB] = | + | smp_mb | F[MB] = | | smp_rmb | F[rmb] = | | smp_wmb | F[wmb] = | | smp_mb__before_atomic | F[before-atomic] = | @@ -54,8 +54,8 @@ | rcu_read_lock | F[rcu-lock] = | | rcu_read_unlock | F[rcu-unlock] = | | synchronize_rcu | F[sync-rcu] = | - | rcu_dereference | R[once] = | - | rcu_assign_pointer | W[release] = | + | rcu_dereference | R[ONCE] = | + | rcu_assign_pointer | W[RELEASE] = | | srcu_read_lock | R[srcu-lock] = | | srcu_down_read | = | | srcu_read_unlock | W[srcu-unlock] = | @@ -65,31 +65,31 @@ ----------------------------------------------------------------------= -------- | RMW ops w/o return value | = | ----------------------------------------------------------------------= -------- - | atomic_add | R*[noreturn] ->rmw W*[noreturn] = | + | atomic_add | R*[NORETURN] ->rmw W*[NORETURN] = | | atomic_and | = | | spin_lock | LKR ->po LKW = | ----------------------------------------------------------------------= -------- | RMW ops w/ return value | = | ----------------------------------------------------------------------= -------- - | atomic_add_return | R*[mb] ->rmw W*[mb] = | + | atomic_add_return | R*[MB] ->rmw W*[MB] = | | atomic_fetch_add | = | | atomic_fetch_and | = | | atomic_xchg | = | | xchg | = | | atomic_add_negative | = | - | atomic_add_return_relaxed | R*[once] ->rmw W*[once] = | + | atomic_add_return_relaxed | R*[ONCE] ->rmw W*[ONCE] = | | atomic_fetch_add_relaxed | = | | atomic_fetch_and_relaxed | = | | atomic_xchg_relaxed | = | | xchg_relaxed | = | | atomic_add_negative_relaxed | = | - | atomic_add_return_acquire | R*[acquire] ->rmw W*[acquire] = | + | atomic_add_return_acquire | R*[ACQUIRE] ->rmw W*[ACQUIRE] = | | atomic_fetch_add_acquire | = | | atomic_fetch_and_acquire | = | | atomic_xchg_acquire | = | | xchg_acquire | = | | atomic_add_negative_acquire | = | - | atomic_add_return_release | R*[release] ->rmw W*[release] = | + | atomic_add_return_release | R*[RELEASE] ->rmw W*[RELEASE] = | | atomic_fetch_add_release | = | | atomic_fetch_and_release | = | | atomic_xchg_release | = | @@ -98,16 +98,16 @@ ----------------------------------------------------------------------= -------- | Conditional RMW ops | = | ----------------------------------------------------------------------= -------- - | atomic_cmpxchg | On success: R*[mb] ->rmw W*[mb] = | - | | On failure: R*[mb] = | + | atomic_cmpxchg | On success: R*[MB] ->rmw W*[MB] = | + | | On failure: R*[MB] = | | cmpxchg | = | | atomic_add_unless | = | - | atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once]= | - | | On failure: R*[once] = | - | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[ac= quire] | - | | On failure: R*[acquire] = | - | atomic_cmpxchg_release | On success: R*[release] ->rmw W*[re= lease] | - | | On failure: R*[release] = | + | atomic_cmpxchg_relaxed | On success: R*[ONCE] ->rmw W*[ONCE]= | + | | On failure: R*[ONCE] = | + | atomic_cmpxchg_acquire | On success: R*[ACQUIRE] ->rmw W*[AC= QUIRE] | + | | On failure: R*[ACQUIRE] = | + | atomic_cmpxchg_release | On success: R*[RELEASE] ->rmw W*[RE= LEASE] | + | | On failure: R*[RELEASE] = | | spin_trylock | On success: LKR ->po LKW = | | | On failure: LF = | ----------------------------------------------------------------------= -------- diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linu= x-kernel.bell index 8ae47545df978..fe65998002b99 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -13,18 +13,18 @@ =20 "Linux-kernel memory consistency model" =20 -enum Accesses =3D 'once (*READ_ONCE,WRITE_ONCE*) || - 'release (*smp_store_release*) || - 'acquire (*smp_load_acquire*) || - 'noreturn (* R of non-return RMW *) || - 'mb (*xchg(),cmpxchg(),...*) +enum Accesses =3D 'ONCE (*READ_ONCE,WRITE_ONCE*) || + 'RELEASE (*smp_store_release*) || + 'ACQUIRE (*smp_load_acquire*) || + 'NORETURN (* R of non-return RMW *) || + 'MB (*xchg(),cmpxchg(),...*) instructions R[Accesses] instructions W[Accesses] instructions RMW[Accesses] =20 enum Barriers =3D 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || - 'mb (*smp_mb*) || + 'MB (*smp_mb*) || 'barrier (*barrier*) || 'rcu-lock (*rcu_read_lock*) || 'rcu-unlock (*rcu_read_unlock*) || @@ -42,10 +42,10 @@ instructions F[Barriers] * semantic ordering, such as Acquire on a store or Mb on a failed RMW. *) let FailedRMW =3D RMW \ (domain(rmw) | range(rmw)) -let Acquire =3D Acquire \ W \ FailedRMW -let Release =3D Release \ R \ FailedRMW -let Mb =3D Mb \ FailedRMW -let Noreturn =3D Noreturn \ W +let Acquire =3D ACQUIRE \ W \ FailedRMW +let Release =3D RELEASE \ R \ FailedRMW +let Mb =3D MB \ FailedRMW +let Noreturn =3D NORETURN \ W =20 (* SRCU *) enum SRCU =3D 'srcu-lock || 'srcu-unlock || 'sync-srcu @@ -85,7 +85,7 @@ flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid= -sleep flag ~empty different-values(srcu-rscs) as srcu-bad-value-match =20 (* Compute marked and plain memory accesses *) -let Marked =3D (~M) | IW | Once | Release | Acquire | domain(rmw) | range(= rmw) | +let Marked =3D (~M) | IW | ONCE | RELEASE | ACQUIRE | MB | RMW | LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock let Plain =3D M \ Marked =20 diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux= -kernel.def index d7279a357cba0..49e402782e49c 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -6,18 +6,18 @@ // which appeared in ASPLOS 2018. =20 // ONCE -READ_ONCE(X) __load{once}(X) -WRITE_ONCE(X,V) { __store{once}(X,V); } +READ_ONCE(X) __load{ONCE}(X) +WRITE_ONCE(X,V) { __store{ONCE}(X,V); } =20 // Release Acquire and friends -smp_store_release(X,V) { __store{release}(*X,V); } -smp_load_acquire(X) __load{acquire}(*X) -rcu_assign_pointer(X,V) { __store{release}(X,V); } -rcu_dereference(X) __load{once}(X) -smp_store_mb(X,V) { __store{once}(X,V); __fence{mb}; } +smp_store_release(X,V) { __store{RELEASE}(*X,V); } +smp_load_acquire(X) __load{ACQUIRE}(*X) +rcu_assign_pointer(X,V) { __store{RELEASE}(X,V); } +rcu_dereference(X) __load{ONCE}(X) +smp_store_mb(X,V) { __store{ONCE}(X,V); __fence{MB}; } =20 // Fences -smp_mb() { __fence{mb}; } +smp_mb() { __fence{MB}; } smp_rmb() { __fence{rmb}; } smp_wmb() { __fence{wmb}; } smp_mb__before_atomic() { __fence{before-atomic}; } @@ -28,14 +28,14 @@ smp_mb__after_srcu_read_unlock() { __fence{after-srcu-r= ead-unlock}; } barrier() { __fence{barrier}; } =20 // Exchange -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) +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) =20 // Spinlocks spin_lock(X) { __lock(X); } @@ -63,86 +63,86 @@ 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); } =20 -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) -atomic_add_return_acquire(V,X) __atomic_op_return{acquire}(X,+,V) -atomic_add_return_release(V,X) __atomic_op_return{release}(X,+,V) -atomic_fetch_add(V,X) __atomic_fetch_op{mb}(X,+,V) -atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{once}(X,+,V) -atomic_fetch_add_acquire(V,X) __atomic_fetch_op{acquire}(X,+,V) -atomic_fetch_add_release(V,X) __atomic_fetch_op{release}(X,+,V) - -atomic_fetch_and(V,X) __atomic_fetch_op{mb}(X,&,V) -atomic_fetch_and_relaxed(V,X) __atomic_fetch_op{once}(X,&,V) -atomic_fetch_and_acquire(V,X) __atomic_fetch_op{acquire}(X,&,V) -atomic_fetch_and_release(V,X) __atomic_fetch_op{release}(X,&,V) - -atomic_fetch_or(V,X) __atomic_fetch_op{mb}(X,|,V) -atomic_fetch_or_relaxed(V,X) __atomic_fetch_op{once}(X,|,V) -atomic_fetch_or_acquire(V,X) __atomic_fetch_op{acquire}(X,|,V) -atomic_fetch_or_release(V,X) __atomic_fetch_op{release}(X,|,V) - -atomic_fetch_xor(V,X) __atomic_fetch_op{mb}(X,^,V) -atomic_fetch_xor_relaxed(V,X) __atomic_fetch_op{once}(X,^,V) -atomic_fetch_xor_acquire(V,X) __atomic_fetch_op{acquire}(X,^,V) -atomic_fetch_xor_release(V,X) __atomic_fetch_op{release}(X,^,V) - -atomic_inc_return(X) __atomic_op_return{mb}(X,+,1) -atomic_inc_return_relaxed(X) __atomic_op_return{once}(X,+,1) -atomic_inc_return_acquire(X) __atomic_op_return{acquire}(X,+,1) -atomic_inc_return_release(X) __atomic_op_return{release}(X,+,1) -atomic_fetch_inc(X) __atomic_fetch_op{mb}(X,+,1) -atomic_fetch_inc_relaxed(X) __atomic_fetch_op{once}(X,+,1) -atomic_fetch_inc_acquire(X) __atomic_fetch_op{acquire}(X,+,1) -atomic_fetch_inc_release(X) __atomic_fetch_op{release}(X,+,1) - -atomic_sub_return(V,X) __atomic_op_return{mb}(X,-,V) -atomic_sub_return_relaxed(V,X) __atomic_op_return{once}(X,-,V) -atomic_sub_return_acquire(V,X) __atomic_op_return{acquire}(X,-,V) -atomic_sub_return_release(V,X) __atomic_op_return{release}(X,-,V) -atomic_fetch_sub(V,X) __atomic_fetch_op{mb}(X,-,V) -atomic_fetch_sub_relaxed(V,X) __atomic_fetch_op{once}(X,-,V) -atomic_fetch_sub_acquire(V,X) __atomic_fetch_op{acquire}(X,-,V) -atomic_fetch_sub_release(V,X) __atomic_fetch_op{release}(X,-,V) - -atomic_dec_return(X) __atomic_op_return{mb}(X,-,1) -atomic_dec_return_relaxed(X) __atomic_op_return{once}(X,-,1) -atomic_dec_return_acquire(X) __atomic_op_return{acquire}(X,-,1) -atomic_dec_return_release(X) __atomic_op_return{release}(X,-,1) -atomic_fetch_dec(X) __atomic_fetch_op{mb}(X,-,1) -atomic_fetch_dec_relaxed(X) __atomic_fetch_op{once}(X,-,1) -atomic_fetch_dec_acquire(X) __atomic_fetch_op{acquire}(X,-,1) -atomic_fetch_dec_release(X) __atomic_fetch_op{release}(X,-,1) - -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_sub_and_test(V,X) __atomic_op_return{mb}(X,-,V) =3D=3D 0 -atomic_dec_and_test(X) __atomic_op_return{mb}(X,-,1) =3D=3D 0 -atomic_inc_and_test(X) __atomic_op_return{mb}(X,+,1) =3D=3D 0 -atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0 -atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0 -atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0 -atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0 - -atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V) -atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V) -atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V) -atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V) - -atomic_add_unless(X,V,W) __atomic_add_unless{mb}(X,V,W) +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) +atomic_add_return_acquire(V,X) __atomic_op_return{ACQUIRE}(X,+,V) +atomic_add_return_release(V,X) __atomic_op_return{RELEASE}(X,+,V) +atomic_fetch_add(V,X) __atomic_fetch_op{MB}(X,+,V) +atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{ONCE}(X,+,V) +atomic_fetch_add_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,+,V) +atomic_fetch_add_release(V,X) __atomic_fetch_op{RELEASE}(X,+,V) + +atomic_fetch_and(V,X) __atomic_fetch_op{MB}(X,&,V) +atomic_fetch_and_relaxed(V,X) __atomic_fetch_op{ONCE}(X,&,V) +atomic_fetch_and_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,&,V) +atomic_fetch_and_release(V,X) __atomic_fetch_op{RELEASE}(X,&,V) + +atomic_fetch_or(V,X) __atomic_fetch_op{MB}(X,|,V) +atomic_fetch_or_relaxed(V,X) __atomic_fetch_op{ONCE}(X,|,V) +atomic_fetch_or_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,|,V) +atomic_fetch_or_release(V,X) __atomic_fetch_op{RELEASE}(X,|,V) + +atomic_fetch_xor(V,X) __atomic_fetch_op{MB}(X,^,V) +atomic_fetch_xor_relaxed(V,X) __atomic_fetch_op{ONCE}(X,^,V) +atomic_fetch_xor_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,^,V) +atomic_fetch_xor_release(V,X) __atomic_fetch_op{RELEASE}(X,^,V) + +atomic_inc_return(X) __atomic_op_return{MB}(X,+,1) +atomic_inc_return_relaxed(X) __atomic_op_return{ONCE}(X,+,1) +atomic_inc_return_acquire(X) __atomic_op_return{ACQUIRE}(X,+,1) +atomic_inc_return_release(X) __atomic_op_return{RELEASE}(X,+,1) +atomic_fetch_inc(X) __atomic_fetch_op{MB}(X,+,1) +atomic_fetch_inc_relaxed(X) __atomic_fetch_op{ONCE}(X,+,1) +atomic_fetch_inc_acquire(X) __atomic_fetch_op{ACQUIRE}(X,+,1) +atomic_fetch_inc_release(X) __atomic_fetch_op{RELEASE}(X,+,1) + +atomic_sub_return(V,X) __atomic_op_return{MB}(X,-,V) +atomic_sub_return_relaxed(V,X) __atomic_op_return{ONCE}(X,-,V) +atomic_sub_return_acquire(V,X) __atomic_op_return{ACQUIRE}(X,-,V) +atomic_sub_return_release(V,X) __atomic_op_return{RELEASE}(X,-,V) +atomic_fetch_sub(V,X) __atomic_fetch_op{MB}(X,-,V) +atomic_fetch_sub_relaxed(V,X) __atomic_fetch_op{ONCE}(X,-,V) +atomic_fetch_sub_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,-,V) +atomic_fetch_sub_release(V,X) __atomic_fetch_op{RELEASE}(X,-,V) + +atomic_dec_return(X) __atomic_op_return{MB}(X,-,1) +atomic_dec_return_relaxed(X) __atomic_op_return{ONCE}(X,-,1) +atomic_dec_return_acquire(X) __atomic_op_return{ACQUIRE}(X,-,1) +atomic_dec_return_release(X) __atomic_op_return{RELEASE}(X,-,1) +atomic_fetch_dec(X) __atomic_fetch_op{MB}(X,-,1) +atomic_fetch_dec_relaxed(X) __atomic_fetch_op{ONCE}(X,-,1) +atomic_fetch_dec_acquire(X) __atomic_fetch_op{ACQUIRE}(X,-,1) +atomic_fetch_dec_release(X) __atomic_fetch_op{RELEASE}(X,-,1) + +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_sub_and_test(V,X) __atomic_op_return{MB}(X,-,V) =3D=3D 0 +atomic_dec_and_test(X) __atomic_op_return{MB}(X,-,1) =3D=3D 0 +atomic_inc_and_test(X) __atomic_op_return{MB}(X,+,1) =3D=3D 0 +atomic_add_negative(V,X) __atomic_op_return{MB}(X,+,V) < 0 +atomic_add_negative_relaxed(V,X) __atomic_op_return{ONCE}(X,+,V) < 0 +atomic_add_negative_acquire(V,X) __atomic_op_return{ACQUIRE}(X,+,V) < 0 +atomic_add_negative_release(V,X) __atomic_op_return{RELEASE}(X,+,V) < 0 + +atomic_fetch_andnot(V,X) __atomic_fetch_op{MB}(X,&~,V) +atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{ACQUIRE}(X,&~,V) +atomic_fetch_andnot_release(V,X) __atomic_fetch_op{RELEASE}(X,&~,V) +atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{ONCE}(X,&~,V) + +atomic_add_unless(X,V,W) __atomic_add_unless{MB}(X,V,W) --=20 2.40.1