From nobody Sun Sep 14 07:35:39 2025 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 A2469C54E94 for ; Wed, 25 Jan 2023 20:20:55 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S235942AbjAYUUy (ORCPT ); Wed, 25 Jan 2023 15:20:54 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:54306 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S235541AbjAYUUx (ORCPT ); Wed, 25 Jan 2023 15:20:53 -0500 Received: from netrider.rowland.org (netrider.rowland.org [192.131.102.5]) by lindbergh.monkeyblade.net (Postfix) with SMTP id 4A1D758972 for ; Wed, 25 Jan 2023 12:20:52 -0800 (PST) Received: (qmail 225322 invoked by uid 1000); 25 Jan 2023 15:20:51 -0500 Date: Wed, 25 Jan 2023 15:20:51 -0500 From: Alan Stern To: "Paul E. McKenney" Cc: Jonas Oberhauser , Andrea Parri , Jonas Oberhauser , Peter Zijlstra , will , "boqun.feng" , npiggin , dhowells , "j.alglave" , "luc.maranget" , akiyks , dlustig , joel , urezki , quic_neeraju , frederic , Kernel development list Subject: [Patch 1/2] tools/memory-model: Update some warning labels Message-ID: References: MIME-Version: 1.0 Content-Disposition: inline In-Reply-To: Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset="utf-8" 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 --- tools/memory-model/linux-kernel.bell | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) Index: usb-devel/tools/memory-model/linux-kernel.bell =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D --- usb-devel.orig/tools/memory-model/linux-kernel.bell +++ usb-devel/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) |