Received: by 2002:a05:6358:11c7:b0:104:8066:f915 with SMTP id i7csp6189904rwl; Wed, 22 Mar 2023 07:36:43 -0700 (PDT) X-Google-Smtp-Source: AK7set+STTIwQpz97pQwfPTKVRZJTZfBgo24h/C8XTDZoHOUNMyFhH/nYK5k32KjOlGXi0Ensb5+ X-Received: by 2002:a17:90b:4d11:b0:22c:afd6:e597 with SMTP id mw17-20020a17090b4d1100b0022cafd6e597mr4069708pjb.17.1679495802941; Wed, 22 Mar 2023 07:36:42 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1679495802; cv=none; d=google.com; s=arc-20160816; b=ylzneacUaWJ/GrcrUIeyYopFDyfTdsscieXh5QG3uRAvbyrlEQKwl1eUGXRf89dbqd OKeR4focythvBFBsWZKX+eAS0X5dyjJgEFacidEyzTWlbDxq6dlxSajMobirO4OACRYS eJXULs1xwFrR81mLZg8+xyxtF2baqyx10l21BVl3kMmrB3QnawDGGp2zBVJoEby7d8NC NdP6jYRtPmhxH0+Lsxp67M/ESn/ZDe8EEjmHleT1mF6n++AO/n+sdigni/wKZ6hcjHkR BDfMbW8kcWh7OE95VP73b6rgibpz+lz9/JUQ+m+/D0tyrLmW6h38htF4Twxz+bHL9u8J oUgw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:in-reply-to:content-disposition:mime-version :references:message-id:subject:cc:to:from:date; bh=PHnDjOmXjlQaGagkbG49WaerPG0DucisYDyn0GSNc44=; b=jAmCBur1FIxJ8amYvWdK6AgP4DfvybvPqAKWjZhpsqmDJ2Jbx6CyyVQAvKpnWREh90 Jkc8YHhcI4SBcKIecqTM7rD+iwtehVh8HONXRcxxq34Cmm/VfVhQnzEN1HEHplD/qh5Z b80CmxS64SjKC33uXZOXq6oOobhlJ/HMJ1SOXxhFRoEplMNpBze5/Xmw4GLjqOq2DHik ouVjqklp/YR3P3JGjYXST52At+h0XpHnqvA3dDUAJSb2E8pMti4aDvGQwJusxKlZhTAi FgeBeMv45hLJSdOkhaG/ObfZL46gtYGiJxqtN5GrWmBJvMr6yG84LcVs2rs6/orVP74M URyg== ARC-Authentication-Results: i=1; mx.google.com; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Return-Path: Received: from out1.vger.email (out1.vger.email. [2620:137:e000::1:20]) by mx.google.com with ESMTP id f23-20020a17090ac29700b0023f5ee62c13si15311829pjt.179.2023.03.22.07.36.31; Wed, 22 Mar 2023 07:36:42 -0700 (PDT) Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20; Authentication-Results: mx.google.com; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S231446AbjCVObD (ORCPT + 99 others); Wed, 22 Mar 2023 10:31:03 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:47182 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S231464AbjCVObB (ORCPT ); Wed, 22 Mar 2023 10:31:01 -0400 Received: from netrider.rowland.org (netrider.rowland.org [192.131.102.5]) by lindbergh.monkeyblade.net (Postfix) with SMTP id 5C99D64B11 for ; Wed, 22 Mar 2023 07:30:58 -0700 (PDT) Received: (qmail 1103384 invoked by uid 1000); 22 Mar 2023 10:30:57 -0400 Date: Wed, 22 Mar 2023 10:30:57 -0400 From: Alan Stern To: Andrea Parri Cc: "Paul E. McKenney" , linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, kernel-team@meta.com, mingo@kernel.org, will@kernel.org, peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, akiyks@gmail.com, Joel Fernandes , Andrea Parri , Jonas Oberhauser , "Paul E. McKenney" Subject: Re: [PATCH memory-model 7/8] tools/memory-model: Add documentation about SRCU read-side critical sections Message-ID: <4599c0d4-6c2a-431f-8bf3-173855c7ba77@rowland.harvard.edu> References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop> <20230321010246.50960-7-paulmck@kernel.org> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: X-Spam-Status: No, score=0.2 required=5.0 tests=HEADER_FROM_DIFFERENT_DOMAINS, SPF_HELO_PASS,SPF_PASS autolearn=no autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on lindbergh.monkeyblade.net Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Wed, Mar 22, 2023 at 02:40:52AM +0100, Andrea Parri wrote: > On Mon, Mar 20, 2023 at 06:02:45PM -0700, Paul E. McKenney wrote: > > From: Alan Stern > > > > Expand the discussion of SRCU and its read-side critical sections in > > the Linux Kernel Memory Model documentation file explanation.txt. The > > new material discusses recent changes to the memory model made in > > commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU > > semantics"). > > How about squashing the diff below (adjusting subject and changelog): > > Andrea > > diff --git a/tools/memory-model/Documentation/litmus-tests.txt b/tools/memory-model/Documentation/litmus-tests.txt > index 26554b1c5575e..acac527328a1f 100644 > --- a/tools/memory-model/Documentation/litmus-tests.txt > +++ b/tools/memory-model/Documentation/litmus-tests.txt > @@ -1028,32 +1028,7 @@ Limitations of the Linux-kernel memory model (LKMM) include: > additional call_rcu() process to the site of the > emulated rcu-barrier(). > > - e. Although sleepable RCU (SRCU) is now modeled, there > - are some subtle differences between its semantics and > - those in the Linux kernel. For example, the kernel > - might interpret the following sequence as two partially > - overlapping SRCU read-side critical sections: > - > - 1 r1 = srcu_read_lock(&my_srcu); > - 2 do_something_1(); > - 3 r2 = srcu_read_lock(&my_srcu); > - 4 do_something_2(); > - 5 srcu_read_unlock(&my_srcu, r1); > - 6 do_something_3(); > - 7 srcu_read_unlock(&my_srcu, r2); > - > - In contrast, LKMM will interpret this as a nested pair of > - SRCU read-side critical sections, with the outer critical > - section spanning lines 1-7 and the inner critical section > - spanning lines 3-5. > - > - This difference would be more of a concern had anyone > - identified a reasonable use case for partially overlapping > - SRCU read-side critical sections. For more information > - on the trickiness of such overlapping, please see: > - https://paulmck.livejournal.com/40593.html > - > - f. Reader-writer locking is not modeled. It can be > + e. Reader-writer locking is not modeled. It can be > emulated in litmus tests using atomic read-modify-write > operations. Excellent suggestion! Acked-by: Alan Stern Alan