From patchwork Mon Feb 13 01:55:06 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Joel Fernandes X-Patchwork-Id: 55994 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:adf:eb09:0:0:0:0:0 with SMTP id s9csp2128769wrn; Sun, 12 Feb 2023 17:56:48 -0800 (PST) X-Google-Smtp-Source: AK7set9n6vmRsApmyEz/t6/dCn1z868yma0FCjN7q3ScHWmhIqyT0TcX/2QkeJ/AgsjDEs96pqGF X-Received: by 2002:a50:cd41:0:b0:4ac:c81d:149e with SMTP id d1-20020a50cd41000000b004acc81d149emr1350200edj.40.1676253408596; Sun, 12 Feb 2023 17:56:48 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1676253408; cv=none; d=google.com; s=arc-20160816; b=ri2XNuji0HOCUSRi3rGnfIBN75zaK6cBsN5ydygF0cGlPqVe/yG+YAmJz5jwejnZ0Z KzM75OxXb4bIAGiHMyS9XGFxnBHuusihmVnPZMOJADkLVt8MFwiMwhXBiEGJzXiSvmN/ yDqzAko0mJ/u8eVujZSjaFe3CbkoaNWfnVyDgybDLi2b9rxX8cLY1hLchRjkRY8p2KEE 9nTUR5A0MQ9tuOGeoG273MJkorOlwpy2cCNHdWJxT6uT9xUi5B49KS/3tjdbwKNgv8Pr ckvo1ILujMKM0tABMGqH/3i/qayVPhfPncz1eKRyoupYlF59WNzWT/+TcCAX+9oKv7Xp 4kTg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:content-transfer-encoding:mime-version :message-id:date:subject:cc:to:from:dkim-signature; bh=xfWgFky8Oo0dLRgocQgSyLFVq1vdjV8IYOHij7ANhkk=; b=WfycQ1jEv94MJ+4khrdaOMM6Bds3LQl3wKSC+Zkh3IvexT24cCsQhq44pGY8NXay8Y Ki6pGrT+tg4Pt+z85DpMRifWeyJGUdgRFtY1Cp83Ji1AsrK6zveRzttFIpGEQsHWH91O yKM57V00l1fSaOEMwgJaeorl4EV65RE87DM94/RS4NEPHhVHNTkctKVrm1fhD/568+xo uox5E5luPHoLTio1hYRZFxJrZZdsj3mvAtJ1jCY+Cfk2lv+EwoOY2XAwojz1LfNetZ+5 T0z8DSp7GGB9hIvo5TdswWabeU7ySwm0K4NnsoLcolKYws1DGGGjFm3qnmTjT16SbGxE sOrw== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@joelfernandes.org header.s=google header.b=V3s3hHtb; 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: from out1.vger.email (out1.vger.email. [2620:137:e000::1:20]) by mx.google.com with ESMTP id b6-20020aa7d486000000b004acaa4dcac4si6757508edr.583.2023.02.12.17.56.25; Sun, 12 Feb 2023 17:56:48 -0800 (PST) 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; dkim=pass header.i=@joelfernandes.org header.s=google header.b=V3s3hHtb; 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 S229709AbjBMBzc (ORCPT + 99 others); Sun, 12 Feb 2023 20:55:32 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:58202 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S229477AbjBMBzb (ORCPT ); Sun, 12 Feb 2023 20:55:31 -0500 Received: from mail-qt1-x82c.google.com (mail-qt1-x82c.google.com [IPv6:2607:f8b0:4864:20::82c]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id F3087EF94 for ; Sun, 12 Feb 2023 17:55:29 -0800 (PST) Received: by mail-qt1-x82c.google.com with SMTP id c2so12410631qtw.5 for ; Sun, 12 Feb 2023 17:55:29 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=joelfernandes.org; s=google; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=xfWgFky8Oo0dLRgocQgSyLFVq1vdjV8IYOHij7ANhkk=; b=V3s3hHtb0C0w6Op4gMTtToGItfVkMz1GV1YRSAVo92QOgpk7wvHN2zcilMgF4sGWFM hOb/28Kf14srY+IPR4svTMsgyt0CIbmWlQQ9DNT9OUi6mu09O2/jFaKumSu8NxW7A/SX eeuA7pwAgJyeV5Ff514T4HO9DMuAjBeHHzZQg= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=xfWgFky8Oo0dLRgocQgSyLFVq1vdjV8IYOHij7ANhkk=; b=06T5f0GUasfLikekuNt+8H+1J7MdPt49DNujsJTAAqYdoP58sirr+Dfaudrx8xLBV7 PFVKHsK92NssDYhf2hnhgLq6LE70yWoJTRE7gAwgeTIxen2kHtjaDbCStejJrly6WmDF XOrAoqnWFQWbxWMz2pyeTJbpWcmQXzDFxFBBGeh02jBZo3fipVZ039HhnX3PnXVdWoNG OaVjHCL9ioD8oM7FvwnFtEM+jM1sIdDlMRBebPus6t9NhAdoz8MSofKh126mDKCVS8P2 FPFKWee1uKuIahJJjbtIoj0JgbFnpxbKn9WAWiqlK9ggcawB3yh0QYV9Zjjl1t/t+REr AX9g== X-Gm-Message-State: AO0yUKXZTyUBnb0fgVHH7WafLMjLnt6FQYhuyYwUjSd1om3x5gRsliWZ jCxFbFWwQbdw+uWZ8uBjuPGc5blLO1ioBxMC X-Received: by 2002:ac8:4e88:0:b0:3b8:8756:6de8 with SMTP id 8-20020ac84e88000000b003b887566de8mr38308317qtp.67.1676253328375; Sun, 12 Feb 2023 17:55:28 -0800 (PST) Received: from joelboxx.c.googlers.com.com (129.239.188.35.bc.googleusercontent.com. [35.188.239.129]) by smtp.gmail.com with ESMTPSA id p18-20020ac84092000000b003a7eb5baf3csm8354975qtl.69.2023.02.12.17.55.27 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 12 Feb 2023 17:55:27 -0800 (PST) From: "Joel Fernandes (Google)" To: linux-kernel@vger.kernel.org Cc: "Joel Fernandes (Google)" , Andrea Parri , Boqun Feng , Jade Alglave , Luc Maranget , "Paul E. McKenney" , Peter Zijlstra , Will Deacon , Jonas Oberhauser , Alan Stern , Akira Yokosawa , Andrea Parri , Daniel Lustig , David Howells , Jonas Oberhauser , linux-arch@vger.kernel.org, Nicholas Piggin , "Paul E. McKenney" , =?utf-8?q?Paul_Heidekr=C3=BCger?= , Will Deacon Subject: [PATCH] tools/memory-model: Add details about SRCU read-side critical sections Date: Mon, 13 Feb 2023 01:55:06 +0000 Message-Id: <20230213015506.778246-1-joel@joelfernandes.org> X-Mailer: git-send-email 2.39.1.581.gbfd45094c4-goog MIME-Version: 1.0 X-Spam-Status: No, score=-2.1 required=5.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,RCVD_IN_DNSWL_NONE, SPF_HELO_NONE,SPF_PASS autolearn=unavailable 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 X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1757679093841363865?= X-GMAIL-MSGID: =?utf-8?q?1757679093841363865?= Add details about SRCU read-side critical sections and how they are modeled. Cc: Andrea Parri Cc: Boqun Feng Cc: Jade Alglave Cc: Luc Maranget Cc: "Paul E. McKenney" Cc: Peter Zijlstra Cc: Will Deacon Cc: Jonas Oberhauser Suggested-by: Alan Stern Signed-off-by: Joel Fernandes (Google) Reviewed-by: Joel Fernandes (Google) --- .../Documentation/explanation.txt | 55 ++++++++++++++++++- 1 file changed, 52 insertions(+), 3 deletions(-) diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt index 8e7085238470..5f486d39fe10 100644 --- a/tools/memory-model/Documentation/explanation.txt +++ b/tools/memory-model/Documentation/explanation.txt @@ -28,9 +28,10 @@ Explanation of the Linux-Kernel Memory Consistency Model 20. THE HAPPENS-BEFORE RELATION: hb 21. THE PROPAGATES-BEFORE RELATION: pb 22. RCU RELATIONS: rcu-link, rcu-gp, rcu-rscsi, rcu-order, rcu-fence, and rb - 23. LOCKING - 24. PLAIN ACCESSES AND DATA RACES - 25. ODDS AND ENDS + 23. SRCU READ-SIDE CRITICAL SECTIONS + 24. LOCKING + 25. PLAIN ACCESSES AND DATA RACES + 26. ODDS AND ENDS @@ -1858,6 +1859,54 @@ links having the same SRCU domain with proper nesting); the details are relatively unimportant. +SRCU READ-SIDE CRITICAL SECTIONS +-------------------------------- +An SRCU read-side section is modeled with the srcu-rscs relation and +is different from rcu-rscs in the following respects: + +1. SRCU read-side sections are associated with a specific domain and +are independent of ones in different domains. Each domain has their +own independent grace-periods. + +2. Partitially overlapping SRCU read-side sections cannot fuse. It is +possible that among 2 partitally overlapping readers, the one that +starts earlier, starts before a GP started and the later reader starts +after the same GP started. These 2 readers are to be treated as +different srcu-rscs even for the same SRCU domain. + +3. The srcu_down_read() and srcu_up_read() primitives permit an SRCU +read-side lock to be acquired on one CPU and released another. While +this is also true about preemptible RCU, the LKMM does not model +preemption. So unlike SRCU, RCU readers are still modeled and +expected to be locked and unlocked on the same CPU in litmus tests. + +To make it easy to model SRCU readers in LKMM with the above 3 +properties, an SRCU lock operation is modeled as a load annotated with +'srcu-lock' and an SRCU unlock operation is modeled as a store +annotated with 'srcu-unlock'. This load and store takes the memory +address of an srcu_struct as an input, and the value returned is the +SRCU index (value). Thus LKMM creates a data-dependency between them +by virtue of the load and store memory accesses before performed on +the same srcu_struct: R[srcu-lock] ->data W[srcu-unlock]. +This data dependency becomes: R[srcu-lock] ->srcu-rscs W[srcu-unlock]. + +It is also possible that the data loaded from the R[srcu-lock] is +stored back into a memory location, and loaded on the same or even +another CPU, before doing an unlock. +This becomes: + R[srcu-lock] ->data W[once] ->rf R[once] ->data W[srcu-unlock] + +The model also treats this chaining of ->data and ->rf relations as: + R[srcu-lock] ->srcu-rscs W[srcu-unlock] by the model. + +Care must be taken that: + R[srcu-lock] ->data W[srcu-unlock] ->rf R[srcu-lock] is not +considered as a part of the above ->data and ->rf chain, which happens +because of one reader unlocking and another locking right after it. +The model excludes these ->rf relations when building the ->srcu-rscs +relation. + + LOCKING -------