Message ID | 20230203201913.2555494-1-joel@joelfernandes.org |
---|---|
State | New |
Headers |
Return-Path: <linux-kernel-owner@vger.kernel.org> Delivered-To: ouuuleilei@gmail.com Received: by 2002:adf:eb09:0:0:0:0:0 with SMTP id s9csp1045456wrn; Fri, 3 Feb 2023 12:33:08 -0800 (PST) X-Google-Smtp-Source: AK7set8Bl7wROcVqg9Yl220y9LHozL9BB7yriYX2f9rU+zZq3cdL7g5+iiyRhk2jHevaSl86cNcP X-Received: by 2002:a50:8d86:0:b0:4a2:7cbc:7f49 with SMTP id r6-20020a508d86000000b004a27cbc7f49mr10299322edh.34.1675456387888; Fri, 03 Feb 2023 12:33:07 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1675456387; cv=none; d=google.com; s=arc-20160816; b=A60jUYqGcwjl6J+aEVy5JysltnDY8Pqo2IuQGpz63p45X/VW1xY6Kxh3nEGQmTvuZw FRZ/fu+Kbv2sTo0+i7voH/v/nVqr/dbtQj7RUuCL4LICMPDvCACa7zNX064n07N9MUWu U4Rza4Olcrh6oFa2us0KM8KcbedVTktEmhfIUfyCBpA2P/VGgYCQk8iXxh0594IZpAVW VuzMVJyCO0z6YP/tRVdJSzR2S5NZzZ4DDVXpfSPNEkR+jQSj9aSsHwGTaUq/JNvO/o9c riOBmqMjXz3F8x4bCU6d4bYEw099gW5ktjQJCkSw+jKRkLKALTNL61bcJoqmcBGY8ODR DWcA== 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=PlO+7yJUL6nZz6lWyKAteQU74Ju3H8abrNP72ihWCAM=; b=A6rOndbwrQ3K9zjoaoYXmU4ag9C2gXoRHi8cDIMgwF4mSGxZkCpIcxtS1dzwlzTBKc UroSWot+ShehC6NLOdAN6fjNxK+rJ5+NODB5jTubOlE9Z5Mcauh8mC7lfOqVrvoSJQMa pxhtadEIlq3sENpVNSXAfoK2HdMgrPqhcGHpdQQgEjmlN4AMJ+aOlApzXWsF5lAFYdgW 4MSdgIU0tap/fZb/W86vNKSa8KnXbchJoZmgNY889Xk9q2WrXS+9XRd6pzkvBRHkchNs PHRV+9YQLCFctoC+EPnM8S4l/IOdkmnEdCYlIUavVfxoIFg3edbpLZJjIXgdnVRF4BSK L79A== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@joelfernandes.org header.s=google header.b=Kmqgxr98; 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 cn25-20020a0564020cb900b00499c322d3b9si3426931edb.377.2023.02.03.12.32.43; Fri, 03 Feb 2023 12:33:07 -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=Kmqgxr98; 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 S233294AbjBCUTm (ORCPT <rfc822;il.mystafa@gmail.com> + 99 others); Fri, 3 Feb 2023 15:19:42 -0500 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:58466 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S233013AbjBCUTk (ORCPT <rfc822;linux-kernel@vger.kernel.org>); Fri, 3 Feb 2023 15:19:40 -0500 Received: from mail-qt1-x82e.google.com (mail-qt1-x82e.google.com [IPv6:2607:f8b0:4864:20::82e]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 11B239D58A for <linux-kernel@vger.kernel.org>; Fri, 3 Feb 2023 12:19:39 -0800 (PST) Received: by mail-qt1-x82e.google.com with SMTP id w3so6853766qts.7 for <linux-kernel@vger.kernel.org>; Fri, 03 Feb 2023 12:19:39 -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=PlO+7yJUL6nZz6lWyKAteQU74Ju3H8abrNP72ihWCAM=; b=Kmqgxr98A8rmlt1eG1Qvlry8R2htsdd8gpZ6xlaKDfwShmcldtpeNwAwBl+zru4UHO EjSIuyi/1gvQIqauWKxF1u9onlcTqDp2tfx7qNRK4/Y3nKJ9VCvqtvFoKH9iEkIm9TtH lMJWMucq5G4qzkWScRZDtPT9ns3GVif+j0OXs= 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=PlO+7yJUL6nZz6lWyKAteQU74Ju3H8abrNP72ihWCAM=; b=CJoWrAK4jHbZO6v+QxIEb5a+74f9kn3CuoNr9v1uOHmn1Xke8/MCSrfpDTp8GPFffs 6ZK7nORyqjYQQX25/DAV6CJmpaOMQ2VbvSgxE3wZhBfdi0APqJ2dVp2EeDrO2dSY8qy4 dvZ/3TDPkBCBXkdY4rgEV3GgfcwmlBrzGlc8Z8rNqRKxicteSuVZ/cU2MV5s1244kUje Tshuc5rwfrAkynHFyw3Vt2OuZbBhJN3OGifUgmifI2+u7m/EyknqDAEYytclbcufCGD8 pmJy8n81Skw833sNh6DlQDUinz7gAaJfAgrLnxiitgDjOXEPE5kgWXzRdxNU28xJN5gV 4q2g== X-Gm-Message-State: AO0yUKVp0HmNW4M8bmfEAgo1dLwmwWNbO0O0a/sySG6R2rK4N/OVP9Ia ivVKWueYUcov9FD8zVNd3ldUiIC2uhhmv4mI X-Received: by 2002:ac8:7e86:0:b0:3b9:a641:aa66 with SMTP id w6-20020ac87e86000000b003b9a641aa66mr21897622qtj.15.1675455577457; Fri, 03 Feb 2023 12:19:37 -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 g17-20020ae9e111000000b006ce580c2663sm2457424qkm.35.2023.02.03.12.19.36 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 03 Feb 2023 12:19:36 -0800 (PST) From: "Joel Fernandes (Google)" <joel@joelfernandes.org> To: linux-kernel@vger.kernel.org Cc: "Joel Fernandes (Google)" <joel@joelfernandes.org>, Akira Yokosawa <akiyks@gmail.com>, Alan Stern <stern@rowland.harvard.edu>, Andrea Parri <parri.andrea@gmail.com>, Boqun Feng <boqun.feng@gmail.com>, Daniel Lustig <dlustig@nvidia.com>, David Howells <dhowells@redhat.com>, Jade Alglave <j.alglave@ucl.ac.uk>, linux-arch@vger.kernel.org, Luc Maranget <luc.maranget@inria.fr>, Nicholas Piggin <npiggin@gmail.com>, "Paul E. McKenney" <paulmck@kernel.org>, Peter Zijlstra <peterz@infradead.org>, Will Deacon <will@kernel.org> Subject: [PATCH RFC] tools/memory-model: Restrict to-r to read-read address dependency Date: Fri, 3 Feb 2023 20:19:13 +0000 Message-Id: <20230203201913.2555494-1-joel@joelfernandes.org> X-Mailer: git-send-email 2.39.1.519.gcb327c4b5f-goog MIME-Version: 1.0 Content-Transfer-Encoding: 8bit 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: <linux-kernel.vger.kernel.org> X-Mailing-List: linux-kernel@vger.kernel.org X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1756843357085219699?= X-GMAIL-MSGID: =?utf-8?q?1756843357085219699?= |
Series |
[RFC] tools/memory-model: Restrict to-r to read-read address dependency
|
|
Commit Message
Joel Fernandes
Feb. 3, 2023, 8:19 p.m. UTC
During a code-reading exercise of linux-kernel.cat CAT file, I generated
a graph to show the to-r relations. While likely not problematic for the
model, I found it confusing that a read-write address dependency would
show as a to-r edge on the graph.
This patch therefore restricts the to-r links derived from addr to only
read-read address dependencies, so that read-write address dependencies don't
show as to-r in the graphs. This should also prevent future users of to-r from
deriving incorrect relations. Note that a read-write address dep, obviously,
still ends up in the ppo relation via the to-w relation.
I verified that a read-read address dependency still shows up as a to-r
link in the graph, as it did before.
For reference, the problematic graph was generated with the following
command:
herd7 -conf linux-kernel.cfg \
-doshow dep -doshow to-r -doshow to-w ./foo.litmus -show all -o OUT/
Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org>
---
tools/memory-model/linux-kernel.cat | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
Comments
On Fri, Feb 03, 2023 at 08:19:13PM +0000, Joel Fernandes (Google) wrote: > During a code-reading exercise of linux-kernel.cat CAT file, I generated > a graph to show the to-r relations. While likely not problematic for the > model, I found it confusing that a read-write address dependency would > show as a to-r edge on the graph. > > This patch therefore restricts the to-r links derived from addr to only > read-read address dependencies, so that read-write address dependencies don't > show as to-r in the graphs. This should also prevent future users of to-r from > deriving incorrect relations. Note that a read-write address dep, obviously, > still ends up in the ppo relation via the to-w relation. > > I verified that a read-read address dependency still shows up as a to-r > link in the graph, as it did before. > > For reference, the problematic graph was generated with the following > command: > herd7 -conf linux-kernel.cfg \ > -doshow dep -doshow to-r -doshow to-w ./foo.litmus -show all -o OUT/ > > Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org> > --- > tools/memory-model/linux-kernel.cat | 2 +- > 1 file changed, 1 insertion(+), 1 deletion(-) > > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat > index d70315fddef6..26e6f0968143 100644 > --- a/tools/memory-model/linux-kernel.cat > +++ b/tools/memory-model/linux-kernel.cat > @@ -69,7 +69,7 @@ let dep = addr | data > let rwdep = (dep | ctrl) ; [W] > let overwrite = co | fr > let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) > -let to-r = addr | (dep ; [Marked] ; rfi) > +let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi) > let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) > > (* Propagation: Ordering from release operations and strong fences. *) > -- > 2.39.1.519.gcb327c4b5f-goog Acked-by: Alan Stern <stern@rowland.harvard.edu>
On Fri, Feb 03, 2023 at 08:29:53PM -0500, Alan Stern wrote: > On Fri, Feb 03, 2023 at 08:19:13PM +0000, Joel Fernandes (Google) wrote: > > During a code-reading exercise of linux-kernel.cat CAT file, I generated > > a graph to show the to-r relations. While likely not problematic for the > > model, I found it confusing that a read-write address dependency would > > show as a to-r edge on the graph. > > > > This patch therefore restricts the to-r links derived from addr to only > > read-read address dependencies, so that read-write address dependencies don't > > show as to-r in the graphs. This should also prevent future users of to-r from > > deriving incorrect relations. Note that a read-write address dep, obviously, > > still ends up in the ppo relation via the to-w relation. > > > > I verified that a read-read address dependency still shows up as a to-r > > link in the graph, as it did before. > > > > For reference, the problematic graph was generated with the following > > command: > > herd7 -conf linux-kernel.cfg \ > > -doshow dep -doshow to-r -doshow to-w ./foo.litmus -show all -o OUT/ > > > > Signed-off-by: Joel Fernandes (Google) <joel@joelfernandes.org> > > --- > > tools/memory-model/linux-kernel.cat | 2 +- > > 1 file changed, 1 insertion(+), 1 deletion(-) > > > > diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat > > index d70315fddef6..26e6f0968143 100644 > > --- a/tools/memory-model/linux-kernel.cat > > +++ b/tools/memory-model/linux-kernel.cat > > @@ -69,7 +69,7 @@ let dep = addr | data > > let rwdep = (dep | ctrl) ; [W] > > let overwrite = co | fr > > let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) > > -let to-r = addr | (dep ; [Marked] ; rfi) > > +let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi) > > let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) > > > > (* Propagation: Ordering from release operations and strong fences. *) > > -- > > 2.39.1.519.gcb327c4b5f-goog > > Acked-by: Alan Stern <stern@rowland.harvard.edu> Thank you both, queued for v6.4. Thanx, Paul
diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index d70315fddef6..26e6f0968143 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -69,7 +69,7 @@ let dep = addr | data let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) -let to-r = addr | (dep ; [Marked] ; rfi) +let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi) let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) (* Propagation: Ordering from release operations and strong fences. *)