From mboxrd@z Thu Jan 1 00:00:00 1970 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 B3054C38142 for ; Wed, 18 Jan 2023 02:15:21 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229754AbjARCPU (ORCPT ); Tue, 17 Jan 2023 21:15:20 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:49558 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229525AbjARCPR (ORCPT ); Tue, 17 Jan 2023 21:15:17 -0500 Received: from netrider.rowland.org (netrider.rowland.org [192.131.102.5]) by lindbergh.monkeyblade.net (Postfix) with SMTP id 88A0D51C66 for ; Tue, 17 Jan 2023 18:15:16 -0800 (PST) Received: (qmail 190654 invoked by uid 1000); 17 Jan 2023 21:15:15 -0500 Date: Tue, 17 Jan 2023 21:15:15 -0500 From: Alan Stern To: "Paul E. McKenney" Cc: 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: Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) Message-ID: References: <20230116042329.GN2948950@paulmck-ThinkPad-P17-Gen-1> <20230116190652.GZ2948950@paulmck-ThinkPad-P17-Gen-1> <20230116221357.GA2948950@paulmck-ThinkPad-P17-Gen-1> <20230117151416.GI2948950@paulmck-ThinkPad-P17-Gen-1> <20230117174308.GK2948950@paulmck-ThinkPad-P17-Gen-1> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20230117174308.GK2948950@paulmck-ThinkPad-P17-Gen-1> Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Tue, Jan 17, 2023 at 09:43:08AM -0800, Paul E. McKenney wrote: > On Tue, Jan 17, 2023 at 10:56:34AM -0500, Alan Stern wrote: > > Isn't it true that the current code will flag srcu-bad-nesting if a > > litmus test has non-nested overlapping SRCU read-side critical sections? > > Now that you mention it, it does indeed, flagging srcu-bad-nesting. > > Just to see if I understand, different-values yields true if the set > contains multiple elements with the same value mapping to different > values. Or, to put it another way, if the relation does not correspond > to a function. > > Or am I still missing something? > > > And if it is true, is there any need to change the memory model at this > > point? > > > > (And if it's not true, that's most likely due to a bug in herd7.) > > Agreed, changes must wait for SRCU support in herd7. Maybe we don't. Please test the patch below; I think it will do what you want -- and it doesn't rule out nesting. Alan Index: usb-devel/tools/memory-model/linux-kernel.bell =================================================================== --- usb-devel.orig/tools/memory-model/linux-kernel.bell +++ usb-devel/tools/memory-model/linux-kernel.bell @@ -57,20 +57,12 @@ flag ~empty Rcu-lock \ domain(rcu-rscs) flag ~empty Rcu-unlock \ range(rcu-rscs) as unbalanced-rcu-locking (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *) -let srcu-rscs = let rec - unmatched-locks = Srcu-lock \ domain(matched) - and unmatched-unlocks = Srcu-unlock \ range(matched) - and unmatched = unmatched-locks | unmatched-unlocks - and unmatched-po = ([unmatched] ; po ; [unmatched]) & loc - and unmatched-locks-to-unlocks = - ([unmatched-locks] ; po ; [unmatched-unlocks]) & loc - and matched = matched | (unmatched-locks-to-unlocks \ - (unmatched-po ; unmatched-po)) - in matched +let srcu-rscs = ([Srcu-lock] ; data ; [Srcu-unlock]) & loc (* 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-unlock \ range(srcu-rscs) as unbalanced-srcu-unlocking +flag ~empty (srcu-rscs^-1 ; srcu-rscs) \ id as multiple-srcu-unlocks (* Check for use of synchronize_srcu() inside an RCU critical section *) flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep @@ -80,11 +72,11 @@ flag ~empty different-values(srcu-rscs) (* Compute marked and plain memory accesses *) let Marked = (~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 = M \ Marked (* Redefine dependencies to include those carried through plain accesses *) -let carry-dep = (data ; rfi)* +let carry-dep = (data ; rfi ; [~Srcu-lock])* let addr = carry-dep ; addr let ctrl = carry-dep ; ctrl let data = carry-dep ; data Index: usb-devel/tools/memory-model/linux-kernel.def =================================================================== --- usb-devel.orig/tools/memory-model/linux-kernel.def +++ usb-devel/tools/memory-model/linux-kernel.def @@ -49,8 +49,8 @@ synchronize_rcu() { __fence{sync-rcu}; } synchronize_rcu_expedited() { __fence{sync-rcu}; } // 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); } synchronize_srcu(X) { __srcu{sync-srcu}(X); } synchronize_srcu_expedited(X) { __srcu{sync-srcu}(X); }