From patchwork Fri Feb 3 20:19:13 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Joel Fernandes X-Patchwork-Id: 52636 Return-Path: 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 + 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 ); 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 ; Fri, 3 Feb 2023 12:19:39 -0800 (PST) Received: by mail-qt1-x82e.google.com with SMTP id w3so6853766qts.7 for ; 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)" To: linux-kernel@vger.kernel.org Cc: "Joel Fernandes (Google)" , Akira Yokosawa , Alan Stern , Andrea Parri , Boqun Feng , Daniel Lustig , David Howells , Jade Alglave , linux-arch@vger.kernel.org, Luc Maranget , Nicholas Piggin , "Paul E. McKenney" , Peter Zijlstra , Will Deacon 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 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?1756843357085219699?= X-GMAIL-MSGID: =?utf-8?q?1756843357085219699?= 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) Acked-by: Alan Stern --- 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. *)