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 188CDC54EBE for ; Mon, 16 Jan 2023 19:21:05 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S233043AbjAPTVD (ORCPT ); Mon, 16 Jan 2023 14:21:03 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:41076 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S232415AbjAPTU7 (ORCPT ); Mon, 16 Jan 2023 14:20:59 -0500 Received: from netrider.rowland.org (netrider.rowland.org [192.131.102.5]) by lindbergh.monkeyblade.net (Postfix) with SMTP id 27751524F for ; Mon, 16 Jan 2023 11:20:57 -0800 (PST) Received: (qmail 137219 invoked by uid 1000); 16 Jan 2023 14:20:57 -0500 Date: Mon, 16 Jan 2023 14:20:57 -0500 From: Alan Stern To: "Paul E. McKenney" Cc: Jonas Oberhauser , Peter Zijlstra , "parri.andrea" , 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: <20230114175343.GF2948950@paulmck-ThinkPad-P17-Gen-1> <20230114181537.GA493203@paulmck-ThinkPad-P17-Gen-1> <20230115051510.GG2948950@paulmck-ThinkPad-P17-Gen-1> <20230115181052.GJ2948950@paulmck-ThinkPad-P17-Gen-1> <20230116042329.GN2948950@paulmck-ThinkPad-P17-Gen-1> <20230116190652.GZ2948950@paulmck-ThinkPad-P17-Gen-1> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <20230116190652.GZ2948950@paulmck-ThinkPad-P17-Gen-1> Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Mon, Jan 16, 2023 at 11:06:52AM -0800, Paul E. McKenney wrote: > On Mon, Jan 16, 2023 at 01:11:41PM -0500, Alan Stern wrote: > > Why do you want to prohibit nesting? Why would that be a better > > approximation? > > Because the current LKMM gives wrong answers for nested critical > sections. I don't agree. Or at least, it depends on whose definition of "nested critical sections" you adopt. > For example, for the litmus test shown below, mainline > LKMM will incorrectly report "Never". The two SRCU read-side critical > sections are independent, so the fact that P1()'s synchronize_srcu() is > guaranteed to wait for the first on to complete says nothing about the > second having completed. Therefore, in Linux-kernel SRCU, the "exists" > clause could be satisfied. > > In contrast, the proposed change flags this as having nesting. In fact, this litmus test has overlapping critical sections, not nested ones. But the current LKML incorrectly _thinks_ they are nested, because it matches each lock with the first unmatched unlock. If you write a litmus test that has properly nested (not overlapping!) read-side critical sections, the current LKMM will match the locks and unlocks correctly and will give the right answer. So what you really want to do is rule out overlapping, not nesting. But I guess there's no way to do one without the other. Alan > Thaxn, Paul > > ------------------------------------------------------------------------ > > C C-srcu-nest-5 > > (* > * Result: Sometimes > * > * This demonstrates non-nesting of SRCU read-side critical sections. > * Unlike RCU, SRCU critical sections do not nest. > *) > > {} > > P0(int *x, int *y, struct srcu_struct *s1) > { > int r1; > int r2; > int r3; > int r4; > > r3 = srcu_read_lock(s1); > r2 = READ_ONCE(*y); > r4 = srcu_read_lock(s1); > srcu_read_unlock(s1, r3); > r1 = READ_ONCE(*x); > srcu_read_unlock(s1, r4); > } > > P1(int *x, int *y, struct srcu_struct *s1) > { > WRITE_ONCE(*y, 1); > synchronize_srcu(s1); > WRITE_ONCE(*x, 1); > } > > locations [0:r1] > exists (0:r1=1 /\ 0:r2=0)