From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail-pl1-f172.google.com (mail-pl1-f172.google.com [209.85.214.172]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 8ACAA41DEF7 for ; Mon, 7 Sep 2026 07:58:49 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.214.172 ARC-Seal:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1788767931; cv=none; b=lRlxLGWqmRxLR6te4drsxfFxFHXVX5baxuFVIWpUo5Zs4DjwfT5jYHwp1wnJT0N8q6NSMUwKl/CMagD/RLcFq1WMenx8pChxVpMiJ9uNqCKg84FiyjXLgl6EiBbUuaPtAw2SzYHhR2XWCkhZS4eRcrsJOG5XN9OKzcjunOIjVfA= ARC-Message-Signature:i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1788767931; c=relaxed/simple; bh=TCCpXwnmodeVmKo1E6y7S918XFzRwDxpNrXxJ9AKFVc=; h=From:To:Cc:Subject:Date:Message-ID:In-Reply-To:References: MIME-Version; b=QKelLs9A5ngp4MtJkaSeAT/65IsOF8wbqrYuTJ+TnH3dJO6fYoG53PnTf88oW17le/9TaSsEnoCOyFqT4NmRFeLNuIv4K0IkAloId9WK6TP4FvJwVBX3jcrdoAWUbCvJ/LTVLuz5agJ+6YGnNdNyUsjmxuNPsa4t4x4VyLfOHYk= ARC-Authentication-Results:i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com; spf=pass smtp.mailfrom=gmail.com; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b=SG1bOGsB; arc=none smtp.client-ip=209.85.214.172 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=gmail.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b="SG1bOGsB" Received: by mail-pl1-f172.google.com with SMTP id d9443c01a7336-2d6d28aa26cso18961335ad.2 for ; Mon, 07 Sep 2026 00:58:48 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20251104; t=1788767927; x=1789372727; darn=vger.kernel.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to:content-type; bh=kkKaVITt+/rz08+YgC0jvTu5c22naN5LQ082iYcixrU=; b=SG1bOGsBqe8CnfPDXvaR6Qj4r+mDvEJoZMa9O2M+gLVJ7ZY2308DAh0NvCM4ntJMW/ j1ugl2zMkmizJtVEr4fQQZNRUaqikpEFbYIvsG9X+rZt94v6ZZBATyNFfhsKcmgvK7H6 yBGOHkrIENzwALIheKqd0lsRh6pmnXLonLqARhh8UoXgb28NODO/rLYOrBTXqV2uF2wl j7CXxx6bB7ME2nVGDegZCdbpcsF0Q+l1tgmZ2aLoLfrB9uDPCvTUJun/9KoZjHJngbfD Xbf9E9o0L3VimHI3Y/MHJcwhTuzCHli++grhfDm2OE8D6+IO4sK23who2PQF4eVce3AK m1KA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1788767927; x=1789372727; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-gg:x-gm-message-state:from :to:cc:subject:date:message-id:reply-to:content-type; bh=kkKaVITt+/rz08+YgC0jvTu5c22naN5LQ082iYcixrU=; b=X/Zpb5z19YeoG2e0PpU4gP8qCR+AGSk8Cj8/N+qNcBvpLlRVnkhZvpZwdK4M+n070E 35RTP7zF1is/OvCAmBgZu2kvSx4Pi3T3OZkI8sEe9gwNEXQGKzCNQEtpcaPIlYAU3Yse 2ibApcf6zJXfqKYMSOgp764ybyaA5x/h+3mikIKmvcSs9a86jElVD7O9xwOMB/aaYOqB PI+oo1Dewsr45gLh5N4UDKTwqETFLea8ntji4A76a4jU7XpnU1f8NPzHYwTf+xR8VQOl i9TrETXRmaZq65fgFTVZ1sF/7ufBZPc1tivyE+C4ro1si1audEh379eneFiLCNyOMLRT RRDQ== X-Forwarded-Encrypted: i=1; AKwUvBw4nIIjiRvgRyf2Uj30mF29mJTL6wL1wqsd4eaQ8GfBU8oUSGeXMWhjTf1byN3G5msMzUFbemCA27cRHaI=@vger.kernel.org X-Gm-Message-State: AFuF++llLw3rf1ciZOi71MW6MRmxibrAP3n1y+Fgi1ap8++OyzMDrtwq 4WU3SLALMzLLb0TPTWkwzLbFTVrooAqS59KkPI0/ySYjlfQyV797sq4p X-Gm-Gg: AYBFou200TcEPgGzJzsjBxpTspZnc2rjCGp57oL4aXaS163tXK/8wLY4bL4Ns6QwU9d 6wXFTylc0FIx6wQxe1WSInP3j9SLSD/KFloD1KEaLVp1dzoKPgDp7HExNoIC1oiKzpBiREIUJzb ClHcYKAtgPOsWFsKmKhwtR5QTnb5kSuBmVG6VXlAnC9esXTm60Mwa/jA2GbHb/HPiy9077QYnhE qZO0CQ+8zSjXGxOvygE4Dvlm6FNoY3Q1bo+w7kSo1knwtFcaKkB3fFVCvITB5G0uowPs+cqc2v+ 7rh4j90MKsjkw3TuZMEkEsvyeJDbTFvbDsnFXUtV2tm1+QjoIJ1dvYtpWbWTbqxEpOhpdYMsH9x keL5zE5As0yTNAWppymyZzpEapLCiCzcRQvGL/L4q2U7BQWRVU34TcZL2ELlXmA6xN8bQkq3zzF sN6gpu00HakdnDERY0G+sylctiw4wLM8tDhGrK3LdqWD6BdGqd/jr0vzewX/aiJnRpo8ChGRZRx eRTZhgw X-Received: by 2002:a17:903:2383:b0:2d8:d4ce:9f35 with SMTP id d9443c01a7336-2db12757af4mr288425665ad.19.1788767926938; Mon, 07 Sep 2026 00:58:46 -0700 (PDT) Received: from kernel.tail6741c6.ts.net ([185.220.238.35]) by smtp.gmail.com with ESMTPSA id d9443c01a7336-2db14ae7637sm40945595ad.79.2026.09.07.00.58.42 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 07 Sep 2026 00:58:46 -0700 (PDT) From: Kunwu Chan X-Google-Original-From: Kunwu Chan To: paulmck@kernel.org, jiangshanlai@gmail.com, josh@joshtriplett.org Cc: rostedt@goodmis.org, mathieu.desnoyers@efficios.com, rcu@vger.kernel.org, linux-kernel@vger.kernel.org, Kunwu Chan Subject: [PATCH 01/13] litmus: Add SRCU fastpath anchor-before-scan test Date: Mon, 7 Sep 2026 15:58:17 +0800 Message-ID: <20260907075829.2073224-2-kunwu.chan@linux.dev> X-Mailer: git-send-email 2.43.0 In-Reply-To: <20260907075829.2073224-1-kunwu.chan@linux.dev> References: <20260907075829.2073224-1-kunwu.chan@linux.dev> Precedence: bulk X-Mailing-List: linux-kernel@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: 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, with the smp_mb() of __srcu_read_lock() following the 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 --- .../SRCU-fastpath-anchor-before-scan.litmus | 56 +++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus diff --git a/tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus b/tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus new file mode 100644 index 000000000000..8200a75e15ef --- /dev/null +++ b/tools/memory-model/litmus-tests/SRCU-fastpath-anchor-before-scan.litmus @@ -0,0 +1,56 @@ +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, with the smp_mb() of __srcu_read_lock() following the + * 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); + smp_mb(); +} + +P2(int *seq, int *ctr) +{ + int r3; + int r4; + + r3 = READ_ONCE(*ctr); + smp_mb(); + r4 = READ_ONCE(*seq); +} + +exists (0:r2 = 0 /\ 2:r3 = 1 /\ 2:r4 = 0) -- 2.43.0