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 3A1CBC05027 for ; Fri, 20 Jan 2023 21:37:35 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229542AbjATVhe (ORCPT ); Fri, 20 Jan 2023 16:37:34 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:46686 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229379AbjATVhd (ORCPT ); Fri, 20 Jan 2023 16:37:33 -0500 Received: from sin.source.kernel.org (sin.source.kernel.org [IPv6:2604:1380:40e1:4800::1]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id AFCA543914 for ; Fri, 20 Jan 2023 13:37:31 -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 sin.source.kernel.org (Postfix) with ESMTPS id DE4A6CE2AB6 for ; Fri, 20 Jan 2023 21:37:29 +0000 (UTC) Received: by smtp.kernel.org (Postfix) with ESMTPSA id EE4F5C433EF; Fri, 20 Jan 2023 21:37:27 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1674250648; bh=0DBSmP2vyNqu+oxytuTdeFsmN6xFvQcBg4PiuLnSEd8=; h=Date:From:To:Cc:Subject:Reply-To:References:In-Reply-To:From; b=IHDxRfuiZw/KNe5MEbpxwpw6kn57dkRVF0ZUgDRCs0kY7g5JaAy+dRMAI+J81c2BV bZHhoyvMERS68GIfJhuwzCGsiMSlg+KYzaG4/bF5HQzEPfSQa/QJlib7dlBKQyv5nv CJ7tq+BQW9C1sxogRGx2pgBUrlSboX6NJTuMzT1SzsbjhiZXyG1CVnUjZmrn7lOs1X x9RF1zEHOn+DFbo8lEkyT+HagjghNoURc61L1+zmnTMITMeIVc++kuh39JnJvFuqXD v3XKNladg7l4osnvH1y+rICs+ZhSqpg9gSca0HgrMbyZGxOhmxzXQD2jU4oa8Q+TtH ghvFP9YbMYIBg== Received: by paulmck-ThinkPad-P17-Gen-1.home (Postfix, from userid 1000) id 81DF15C08A4; Fri, 20 Jan 2023 13:37:27 -0800 (PST) Date: Fri, 20 Jan 2023 13:37:27 -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: <20230120213727.GX2948950@paulmck-ThinkPad-P17-Gen-1> Reply-To: paulmck@kernel.org References: <20230118211201.GL2948950@paulmck-ThinkPad-P17-Gen-1> <09f084d2-6128-7f83-b2a5-cbe236b1678d@huaweicloud.com> <20230119001147.GN2948950@paulmck-ThinkPad-P17-Gen-1> <0fae983b-2a7c-d44e-8881-53d5cc053f09@huaweicloud.com> <20230119184107.GT2948950@paulmck-ThinkPad-P17-Gen-1> <20230119215304.GA2948950@paulmck-ThinkPad-P17-Gen-1> <20230120153909.GF2948950@paulmck-ThinkPad-P17-Gen-1> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Fri, Jan 20, 2023 at 09:46:55PM +0100, Jonas Oberhauser wrote: > > > On 1/20/2023 4:39 PM, Paul E. McKenney wrote: > > On Fri, Jan 20, 2023 at 10:43:10AM +0100, Jonas Oberhauser wrote: > > > > > I don't think Boqun's patch is hard to repair. > > > Besides the issue you mention, I think it's also missing Sync-srcu, which > > > seems to be linked by loc based on its first argument. > > > > > > How about something like this? > > > > > > let ALL-LOCKS = LKR | LKW | UL | LF | RU | Srcu-lock | Srcu-unlock | > > > Sync-srcu flag ~empty ~[ALL_LOCKS | IW] ; loc ; [ALL-LOCKS] as > > > mixed-lock-accesses > > > > > > If you're using something that isn't a lock or intial write on the same location as a lock, you get the flag. > > Wouldn't that unconditionally complain about the first srcu_read_lock() > > in a given process? Or am I misreading those statements? > > > > I unfolded the definition step by step and it seems I was careless when > distributing the ~ over the [] operator. > I should have written: > > flag ~empty [~(ALL_LOCKS | IW)] ; loc ; [ALL-LOCKS] as mixed-lock-accesses > > but somehow I thought I can save the parentheses by putting the ~ on the > outside. > Now on the off-chance that this is kind of how you already read the > relation, let me unfold it step-by-step. > > Let's assume that the sequence s of operations on this location is >   s = initial write , (perhaps some gps) , first read lock , read > lock&unlock&gp ... > then the flag would appear if the specified relation isn't empty. That would > be the case if there are a and b that are linked by > > a ->[~(ALL_LOCKS | IW)] ; loc ; [ALL-LOCKS] b > > This means a is neither in ALL_LOCKS nor in IW, while b is ALL-LOCKS; and furthermore, they are equal to a' and b' resp. that are related by loc, i.e., appear in this sequence s. Thus both a and b are actually appearing both in the sequence s. > However, every event in the sequence s is either in ALL_LOCKS or in IW, which contradicts the assumption that a is in the sequence and in neither of the sets. Because of this contradiction, the flag doesn't appear if the sequence looks like this. > > More generally, if every event in the sequence is either the initial write or one of (srcu-) lock,unlock,up,down,sync, there won't be a flag. > > In contrast, if the sequence has the form > s' = initial write, (normal srcu events), some other acces x, (normal srcu events) > and y is one of the srcu events in this sequence, then > x ->[~(ALL_LOCKS | IW)] ; loc ; [ALL_LOCKS] y > and you get a flag. Thank you! When I get done messing with NMIs, I will give this a go. Just out of curiosity, are you sent up to run LKMM locally at your end? Thanx, Paul