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 6A6BDC54E94 for ; Wed, 25 Jan 2023 01:55:08 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S230510AbjAYBzG (ORCPT ); Tue, 24 Jan 2023 20:55:06 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:43528 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S230334AbjAYBzD (ORCPT ); Tue, 24 Jan 2023 20:55:03 -0500 Received: from netrider.rowland.org (netrider.rowland.org [192.131.102.5]) by lindbergh.monkeyblade.net (Postfix) with SMTP id D372D45F42 for ; Tue, 24 Jan 2023 17:54:57 -0800 (PST) Received: (qmail 192514 invoked by uid 1000); 24 Jan 2023 20:54:56 -0500 Date: Tue, 24 Jan 2023 20:54:56 -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: Re: Internal vs. external barriers (was: Re: Interesting LKMM litmus test) Message-ID: References: <20230124145423.GI2948950@paulmck-ThinkPad-P17-Gen-1> <8cc799ab-ffa1-47f7-6e1d-97488a210f14@huaweicloud.com> <20230124162253.GL2948950@paulmck-ThinkPad-P17-Gen-1> <3e5020c2-0dd3-68a6-9b98-5a7f57ed7733@huaweicloud.com> <20230124172647.GN2948950@paulmck-ThinkPad-P17-Gen-1> <2788294a-972e-acbc-84ce-25d2bb4d26d6@huaweicloud.com> <20230124221524.GV2948950@paulmck-ThinkPad-P17-Gen-1> <20230124225449.GY2948950@paulmck-ThinkPad-P17-Gen-1> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20230124225449.GY2948950@paulmck-ThinkPad-P17-Gen-1> Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Tue, Jan 24, 2023 at 02:54:49PM -0800, Paul E. McKenney wrote: > On Tue, Jan 24, 2023 at 05:35:33PM -0500, Alan Stern wrote: > > Can you be more explicit? Exactly what guarantees does the kernel > > implementation make that can't be expressed in LKMM? > > I doubt that I will be able to articulate it very well, but here goes. > > Within the Linux kernel, the rule for a given RCU "domain" is that if > an event follows a grace period in pretty much any sense of the word, > then that event sees the effects of all events in all read-side critical > sections that began prior to the start of that grace period. > > Here the senses of the word "follow" include combinations of rf, fr, > and co, combined with the various acyclic and irreflexive relations > defined in LKMM. The LKMM says pretty much the same thing. In fact, it says the event sees the effects of all events po-before the unlock of (not just inside) any read-side critical section that began prior to the start of the grace period. > > And are these anything the memory model needs to worry about? > > Given that several people, yourself included, are starting to use LKMM > to analyze the Linux-kernel RCU implementations, maybe it does. > > Me, I am happy either way. Judging from your description, I don't think we have anything to worry about. Alan