From mboxrd@z Thu Jan 1 00:00:00 1970 Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.remote-ip=100.103.45.18 ARC-Seal: i=1; d=subspace.kernel.org; s=arc20261015; a=rsa-sha256; cv=none; t=1794531472; b=4wCNGhjN5cP5YBfGkn8x998vLVVfK/sKR2wE4NwmNtTV2LdwQdUqpNK9QrOeqyYSISNL 6XbjlINozB3WoXkoqfRHd+iu3uLP1e6DXBvCMQMevWOyA+6k/tfonFSKFIRigPhzyXjbI gRSkbspw+sgzLs2n3XHbQ+r/u7625PlW+uZ5aUO+lwBG6bYBKUEpcoF7lelR58zhwAi29 TCvuO2azYMNT9FJxy1dzSrXOVuBSAkR737GOEOvKXq0ZGU0IsPDI/iDSoguUbSR3eFBw/ DH3Cg5SApU0d4hon9FXoRBrvNMvgiHmlC3AdAMRFnqLSLUTWyzQL5edMwnFUCU0NzqA== ARC-Message-Signature: i=1; d=subspace.kernel.org; s=arc20261015; a=rsa-sha256; c=relaxed/relaxed; t=1794531472; h=Received:DKIM-Signature:From:To:Cc:Subject:Date:Message-ID:X-Mailer: In-Reply-To:References:MIME-Version:Content-Transfer-Encoding; bh=MwbiE1ZOKIvrDWVu+QsX7ujXMHiuFxF8hJmcEZbi4j0=; b=TNODnUX+7EUa78HbfrOLFiEJzcro1KN89t+TjKB6nT0+lj8gnsDablnAHiwcsJyY6Lz9 GZlVYs+oFFkSwQ2Eh05NETYCUJCNVmoMkmmbivJC+opTfLe5FSwROEifGXlzngkwOAEEj Ng2bdnZce0G7M8yzgp6saPdTBBSAuWTokcZzBSOlAn5W21Yl48UuExB/spiy8UYyo0iAw BcdNX9B29djNkk98wlGV1tSZxqSfMtP/Niv0COxsx08v8rmHveqKgEkwAPbxgvsHTm9gA XdM4yiKU+JwIMlszO+0c5layGf7+tj1OahZbmMS/PwO7Q2vT3JNFHJ35dLKKImIu1lg== ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dkim=pass header.d=kernel.org header.i=@kernel.org header.a=rsa-sha256 header.s=k20260515 header.b=hodfwfsD; arc=none smtp.remote-ip=100.103.45.18 Received: from smtp.kernel.org (quasi.space.kernel.org [100.103.45.18]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature ECDSA (prime256v1)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with UTF8SMTPS id C67FF606A337; Fri, 13 Nov 2026 00:57:52 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=kernel.org header.i=@kernel.org header.a=rsa-sha256 header.s=k20260515 header.b=hodfwfsD Received: by smtp.kernel.org (Postfix) with UTF8SMTPSA id 056381F000C5; Fri, 13 Nov 2026 00:57:52 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=kernel.org; s=k20260515; t=1794531472; bh=MwbiE1ZOKIvrDWVu+QsX7ujXMHiuFxF8hJmcEZbi4j0=; h=From:To:Cc:Subject:Date:In-Reply-To:References; b=hodfwfsD8lWZOjkALBKE6tyIStPF567e9XkBvYB2HRv52fgKWMGuy61PGinL0K0rx dQcDueubf5T1alKaXwNodPjvquI9YMdA7l7Dv1vCJLRA7rCDDMrTdIssSofb/I1GIS Ad2b1k2CbNH7lXNP+IDYbbQyXJPMWJoPivv8wfyk1SDA+VUUsf2d8qT57JJSbxE/d7 GOnFJTJfqZSypDeOdUgHfPThbiJH4yfRHPNnY3ytoWr3T4qmiWMWh7tw6V/ON4M7hW lHfcbLQCLWOOhNOAkqw3+ERQ8N2MEbBAJZpsVPHmh0YiNhOZejHjj7Muv8wzNuRQ9a efedSp6t37Aiw== From: Joel Fernandes To: linux-kernel@vger.kernel.org, "Paul E . McKenney" , Frederic Weisbecker , Neeraj Upadhyay , Joel Fernandes , Josh Triplett , Boqun Feng , Uladzislau Rezki , Steven Rostedt , Mathieu Desnoyers , Lai Jiangshan , Zqiang , Alan Stern , Andrea Parri , Will Deacon , Peter Zijlstra , Nicholas Piggin , David Howells , Jade Alglave , Luc Maranget , Akira Yokosawa , Daniel Lustig , Jonathan Corbet , Shuah Khan , Randy Dunlap Cc: rcu@vger.kernel.org, Kunwu Chan , linux-arch@vger.kernel.org, lkmm@lists.linux.dev, linux-doc@vger.kernel.org Subject: [PATCH for-v7.5 01/14] Documentation/litmus-tests: Add SRCU fastpath anchor-before-scan test Date: Thu, 12 Nov 2026 19:57:28 -0500 Message-ID: <20261113005747.2977123-2-jfern@kernel.org> X-Mailer: git-send-email 2.54.0 In-Reply-To: <20261113005747.2977123-1-jfern@kernel.org> References: <20261113005747.2977123-1-jfern@kernel.org> X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Post: List-Help: List-Subscribe: List-Unsubscribe: List-Owner: Precedence: list MIME-Version: 1.0 Content-Transfer-Encoding: 8bit From: Kunwu Chan synchronize_srcu_atomic() may end its grace period immediately when its scan of the per-CPU lock counters finds no readers. Correctness requires the grace-period anchor written by srcu_gp_start() to precede the smp_mb() ordering the lock scan. This ordering ensures that any reader whose lock increment is missed by the scan cannot have incremented its lock counter before the grace-period anchor, and therefore cannot be a pre-existing reader of this grace period. This litmus test models the key ordering between the grace-period anchor and the lock counter scan, where "seq" models the grace-period anchor in ->srcu_gp_seq and "ctr" models the per-CPU ->srcu_ctrs[].srcu_locks counter. P0 writes the anchor before the smp_mb() and the lock scan. P1 models the reader-side counter increment. P2 models an observer that sees the reader's increment before seeing the anchor. The outcome is forbidden by LKMM, and herd7 reports "Never". See SRCU-fastpath-scan-before-anchor.litmus for the reversed ordering, which permits this outcome. Tested with herd7 7.58 using linux-kernel.cfg. Signed-off-by: Kunwu Chan Signed-off-by: Paul E. McKenney Signed-off-by: Joel Fernandes --- .../SRCU-fastpath-anchor-before-scan.litmus | 55 +++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 Documentation/litmus-tests/srcu/SRCU-fastpath-anchor-before-scan.litmus diff --git a/Documentation/litmus-tests/srcu/SRCU-fastpath-anchor-before-scan.litmus b/Documentation/litmus-tests/srcu/SRCU-fastpath-anchor-before-scan.litmus new file mode 100644 index 000000000000..8028f2ade733 --- /dev/null +++ b/Documentation/litmus-tests/srcu/SRCU-fastpath-anchor-before-scan.litmus @@ -0,0 +1,55 @@ +C SRCU-fastpath-anchor-before-scan + +(* + * Result: Never + * + * The synchronize_srcu_atomic() fastpath may end its grace period + * immediately when its scan of the per-CPU lock counters finds no + * readers. Correctness requires the grace-period anchor written by + * srcu_gp_start() to precede the smp_mb() ordering the lock scan. + * This ordering ensures that any reader whose lock increment is missed + * by the scan cannot have incremented its lock counter before the + * grace-period anchor, and therefore cannot be a pre-existing reader + * of this grace period. + * + * This litmus test models the key ordering between the grace-period + * anchor and the lock counter scan, where "seq" models the + * grace-period anchor in ->srcu_gp_seq and "ctr" models the per-CPU + * ->srcu_ctrs[].srcu_locks counter. P0 writes the anchor before the + * smp_mb() and the lock scan. P1 models the reader-side counter + * increment. P2 models an observer that sees the reader's increment + * before seeing the anchor. + * + * The outcome is forbidden by LKMM, and herd7 reports "Never". See + * SRCU-fastpath-scan-before-anchor.litmus for the reversed ordering, + * which permits this outcome. + *) + +{} + +P0(int *seq, int *ctr) +{ + int r2; + + WRITE_ONCE(*seq, 1); + smp_mb(); + r2 = READ_ONCE(*ctr); +} + +P1(int *ctr) +{ + WRITE_ONCE(*ctr, 1); +} + +P2(int *seq, int *ctr) +{ + int r3; + int r4; + + r3 = READ_ONCE(*ctr); + smp_mb(); + r4 = READ_ONCE(*seq); +} + +filter (0:r2 = 0) +exists (2:r3 = 1 /\ 2:r4 = 0) -- 2.54.0