From nobody Mon Feb 9 00:55:34 2026 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 9A686C761A6 for ; Tue, 21 Mar 2023 01:03:17 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229898AbjCUBDP (ORCPT ); Mon, 20 Mar 2023 21:03:15 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:46930 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229828AbjCUBDL (ORCPT ); Mon, 20 Mar 2023 21:03:11 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [139.178.84.217]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 06979311EC; Mon, 20 Mar 2023 18:02:49 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 59A91618E6; Tue, 21 Mar 2023 01:02:48 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id B458FC433D2; Tue, 21 Mar 2023 01:02:47 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1679360567; bh=EZtQGfiUVBCTzbeZZD6hd/oXm/Lh2CaRjKVyFOMGkQg=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=KdRWKpr1DrklM1VpNS4yHWebuftSVAkBgJXz3NTj3UBWwzIhPpJ2TikJMrTAl1xTj mbNfNAYAn7xiBfeJPHyv8zSSBnhoKcbEVygo5JiDQOgxM+UApz/lul8kR4M7AFYMjh wvRUHCrd8uLEC98JEW8+ckrrjc43vKPsdcumPWfQUmr3x3gf2m3ne3wcdhKuVkUmyQ raZbHBK/TewSzdu5ixSK/9RFrGiOCIePp/YODe2cmRsFTmSLsBFmDsItNqiFNbCEi8 0ETFnGHjOJDcZ4sR5b3kRetQ6vF2mIsqCCUD05e8oyJOQUnzQTsYChAbrbIzUU7a4y y4vzuVzLEjlTg== Received: by paulmck-ThinkPad-P72.home (Postfix, from userid 1000) id 69FC61540395; Mon, 20 Mar 2023 18:02:47 -0700 (PDT) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, 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 1/8] tools/memory-model: Update some warning labels Date: Mon, 20 Mar 2023 18:02:39 -0700 Message-Id: <20230321010246.50960-1-paulmck@kernel.org> X-Mailer: git-send-email 2.40.0.rc2 In-Reply-To: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Type: text/plain; charset="utf-8" From: Alan Stern Some of the warning labels used in the LKMM are unfortunately ambiguous. In particular, the same warning is used for both an unmatched rcu_read_lock() call and for an unmatched rcu_read_unlock() call. Likewise for the srcu_* equivalents. Also, the warning about passing a wrong value to srcu_read_unlock() -- i.e., a value different from the one returned by the matching srcu_read_lock() -- talks about bad nesting rather than non-matching values. Let's update the warning labels to make their meanings more clear. Signed-off-by: Alan Stern Reviewed-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney Acked-by: Andrea Parri --- tools/memory-model/linux-kernel.bell | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linu= x-kernel.bell index 70a9073dec3e..dc464854d28a 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -53,8 +53,8 @@ let rcu-rscs =3D let rec in matched =20 (* Validate nesting *) -flag ~empty Rcu-lock \ domain(rcu-rscs) as unbalanced-rcu-locking -flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking +flag ~empty Rcu-lock \ domain(rcu-rscs) as unmatched-rcu-lock +flag ~empty Rcu-unlock \ range(rcu-rscs) as unmatched-rcu-unlock =20 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *) let srcu-rscs =3D let rec @@ -69,14 +69,14 @@ let srcu-rscs =3D let rec in matched =20 (* Validate nesting *) -flag ~empty Srcu-lock \ domain(srcu-rscs) as unbalanced-srcu-locking -flag ~empty Srcu-unlock \ range(srcu-rscs) as unbalanced-srcu-locking +flag ~empty Srcu-lock \ domain(srcu-rscs) as unmatched-srcu-lock +flag ~empty Srcu-unlock \ range(srcu-rscs) as unmatched-srcu-unlock =20 (* Check for use of synchronize_srcu() inside an RCU critical section *) flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep =20 (* Validate SRCU dynamic match *) -flag ~empty different-values(srcu-rscs) as srcu-bad-nesting +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) | --=20 2.40.0.rc2 From nobody Mon Feb 9 00:55:34 2026 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 69364C6FD1D for ; Tue, 21 Mar 2023 01:03:36 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229986AbjCUBDe (ORCPT ); Mon, 20 Mar 2023 21:03:34 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:47060 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229892AbjCUBDP (ORCPT ); Mon, 20 Mar 2023 21:03:15 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [145.40.68.75]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 32CEF32E46; Mon, 20 Mar 2023 18:02:51 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id 1DEA5B80AB3; Tue, 21 Mar 2023 01:02:49 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id CB157C433EF; Tue, 21 Mar 2023 01:02:47 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1679360567; bh=2Y/XkB2XZZFnsP5FyaQPKn2f91HJuzwOuZ3zcl/2c04=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=G9DDTiT46Oi1hcKTuoi/+ql7R4BJ7GnazB3Dgvm89Zx/f4kXniLalQP0HpJ5nvLD0 fGUzRF++FpNxq3Knx4+BbIXUSVErCmq1VxsKb+ZrWrF8b+pz88tR39FgDJgs21YmW8 Fa/dKAeeyhfILqkglV7/WpDMLU0CxQO/oAPNoY1dIX0f7D7N3uQkE79EZlMGsjuXCE 3ln9txdApPjeLtX2YoCSYOkMPtBDdhhmnfXO0427L5T7dWpO5Ft3aUxl59229CQ2ZN LSb/ql8xu4h4BizA5kmkurGpbLDccyFhvOriZJWStVCphzrI30Kwp66cdi18bDM/ar 4h0fEG3U5WE6A== Received: by paulmck-ThinkPad-P72.home (Postfix, from userid 1000) id 6EAAC154039B; Mon, 20 Mar 2023 18:02:47 -0700 (PDT) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, 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 2/8] tools/memory-model: Unify UNLOCK+LOCK pairings to po-unlock-lock-po Date: Mon, 20 Mar 2023 18:02:40 -0700 Message-Id: <20230321010246.50960-2-paulmck@kernel.org> X-Mailer: git-send-email 2.40.0.rc2 In-Reply-To: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Type: text/plain; charset="utf-8" From: Jonas Oberhauser LKMM uses two relations for talking about UNLOCK+LOCK pairings: 1) po-unlock-lock-po, which handles UNLOCK+LOCK pairings on the same CPU or immediate lock handovers on the same lock variable 2) po;[UL];(co|po);[LKW];po, which handles UNLOCK+LOCK pairs literally as described in rcupdate.h#L1002, i.e., even after a sequence of handovers on the same lock variable. The latter relation is used only once, to provide the guarantee defined in rcupdate.h#L1002 by smp_mb__after_unlock_lock(), which makes any UNLOCK+LOCK pair followed by the fence behave like a full barrier. This patch drops this use in favor of using po-unlock-lock-po everywhere, which unifies the way the model talks about UNLOCK+LOCK pairings. At first glance this seems to weaken the guarantee given by LKMM: When considering a long sequence of lock handovers such as below, where P0 hands the lock to P1, which hands it to P2, which finally executes such an after_unlock_lock fence, the mb relation currently links any stores in the critical section of P0 to instructions P2 executes after its fence, but not so after the patch. P0(int *x, int *y, spinlock_t *mylock) { spin_lock(mylock); WRITE_ONCE(*x, 2); spin_unlock(mylock); WRITE_ONCE(*y, 1); } P1(int *y, int *z, spinlock_t *mylock) { int r0 =3D READ_ONCE(*y); // reads 1 spin_lock(mylock); spin_unlock(mylock); WRITE_ONCE(*z,1); } P2(int *z, int *d, spinlock_t *mylock) { int r1 =3D READ_ONCE(*z); // reads 1 spin_lock(mylock); spin_unlock(mylock); smp_mb__after_unlock_lock(); WRITE_ONCE(*d,1); } P3(int *x, int *d) { WRITE_ONCE(*d,2); smp_mb(); WRITE_ONCE(*x,1); } exists (1:r0=3D1 /\ 2:r1=3D1 /\ x=3D2 /\ d=3D2) Nevertheless, the ordering guarantee given in rcupdate.h is actually not weakened. This is because the unlock operations along the sequence of handovers are A-cumulative fences. They ensure that any stores that propagate to the CPU performing the first unlock operation in the sequence must also propagate to every CPU that performs a subsequent lock operation in the sequence. Therefore any such stores will also be ordered correctly by the fence even if only the final handover is considered a full barrier. Indeed this patch does not affect the behaviors allowed by LKMM at all. The mb relation is used to define ordering through: 1) mb/.../ppo/hb, where the ordering is subsumed by hb+ where the lock-release, rfe, and unlock-acquire orderings each provide hb 2) mb/strong-fence/cumul-fence/prop, where the rfe and A-cumulative lock-release orderings simply add more fine-grained cumul-fence edges to substitute a single strong-fence edge provided by a long lock handover sequence 3) mb/strong-fence/pb and various similar uses in the definition of data races, where as discussed above any long handover sequence can be turned into a sequence of cumul-fence edges that provide the same ordering. Signed-off-by: Jonas Oberhauser Reviewed-by: Alan Stern Signed-off-by: Paul E. McKenney Acked-by: Andrea Parri --- tools/memory-model/linux-kernel.cat | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux= -kernel.cat index 07f884f9b2bf..6e531457bb73 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -37,8 +37,19 @@ let mb =3D ([M] ; fencerel(Mb) ; [M]) | ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; - fencerel(After-unlock-lock) ; [M]) +(* + * Note: The po-unlock-lock-po relation only passes the lock to the direct + * successor, perhaps giving the impression that the ordering of the + * smp_mb__after_unlock_lock() fence only affects a single lock handover. + * However, in a longer sequence of lock handovers, the implicit + * A-cumulative release fences of lock-release ensure that any stores that + * propagate to one of the involved CPUs before it hands over the lock to + * the next CPU will also propagate to the final CPU handing over the lock + * to the CPU that executes the fence. Therefore, all those stores are + * also affected by the fence. + *) + ([M] ; po-unlock-lock-po ; + [After-unlock-lock] ; po ; [M]) let gp =3D po ; [Sync-rcu | Sync-srcu] ; po? let strong-fence =3D mb | gp =20 --=20 2.40.0.rc2 From nobody Mon Feb 9 00:55:34 2026 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 82EE0C7618D for ; Tue, 21 Mar 2023 01:03:29 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229940AbjCUBD2 (ORCPT ); Mon, 20 Mar 2023 21:03:28 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:46930 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229843AbjCUBDN (ORCPT ); Mon, 20 Mar 2023 21:03:13 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [IPv6:2604:1380:4601:e00::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 2ECDD32CD2; Mon, 20 Mar 2023 18:02:50 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id 2439AB810A0; Tue, 21 Mar 2023 01:02:49 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id D77ECC4339B; Tue, 21 Mar 2023 01:02:47 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1679360567; bh=v+o7k88i3gFGVlJhUGgecvLTnT0QcUZwggZOJd/nU3A=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=HaPWWk3nvRhqjrKOptAHVkoP8Wrq9SI/mzmx1D5ifqmDkbfu3cBJpnH9aZUrleQvW MFsjnXzoFLsVEBONSk2z+kXCvr3RtoBtj5rDI5DQ2oTaj/zvZ6pJLnBse+pAxzOeCi aLOl9bYqMx/yhFtzqTYDPKPzZlmmTrSP9VwD/pKqQntBI9NI4Jc4rUF/v5RRI26KEM LLYCXPoRb3nOk/2p5MtHQByoDpjhAUKsjWHxROgEt+/uz6ZuD2drpd3m+Qz3okskHT QRFRHUiqoKl+bQsQ0Xdy6r6fkenr+E/Y2a5otbLbrzE8oPDJerNQZ1KyKcso8LNu3O ynThYWkWn8f9Q== Received: by paulmck-ThinkPad-P72.home (Postfix, from userid 1000) id 73E3B154039D; Mon, 20 Mar 2023 18:02:47 -0700 (PDT) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, 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, "Paul E. McKenney" Subject: [PATCH memory-model 3/8] tools/memory-model: Add smp_mb__after_srcu_read_unlock() Date: Mon, 20 Mar 2023 18:02:41 -0700 Message-Id: <20230321010246.50960-3-paulmck@kernel.org> X-Mailer: git-send-email 2.40.0.rc2 In-Reply-To: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Type: text/plain; charset="utf-8" This commit adds support for smp_mb__after_srcu_read_unlock(), which, when combined with a prior srcu_read_unlock(), implies a full memory barrier. No ordering is guaranteed to accesses between the two, and placing accesses between is bad practice in any case. Tests may be found at https://github.com/paulmckrcu/litmus in files matching manual/kernel/C-srcu-mb-*.litmus. Signed-off-by: Paul E. McKenney --- tools/memory-model/linux-kernel.bell | 3 ++- tools/memory-model/linux-kernel.cat | 3 ++- tools/memory-model/linux-kernel.def | 1 + 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linu= x-kernel.bell index dc464854d28a..b92fdf7f6eeb 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -31,7 +31,8 @@ enum Barriers =3D 'wmb (*smp_wmb*) || 'before-atomic (*smp_mb__before_atomic*) || 'after-atomic (*smp_mb__after_atomic*) || 'after-spinlock (*smp_mb__after_spinlock*) || - 'after-unlock-lock (*smp_mb__after_unlock_lock*) + 'after-unlock-lock (*smp_mb__after_unlock_lock*) || + 'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*) instructions F[Barriers] =20 (* SRCU *) diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux= -kernel.cat index 6e531457bb73..3a4d3b49e85c 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -49,7 +49,8 @@ let mb =3D ([M] ; fencerel(Mb) ; [M]) | * also affected by the fence. *) ([M] ; po-unlock-lock-po ; - [After-unlock-lock] ; po ; [M]) + [After-unlock-lock] ; po ; [M]) | + ([M] ; po? ; [Srcu-unlock] ; fencerel(After-srcu-read-unlock) ; [M]) let gp =3D po ; [Sync-rcu | Sync-srcu] ; po? let strong-fence =3D mb | gp =20 diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux= -kernel.def index ef0f3c1850de..a6b6fbc9d0b2 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -24,6 +24,7 @@ smp_mb__before_atomic() { __fence{before-atomic}; } smp_mb__after_atomic() { __fence{after-atomic}; } smp_mb__after_spinlock() { __fence{after-spinlock}; } smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; } +smp_mb__after_srcu_read_unlock() { __fence{after-srcu-read-unlock}; } barrier() { __fence{barrier}; } =20 // Exchange --=20 2.40.0.rc2 From nobody Mon Feb 9 00:55:34 2026 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 45CC6C761A6 for ; Tue, 21 Mar 2023 01:03:33 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229970AbjCUBDb (ORCPT ); Mon, 20 Mar 2023 21:03:31 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:46978 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229846AbjCUBDM (ORCPT ); Mon, 20 Mar 2023 21:03:12 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 0831C3251A; Mon, 20 Mar 2023 18:02:49 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 826B5618F3; Tue, 21 Mar 2023 01:02:48 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id E30FAC4339E; Tue, 21 Mar 2023 01:02:47 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1679360567; bh=FT+Zpl2+JDglqimqaqOEQRRviu8fzMr0CfKlrl4m+TY=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=sTuYivu0kNSe9J7LE0cBTiQ01DXZeVMsPTKFG2LCALmDEeQg/wgzeuO4S6+PRkOYI eHRU0WZrBemHkq2jupfVz1VQu1lVfLZmotMC9y5IVLBT7AiOUjM8BqvHsQJeb19oSf rBCfFZaFJGSJqOZsulzeqPEeb6kjSN8XuYScXtkTgaeVj0hgWfznXElCIHqv8HI+o6 V6wtjYvrDSUVF2UItwNa4g3nlrMTuddEWroM0KhNCxu4IIyv3rekmbS0IzJWdKcq75 ft+ZHckgMCbSi476XTyxIXLnn8UeuEGaxxzlAUOfHHw3znzVLAtUPu3l3Jrx2YZFl+ xBpsrZZobuozw== Received: by paulmck-ThinkPad-P72.home (Postfix, from userid 1000) id 78BF4154039F; Mon, 20 Mar 2023 18:02:47 -0700 (PDT) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, 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, "Joel Fernandes (Google)" , "Paul E . McKenney" Subject: [PATCH memory-model 4/8] tools/memory-model: Restrict to-r to read-read address dependency Date: Mon, 20 Mar 2023 18:02:42 -0700 Message-Id: <20230321010246.50960-4-paulmck@kernel.org> X-Mailer: git-send-email 2.40.0.rc2 In-Reply-To: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Type: text/plain; charset="utf-8" From: "Joel Fernandes (Google)" During a code-reading exercise of linux-kernel.cat CAT file, I generated a graph to show the to-r relations. While likely not problematic for the model, I found it confusing that a read-write address dependency would show as a to-r edge on the graph. This patch therefore restricts the to-r links derived from addr to only read-read address dependencies, so that read-write address dependencies don= 't show as to-r in the graphs. This should also prevent future users of to-r f= rom deriving incorrect relations. Note that a read-write address dep, obviously, still ends up in the ppo relation via the to-w relation. I verified that a read-read address dependency still shows up as a to-r link in the graph, as it did before. For reference, the problematic graph was generated with the following command: herd7 -conf linux-kernel.cfg \ -doshow dep -doshow to-r -doshow to-w ./foo.litmus -show all -o OUT/ Signed-off-by: Joel Fernandes (Google) Acked-by: Alan Stern Signed-off-by: Paul E. McKenney Acked-by: Andrea Parri --- tools/memory-model/linux-kernel.cat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux= -kernel.cat index 3a4d3b49e85c..cfc1b8fd46da 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -81,7 +81,7 @@ let dep =3D addr | data let rwdep =3D (dep | ctrl) ; [W] let overwrite =3D co | fr let to-w =3D rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) -let to-r =3D addr | (dep ; [Marked] ; rfi) +let to-r =3D (addr ; [R]) | (dep ; [Marked] ; rfi) let ppo =3D to-r | to-w | fence | (po-unlock-lock-po & int) =20 (* Propagation: Ordering from release operations and strong fences. *) --=20 2.40.0.rc2 From nobody Mon Feb 9 00:55:34 2026 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 917ACC6FD1D for ; Tue, 21 Mar 2023 01:03:26 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229924AbjCUBDY (ORCPT ); Mon, 20 Mar 2023 21:03:24 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:46976 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229842AbjCUBDM (ORCPT ); Mon, 20 Mar 2023 21:03:12 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 069E831BC0; Mon, 20 Mar 2023 18:02:49 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 9921E618F4; Tue, 21 Mar 2023 01:02:48 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id F1E74C4339C; Tue, 21 Mar 2023 01:02:47 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1679360568; bh=6bX96lqBuqkytWesc7/sc0GFPDrnpTONdzva8MA/OSU=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=KU9TPc9NSL5f21FTl3EsNTG6DgH0hpArAce22TpJMmOarpJB+ZzcKKFzbEgy6YzSK Z+qBn74DzVYa8d2PmoKLdQUFQjIX6H/ZVdq44FMPXtiwGdxe+V7P8uXKb9D+ZJv8+7 StTgzn0/Lddy5Ztkyl/4FcZgEQm58KH8LGoaX8dbN8pWhkVTJt1EiLBsKcBj8cwjlU nAbJVtu9Jo2BFwC9kOJYJfmjt49AMGDYpooZmFxr3M81lLTT5RBTIa8knxEtWb8HOQ cIzLoNcENNKk4AAwl31QoW5X9SEeMKDhz8Az11knI8xBFxWk7dTru7hB5hij2HBCQk XoqIEX5lJsaRQ== Received: by paulmck-ThinkPad-P72.home (Postfix, from userid 1000) id 7D0CF15403A1; Mon, 20 Mar 2023 18:02:47 -0700 (PDT) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, 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, "Paul E . McKenney" , Jonas Oberhauser Subject: [PATCH memory-model 5/8] tools/memory-model: Provide exact SRCU semantics Date: Mon, 20 Mar 2023 18:02:43 -0700 Message-Id: <20230321010246.50960-5-paulmck@kernel.org> X-Mailer: git-send-email 2.40.0.rc2 In-Reply-To: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Type: text/plain; charset="utf-8" From: Alan Stern LKMM has long provided only approximate handling of SRCU read-side critical sections. This has not been a pressing problem because LKMM's traditional handling is correct for the common cases of non-overlapping and properly nested critical sections. However, LKMM's traditional handling of partially overlapping critical sections incorrectly fuses them into one large critical section. For example, consider the following litmus test: Reported-by: Paul E. McKenney Reviewed-by: Jonas Oberhauser ------------------------------------------------------------------------ C C-srcu-nest-5 (* * Result: Sometimes * * This demonstrates non-nested overlapping of SRCU read-side critical * sections. Unlike RCU, SRCU critical sections do not unconditionally * nest. *) {} P0(int *x, int *y, struct srcu_struct *s1) { int r1; int r2; int r3; int r4; r3 =3D srcu_read_lock(s1); r2 =3D READ_ONCE(*y); r4 =3D srcu_read_lock(s1); srcu_read_unlock(s1, r3); r1 =3D READ_ONCE(*x); srcu_read_unlock(s1, r4); } P1(int *x, int *y, struct srcu_struct *s1) { WRITE_ONCE(*y, 1); synchronize_srcu(s1); WRITE_ONCE(*x, 1); } locations [0:r1] exists (0:r1=3D1 /\ 0:r2=3D0) ------------------------------------------------------------------------ Current mainline incorrectly flattens the two critical sections into one larger critical section, giving "Never" instead of the correct "Sometimes": ------------------------------------------------------------------------ $ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus Test C-srcu-nest-5 Allowed States 3 0:r1=3D0; 0:r2=3D0; 0:r1=3D0; 0:r2=3D1; 0:r1=3D1; 0:r2=3D1; No Witnesses Positive: 0 Negative: 3 Flag srcu-bad-nesting Condition exists (0:r1=3D1 /\ 0:r2=3D0) Observation C-srcu-nest-5 Never 0 3 Time C-srcu-nest-5 0.01 Hash=3De692c106cf3e84e20f12991dc438ff1b ------------------------------------------------------------------------ To its credit, it does complain about bad nesting. But with this commit we get the following result, which has the virtue of being correct: ------------------------------------------------------------------------ $ herd7 -conf linux-kernel.cfg C-srcu-nest-5.litmus Test C-srcu-nest-5 Allowed States 4 0:r1=3D0; 0:r2=3D0; 0:r1=3D0; 0:r2=3D1; 0:r1=3D1; 0:r2=3D0; 0:r1=3D1; 0:r2=3D1; Ok Witnesses Positive: 1 Negative: 3 Condition exists (0:r1=3D1 /\ 0:r2=3D0) Observation C-srcu-nest-5 Sometimes 1 3 Time C-srcu-nest-5 0.05 Hash=3De692c106cf3e84e20f12991dc438ff1b ------------------------------------------------------------------------ In addition, there are new srcu_down_read() and srcu_up_read() functions on their way to mainline. Roughly speaking, these are to srcu_read_lock() and srcu_read_unlock() as down() and up() are to mutex_lock() and mutex_unlock(). The key point is that srcu_down_read() can execute in one process and the matching srcu_up_read() in another, as shown in this litmus test: ------------------------------------------------------------------------ C C-srcu-nest-6 (* * Result: Never * * This would be valid for srcu_down_read() and srcu_up_read(). *) {} P0(int *x, int *y, struct srcu_struct *s1, int *idx, int *f) { int r2; int r3; r3 =3D srcu_down_read(s1); WRITE_ONCE(*idx, r3); r2 =3D READ_ONCE(*y); smp_store_release(f, 1); } P1(int *x, int *y, struct srcu_struct *s1, int *idx, int *f) { int r1; int r3; int r4; r4 =3D smp_load_acquire(f); r1 =3D READ_ONCE(*x); r3 =3D READ_ONCE(*idx); srcu_up_read(s1, r3); } P2(int *x, int *y, struct srcu_struct *s1) { WRITE_ONCE(*y, 1); synchronize_srcu(s1); WRITE_ONCE(*x, 1); } locations [0:r1] filter (1:r4=3D1) exists (1:r1=3D1 /\ 0:r2=3D0) ------------------------------------------------------------------------ When run on current mainline, this litmus test gets a complaint about an unknown macro srcu_down_read(). With this commit: ------------------------------------------------------------------------ herd7 -conf linux-kernel.cfg C-srcu-nest-6.litmus Test C-srcu-nest-6 Allowed States 3 0:r1=3D0; 0:r2=3D0; 1:r1=3D0; 0:r1=3D0; 0:r2=3D1; 1:r1=3D0; 0:r1=3D0; 0:r2=3D1; 1:r1=3D1; No Witnesses Positive: 0 Negative: 3 Condition exists (1:r1=3D1 /\ 0:r2=3D0) Observation C-srcu-nest-6 Never 0 3 Time C-srcu-nest-6 0.02 Hash=3Dc1f20257d052ca5e899be508bedcb2a1 ------------------------------------------------------------------------ Note that the user must supply the flag "f" and the "filter" clause, similar to what must be done to emulate call_rcu(). The commit works by treating srcu_read_lock()/srcu_down_read() as loads and srcu_read_unlock()/srcu_up_read() as stores. This allows us to determine which unlock matches which lock by looking for a data dependency between them. In order for this to work properly, the data dependencies have to be tracked through stores to intermediate variables such as "idx" in the litmus test above; this is handled by the new carry-srcu-data relation. But it's important here (and in the existing carry-dep relation) to avoid tracking the dependencies through SRCU unlock stores. Otherwise, in situations resembling: A: r1 =3D srcu_read_lock(s); B: srcu_read_unlock(s, r1); C: r2 =3D srcu_read_lock(s); D: srcu_read_unlock(s, r2); it would look as if D was dependent on both A and C, because "s" would appear to be an intermediate variable written by B and read by C. This explains the complications in the definitions of carry-srcu-dep and carry-dep. As a debugging aid, the commit adds a check for errors in which the value returned by one call to srcu_read_lock()/srcu_down_read() is passed to more than one instance of srcu_read_unlock()/srcu_up_read(). Finally, since these SRCU-related primitives are now treated as ordinary reads and writes, we have to add them into the lists of marked accesses (i.e., not subject to data races) and lock-related accesses (i.e., one shouldn't try to access an srcu_struct with a non-lock-related primitive such as READ_ONCE() or a plain write). Portions of this approach were suggested by Boqun Feng and Jonas Oberhauser. [ paulmck: Fix space-before-tab whitespace nit. ] Reported-by: Paul E. McKenney Signed-off-by: Alan Stern Reviewed-by: Jonas Oberhauser Signed-off-by: Paul E. McKenney --- tools/memory-model/linux-kernel.bell | 17 +++++------------ tools/memory-model/linux-kernel.def | 6 ++++-- tools/memory-model/lock.cat | 6 +++--- 3 files changed, 12 insertions(+), 17 deletions(-) diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linu= x-kernel.bell index b92fdf7f6eeb..ce068700939c 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -58,20 +58,13 @@ flag ~empty Rcu-lock \ domain(rcu-rscs) as unmatched-rc= u-lock flag ~empty Rcu-unlock \ range(rcu-rscs) as unmatched-rcu-unlock =20 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *) -let srcu-rscs =3D let rec - unmatched-locks =3D Srcu-lock \ domain(matched) - and unmatched-unlocks =3D Srcu-unlock \ range(matched) - and unmatched =3D unmatched-locks | unmatched-unlocks - and unmatched-po =3D ([unmatched] ; po ; [unmatched]) & loc - and unmatched-locks-to-unlocks =3D - ([unmatched-locks] ; po ; [unmatched-unlocks]) & loc - and matched =3D matched | (unmatched-locks-to-unlocks \ - (unmatched-po ; unmatched-po)) - in matched +let carry-srcu-data =3D (data ; [~ Srcu-unlock] ; rf)* +let srcu-rscs =3D ([Srcu-lock] ; carry-srcu-data ; data ; [Srcu-unlock]) &= loc =20 (* Validate nesting *) flag ~empty Srcu-lock \ domain(srcu-rscs) as unmatched-srcu-lock flag ~empty Srcu-unlock \ range(srcu-rscs) as unmatched-srcu-unlock +flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-matches =20 (* Check for use of synchronize_srcu() inside an RCU critical section *) flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep @@ -81,11 +74,11 @@ flag ~empty different-values(srcu-rscs) as srcu-bad-val= ue-match =20 (* Compute marked and plain memory accesses *) let Marked =3D (~M) | IW | Once | Release | Acquire | domain(rmw) | range(= rmw) | - LKR | LKW | UL | LF | RL | RU + LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock let Plain =3D M \ Marked =20 (* Redefine dependencies to include those carried through plain accesses *) -let carry-dep =3D (data ; rfi)* +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 diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux= -kernel.def index a6b6fbc9d0b2..88a39601f525 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -50,8 +50,10 @@ synchronize_rcu() { __fence{sync-rcu}; } synchronize_rcu_expedited() { __fence{sync-rcu}; } =20 // SRCU -srcu_read_lock(X) __srcu{srcu-lock}(X) -srcu_read_unlock(X,Y) { __srcu{srcu-unlock}(X,Y); } +srcu_read_lock(X) __load{srcu-lock}(*X) +srcu_read_unlock(X,Y) { __store{srcu-unlock}(*X,Y); } +srcu_down_read(X) __load{srcu-lock}(*X) +srcu_up_read(X,Y) { __store{srcu-unlock}(*X,Y); } synchronize_srcu(X) { __srcu{sync-srcu}(X); } synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); } =20 diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat index 6b52f365d73a..53b5a492739d 100644 --- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -36,9 +36,9 @@ let RU =3D try RU with emptyset (* Treat RL as a kind of LF: a read with no ordering properties *) let LF =3D LF | RL =20 -(* There should be no ordinary R or W accesses to spinlocks *) -let ALL-LOCKS =3D LKR | LKW | UL | LF | RU -flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses +(* There should be no ordinary R or W accesses to spinlocks or SRCU struct= s *) +let ALL-LOCKS =3D LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | Syn= c-srcu +flag ~empty [M \ IW \ ALL-LOCKS] ; loc ; [ALL-LOCKS] as mixed-lock-accesses =20 (* Link Lock-Reads to their RMW-partner Lock-Writes *) let lk-rmw =3D ([LKR] ; po-loc ; [LKW]) \ (po ; po) --=20 2.40.0.rc2 From nobody Mon Feb 9 00:55:34 2026 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 449DFC6FD1D for ; Tue, 21 Mar 2023 01:03:43 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S230020AbjCUBDl (ORCPT ); Mon, 20 Mar 2023 21:03:41 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:47748 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229939AbjCUBD2 (ORCPT ); Mon, 20 Mar 2023 21:03:28 -0400 Received: from sin.source.kernel.org (sin.source.kernel.org [145.40.73.55]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id D85A1303D4; Mon, 20 Mar 2023 18:02:52 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by sin.source.kernel.org (Postfix) with ESMTPS id B1B11CE173F; Tue, 21 Mar 2023 01:02:50 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 22FEAC433A1; Tue, 21 Mar 2023 01:02:48 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1679360568; bh=ogHftEPqZVMExF9RqMnqFfkQ5fyo9sZst3jS5BWNIUQ=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=aMaXhJS0JFHF6wWKE2hp7Jr8p6UBYPwpyxj7DYLWsP8Pr5H8ZWt9ptVZXtxDBO0up 7z0J+t0Px6k/B0I2wTsZpddu/FM+KMJi7YP8kSp2+24uHncdEzhj0DGO+VtixEJkeW VQqHgSIXrasD1prXXHcICpipfPcChsHcAvO+GJORWmfd2JKzSnY9KLqci8soYJahYe WRXjXmBXPMdkz05MTsFr9lJzU7b7MeAVpl60PAHvoxtMW2XHj99HPKyUudkGpZrEl8 zQQwi0xw5tVj2LNkjw7ZAjQ0HBG1rvYhwV1OXJ3dScGW7Z8JCdHFh1XDR9Y5u++ZQ/ ggw5x8LRRnWRw== Received: by paulmck-ThinkPad-P72.home (Postfix, from userid 1000) id 80EC615403A3; Mon, 20 Mar 2023 18:02:47 -0700 (PDT) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, 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 6/8] tools/memory-model: Make ppo a subrelation of po Date: Mon, 20 Mar 2023 18:02:44 -0700 Message-Id: <20230321010246.50960-6-paulmck@kernel.org> X-Mailer: git-send-email 2.40.0.rc2 In-Reply-To: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Type: text/plain; charset="utf-8" From: Jonas Oberhauser As stated in the documentation and implied by its name, the ppo (preserved program order) relation is intended to link po-earlier to po-later instructions under certain conditions. However, a corner case currently allows instructions to be linked by ppo that are not executed by the same thread, i.e., instructions are being linked that have no po relation. This happens due to the mb/strong-fence/fence relations, which (as one case) provide order when locks are passed between threads followed by an smp_mb__after_unlock_lock() fence. This is illustrated in the following litmus test (as can be seen when using herd7 with `doshow ppo`): P0(spinlock_t *x, spinlock_t *y) { spin_lock(x); spin_unlock(x); } P1(spinlock_t *x, spinlock_t *y) { spin_lock(x); smp_mb__after_unlock_lock(); *y =3D 1; } The ppo relation will link P0's spin_lock(x) and P1's *y=3D1, because P0 passes a lock to P1 which then uses this fence. The patch makes ppo a subrelation of po by letting fence contribute to ppo only in case the fence links events of the same thread. Signed-off-by: Jonas Oberhauser Acked-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney --- tools/memory-model/linux-kernel.cat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux= -kernel.cat index cfc1b8fd46da..adf3c4f41229 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -82,7 +82,7 @@ let rwdep =3D (dep | ctrl) ; [W] let overwrite =3D co | fr let to-w =3D rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) let to-r =3D (addr ; [R]) | (dep ; [Marked] ; rfi) -let ppo =3D to-r | to-w | fence | (po-unlock-lock-po & int) +let ppo =3D to-r | to-w | (fence & int) | (po-unlock-lock-po & int) =20 (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) =3D (rfe ; [Marked])? ; r --=20 2.40.0.rc2 From nobody Mon Feb 9 00:55:34 2026 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id 66BE1C6FD1D for ; Tue, 21 Mar 2023 01:03:22 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229915AbjCUBDU (ORCPT ); Mon, 20 Mar 2023 21:03:20 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:46932 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229844AbjCUBDL (ORCPT ); Mon, 20 Mar 2023 21:03:11 -0400 Received: from dfw.source.kernel.org (dfw.source.kernel.org [139.178.84.217]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 7C26E32539; Mon, 20 Mar 2023 18:02:50 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by dfw.source.kernel.org (Postfix) with ESMTPS id 19475618FA; Tue, 21 Mar 2023 01:02:49 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 2F7BFC433A7; Tue, 21 Mar 2023 01:02:48 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1679360568; bh=NMit92Hlr8O4Fd55QLFN98QDjh2AfQaJejrMU0aDepc=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=kSYqFqzLttFaecsizZG22Lw21QYOJCr/4sTVpj/73kiF4/M9aeSVUA6jD54qIzwGk +jad2Nlu2cVuvJAZpfbKiuZ9e/kF6YqxnpA4a4csTbxwPBVCYnA1c3TSGBY9949d/W IzvgD0zzkJwcWQHEdzcwFeToCz7ZXdUnEJ2MWfKxsSvzYd4tz9GbhhX0Ga2NZ2xHRm RTrio7SrsEmZBSAKy/eoRlmwoWWXGbIBFaBz8QdEB7kf5PTsY44WV2AbH2O+goH1i2 h7tpL71mDLT5rFpabcvwcmvPbeHViC47swbyrhTdbQTsPS9EydvFEWWdh2Be3B64Ej qrgO9dLZ5rUxA== Received: by paulmck-ThinkPad-P72.home (Postfix, from userid 1000) id 85A2D15403A5; Mon, 20 Mar 2023 18:02:47 -0700 (PDT) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, 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, Joel Fernandes , Andrea Parri , Jonas Oberhauser , "Paul E. McKenney" , "Paul E . McKenney" Subject: [PATCH memory-model 7/8] tools/memory-model: Add documentation about SRCU read-side critical sections Date: Mon, 20 Mar 2023 18:02:45 -0700 Message-Id: <20230321010246.50960-7-paulmck@kernel.org> X-Mailer: git-send-email 2.40.0.rc2 In-Reply-To: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Type: text/plain; charset="utf-8" From: Alan Stern Expand the discussion of SRCU and its read-side critical sections in the Linux Kernel Memory Model documentation file explanation.txt. The new material discusses recent changes to the memory model made in commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU semantics"). Signed-off-by: Alan Stern Co-developed-by: Joel Fernandes (Google) Signed-off-by: Joel Fernandes (Google) Reviewed-by: Akira Yokosawa Cc: Andrea Parri Cc: Boqun Feng Cc: Jade Alglave Cc: Jonas Oberhauser Cc: Luc Maranget Cc: "Paul E. McKenney" Cc: Peter Zijlstra CC: Will Deacon Signed-off-by: Paul E. McKenney Acked-by: Alan Stern Reviewed-by: Joel Fernandes (Google) --- .../Documentation/explanation.txt | 178 ++++++++++++++++-- 1 file changed, 167 insertions(+), 11 deletions(-) diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memor= y-model/Documentation/explanation.txt index 8e7085238470..6dc8b3642458 100644 --- a/tools/memory-model/Documentation/explanation.txt +++ b/tools/memory-model/Documentation/explanation.txt @@ -28,9 +28,10 @@ Explanation of the Linux-Kernel Memory Consistency Model 20. THE HAPPENS-BEFORE RELATION: hb 21. THE PROPAGATES-BEFORE RELATION: pb 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, an= d rb - 23. LOCKING - 24. PLAIN ACCESSES AND DATA RACES - 25. ODDS AND ENDS + 23. SRCU READ-SIDE CRITICAL SECTIONS + 24. LOCKING + 25. PLAIN ACCESSES AND DATA RACES + 26. ODDS AND ENDS =20 =20 =20 @@ -1848,14 +1849,169 @@ section in P0 both starts before P1's grace period= does and ends before it does, and the critical section in P2 both starts after P1's grace period does and ends after it does. =20 -Addendum: The LKMM now supports SRCU (Sleepable Read-Copy-Update) in -addition to normal RCU. The ideas involved are much the same as -above, with new relations srcu-gp and srcu-rscsi added to represent -SRCU grace periods and read-side critical sections. There is a -restriction on the srcu-gp and srcu-rscsi links that can appear in an -rcu-order sequence (the srcu-rscsi links must be paired with srcu-gp -links having the same SRCU domain with proper nesting); the details -are relatively unimportant. +The LKMM supports SRCU (Sleepable Read-Copy-Update) in addition to +normal RCU. The ideas involved are much the same as above, with new +relations srcu-gp and srcu-rscsi added to represent SRCU grace periods +and read-side critical sections. However, there are some significant +differences between RCU read-side critical sections and their SRCU +counterparts, as described in the next section. + + +SRCU READ-SIDE CRITICAL SECTIONS +-------------------------------- + +The LKMM uses the srcu-rscsi relation to model SRCU read-side critical +sections. They differ from RCU read-side critical sections in the +following respects: + +1. Unlike the analogous RCU primitives, synchronize_srcu(), + srcu_read_lock(), and srcu_read_unlock() take a pointer to a + struct srcu_struct as an argument. This structure is called + an SRCU domain, and calls linked by srcu-rscsi must have the + same domain. Read-side critical sections and grace periods + associated with different domains are independent of one + another; the SRCU version of the RCU Guarantee applies only + to pairs of critical sections and grace periods having the + same domain. + +2. srcu_read_lock() returns a value, called the index, which must + be passed to the matching srcu_read_unlock() call. Unlike + rcu_read_lock() and rcu_read_unlock(), an srcu_read_lock() + call does not always have to match the next unpaired + srcu_read_unlock(). In fact, it is possible for two SRCU + read-side critical sections to overlap partially, as in the + following example (where s is an srcu_struct and idx1 and idx2 + are integer variables): + + idx1 =3D srcu_read_lock(&s); // Start of first RSCS + idx2 =3D srcu_read_lock(&s); // Start of second RSCS + srcu_read_unlock(&s, idx1); // End of first RSCS + srcu_read_unlock(&s, idx2); // End of second RSCS + + The matching is determined entirely by the domain pointer and + index value. By contrast, if the calls had been + rcu_read_lock() and rcu_read_unlock() then they would have + created two nested (fully overlapping) read-side critical + sections: an inner one and an outer one. + +3. The srcu_down_read() and srcu_up_read() primitives work + exactly like srcu_read_lock() and srcu_read_unlock(), except + that matching calls don't have to execute on the same CPU. + (The names are meant to be suggestive of operations on + semaphores.) Since the matching is determined by the domain + pointer and index value, these primitives make it possible for + an SRCU read-side critical section to start on one CPU and end + on another, so to speak. + +In order to account for these properties of SRCU, the LKMM models +srcu_read_lock() as a special type of load event (which is +appropriate, since it takes a memory location as argument and returns +a value, just as a load does) and srcu_read_unlock() as a special type +of store event (again appropriate, since it takes as arguments a +memory location and a value). These loads and stores are annotated as +belonging to the "srcu-lock" and "srcu-unlock" event classes +respectively. + +This approach allows the LKMM to tell whether two events are +associated with the same SRCU domain, simply by checking whether they +access the same memory location (i.e., they are linked by the loc +relation). It also gives a way to tell which unlock matches a +particular lock, by checking for the presence of a data dependency +from the load (srcu-lock) to the store (srcu-unlock). For example, +given the situation outlined earlier (with statement labels added): + + A: idx1 =3D srcu_read_lock(&s); + B: idx2 =3D srcu_read_lock(&s); + C: srcu_read_unlock(&s, idx1); + D: srcu_read_unlock(&s, idx2); + +the LKMM will treat A and B as loads from s yielding values saved in +idx1 and idx2 respectively. Similarly, it will treat C and D as +though they stored the values from idx1 and idx2 in s. The end result +is much as if we had written: + + A: idx1 =3D READ_ONCE(s); + B: idx2 =3D READ_ONCE(s); + C: WRITE_ONCE(s, idx1); + D: WRITE_ONCE(s, idx2); + +except for the presence of the special srcu-lock and srcu-unlock +annotations. You can see at once that we have A ->data C and +B ->data D. These dependencies tell the LKMM that C is the +srcu-unlock event matching srcu-lock event A, and D is the +srcu-unlock event matching srcu-lock event B. + +This approach is admittedly a hack, and it has the potential to lead +to problems. For example, in: + + idx1 =3D srcu_read_lock(&s); + srcu_read_unlock(&s, idx1); + idx2 =3D srcu_read_lock(&s); + srcu_read_unlock(&s, idx2); + +the LKMM will believe that idx2 must have the same value as idx1, +since it reads from the immediately preceding store of idx1 in s. +Fortunately this won't matter, assuming that litmus tests never do +anything with SRCU index values other than pass them to +srcu_read_unlock() or srcu_up_read() calls. + +However, sometimes it is necessary to store an index value in a +shared variable temporarily. In fact, this is the only way for +srcu_down_read() to pass the index it gets to an srcu_up_read() call +on a different CPU. In more detail, we might have soething like: + + struct srcu_struct s; + int x; + + P0() + { + int r0; + + A: r0 =3D srcu_down_read(&s); + B: WRITE_ONCE(x, r0); + } + + P1() + { + int r1; + + C: r1 =3D READ_ONCE(x); + D: srcu_up_read(&s, r1); + } + +Assuming that P1 executes after P0 and does read the index value +stored in x, we can write this (using brackets to represent event +annotations) as: + + A[srcu-lock] ->data B[once] ->rf C[once] ->data D[srcu-unlock]. + +The LKMM defines a carry-srcu-data relation to express this pattern; +it permits an arbitrarily long sequence of + + data ; rf + +pairs (that is, a data link followed by an rf link) to occur between +an srcu-lock event and the final data dependency leading to the +matching srcu-unlock event. carry-srcu-data is complicated by the +need to ensure that none of the intermediate store events in this +sequence are instances of srcu-unlock. This is necessary because in a +pattern like the one above: + + A: idx1 =3D srcu_read_lock(&s); + B: srcu_read_unlock(&s, idx1); + C: idx2 =3D srcu_read_lock(&s); + D: srcu_read_unlock(&s, idx2); + +the LKMM treats B as a store to the variable s and C as a load from +that variable, creating an undesirable rf link from B to C: + + A ->data B ->rf C ->data D. + +This would cause carry-srcu-data to mistakenly extend a data +dependency from A to D, giving the impression that D was the +srcu-unlock event matching A's srcu-lock. To avoid such problems, +carry-srcu-data does not accept sequences in which the ends of any of +the intermediate ->data links (B above) is an srcu-unlock event. =20 =20 LOCKING --=20 2.40.0.rc2 From nobody Mon Feb 9 00:55:34 2026 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by smtp.lore.kernel.org (Postfix) with ESMTP id B13E7C7618D for ; Tue, 21 Mar 2023 01:03:39 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229651AbjCUBDi (ORCPT ); Mon, 20 Mar 2023 21:03:38 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:47600 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229928AbjCUBDZ (ORCPT ); Mon, 20 Mar 2023 21:03:25 -0400 Received: from ams.source.kernel.org (ams.source.kernel.org [IPv6:2604:1380:4601:e00::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 7DD0230E9A; Mon, 20 Mar 2023 18:02:51 -0700 (PDT) Received: from smtp.kernel.org (relay.kernel.org [52.25.139.140]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ams.source.kernel.org (Postfix) with ESMTPS id 9F0D3B811BD; Tue, 21 Mar 2023 01:02:49 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 2F3E7C433A0; Tue, 21 Mar 2023 01:02:48 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1679360568; bh=Gt3XpPSB3ySvhPWXjtcOvUQMKgRg79fVOLRl2xXo2AM=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=WmMRp1zvPLOOAET9ARQLarM8Un0UWuP+RWngaMu+U9SIOvlrNfHi6JnrPrO8JX5d2 ir2brAZPqyWNdfzwMg9ReNIwr8Q9coxnpnYOB8PSWqqScVPaZTYeBQMfWTINy557fE 4lkA+0pjujw8ty3sSXuHGca15SKuzMn7JGXo5LcC/Sf/GD3GyFtXQRob/IOSfydSBe JvL2ugmkqOhhcNJNPWKX3A1IgiPFQmVi8mfxu0Zd2b+7xl6LuvlHGqxpGVlmSwF89P AYwWo2zhLjUMX3rwEvfAk+sWJVMimdqN85o+eq+dt0FBdfttc2IWtSQKN7nt11yr3w WMI5v97sM5yqw== Received: by paulmck-ThinkPad-P72.home (Postfix, from userid 1000) id 89A0215403A7; Mon, 20 Mar 2023 18:02:47 -0700 (PDT) From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, 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, Randy Dunlap , "Paul E. McKenney" , Jonathan Corbet , linux-doc@vger.kernel.org Subject: [PATCH memory-model 8/8] Documentation: litmus-tests: Correct spelling Date: Mon, 20 Mar 2023 18:02:46 -0700 Message-Id: <20230321010246.50960-8-paulmck@kernel.org> X-Mailer: git-send-email 2.40.0.rc2 In-Reply-To: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> MIME-Version: 1.0 Content-Transfer-Encoding: quoted-printable Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Type: text/plain; charset="utf-8" From: Randy Dunlap Correct spelling problems for Documentation/litmus-tests/ as reported by codespell. Signed-off-by: Randy Dunlap Cc: Alan Stern Cc: Andrea Parri Cc: Will Deacon Cc: Peter Zijlstra Cc: Boqun Feng Cc: Nicholas Piggin Cc: David Howells Cc: Jade Alglave Cc: Luc Maranget Cc: "Paul E. McKenney" Cc: linux-arch@vger.kernel.org Cc: Jonathan Corbet Cc: linux-doc@vger.kernel.org Reviewed-by: David Howells Signed-off-by: Paul E. McKenney --- Documentation/litmus-tests/README | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Documentation/litmus-tests/README b/Documentation/litmus-tests= /README index 7f5c6c3ed6c3..658d37860d39 100644 --- a/Documentation/litmus-tests/README +++ b/Documentation/litmus-tests/README @@ -9,7 +9,7 @@ a kernel test module based on a litmus test, please see tools/memory-model/README. =20 =20 -atomic (/atomic derectory) +atomic (/atomic directory) -------------------------- =20 Atomic-RMW+mb__after_atomic-is-stronger-than-acquire.litmus --=20 2.40.0.rc2