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 CF084C32793 for ; Wed, 18 Jan 2023 21:06:48 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S230314AbjARVGr (ORCPT ); Wed, 18 Jan 2023 16:06:47 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:35408 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S230318AbjARVGn (ORCPT ); Wed, 18 Jan 2023 16:06:43 -0500 Received: from dfw.source.kernel.org (dfw.source.kernel.org [IPv6:2604:1380:4641:c500::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 2F5985EF9B for ; Wed, 18 Jan 2023 13:06:43 -0800 (PST) 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 A78E761985 for ; Wed, 18 Jan 2023 21:06:42 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id 023EAC433D2; Wed, 18 Jan 2023 21:06:41 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1674076002; bh=HW/mdSWQSPYCTnuR5bMli1zWuIuU/FaraXxxcfaSjlE=; h=Date:From:To:Cc:Subject:Reply-To:References:In-Reply-To:From; b=B+rRVevPcxeDlD+WDvbFAbfswWm5YAH+HaDPsI/OyX5vueSCd/RFTRMIQsvhYQQXd wsYOkzcLgfqsfg9qIEu++6HhIDmWRD4yWKCM8CJVJZpS5cLbZfhdzj2qJBfacCWsTk u/5wLcZW6IZtyc0KavM1cRR2NKU2VJSdZmRTQIR7wfJD+z/QDUEYzlKkPuVgFj+4Ds KuECUl0MQ8qdMase3/yhp6YEos/ZnTXSg4OF8tzPszedzcn07y5e40REaDM+IZwX41 YNptR34+36cDQpUTyZoslameRv1M1ouWsY0M7VURW5x8IToIo8Z9ZxkogQlAmU06JL sJWWzM6rCztEA== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id 930885C0920; Wed, 18 Jan 2023 13:06:41 -0800 (PST) Date: Wed, 18 Jan 2023 13:06:41 -0800 From: "Paul E. McKenney" To: Jonas Oberhauser Cc: Alan Stern , 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: <20230118210641.GK2948950@paulmck-ThinkPad-P17-Gen-1> Reply-To: paulmck@kernel.org References: <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> <20230118035041.GQ2948950@paulmck-ThinkPad-P17-Gen-1> <73ff21ef-44fa-2dbf-cae0-f74077875502@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <73ff21ef-44fa-2dbf-cae0-f74077875502@gmail.com> Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Wed, Jan 18, 2023 at 08:57:22PM +0100, Jonas Oberhauser wrote: > > > On 1/18/2023 4:50 AM, Paul E. McKenney wrote: > > On Tue, Jan 17, 2023 at 03:15:06PM -0500, Alan Stern wrote: > > > 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. > > > As I understand it, given a relation r (i.e., a set of pairs of events), > > > different-values(r) returns the sub-relation consisting of those pairs > > > in r for which the value associated with the first event of the pair is > > > different from the value associated with the second event of the pair. > > OK, so different-values(r) is different than (r \ id) because the > > former operates on values and the latter on events? > > I think you can say that (if you allow yourself to be a little bit loose > with words, as I allow myself to be, much to the chagrin of Alan :) :( :)). Well, Alan's insistance on rigor has keep LKMM out of trouble more times than I can count. ;-) > If you had a .value functional relation that relates every event to the > value of that event, then >    different-values(r) = r \ .value ; .value^-1 > i.e., it relates events x and y iff: 1) r relates x and y, and 2) the value > of x is not equal to the value of y. > > You could write this as >    different-values(r) = r \ .value ; value-id ; .value^-1 > where value-id is like id but for values, i.e., relates every value v to > itself. > > You could say that this difference operates on the values of the events, > rather than on the events itself. > In contrast, >     r \ id > works directly on the events and relates x and y iff: 1) r relates x and y, > and 2) the event x is not equal to the event y. > > In this sense I think your characterization is appropriate. It looks to be "different domain values", but maybe I should just run some experiments. ;-) Thanx, Paul