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;
Date:   Wed, 22 Mar 2023 01:53:00 +0100
From:   Andrea Parri <parri.andrea@gmail.com>
To:     "Paul E. McKenney" <paulmck@kernel.org>
Cc:     linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org,
        kernel-team@meta.com, mingo@kernel.org, stern@rowland.harvard.edu,
        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 (Google)" <joel@joelfernandes.org>
Subject: Re: [PATCH memory-model 4/8] tools/memory-model: Restrict to-r to
 read-read address dependency
Message-ID: <ZBpRbPvdq6hQLyhX@andrea>
References: <778147e4-ccab-40cf-b6ef-31abe4e3f6b7@paulmck-laptop>
 <20230321010246.50960-4-paulmck@kernel.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <20230321010246.50960-4-paulmck@kernel.org>
Precedence: bulk

On Mon, Mar 20, 2023 at 06:02:42PM -0700, Paul E. McKenney wrote:
> From: "Joel Fernandes (Google)" <joel@joelfernandes.org>
> 
> 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>
> Acked-by: Alan Stern <stern@rowland.harvard.edu>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>

Acked-by: Andrea Parri <parri.andrea@gmail.com>

  Andrea


> ---
>  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 3a4d3b49e85c..cfc1b8fd46da 100644
> --- a/tools/memory-model/linux-kernel.cat
> +++ b/tools/memory-model/linux-kernel.cat
> @@ -81,7 +81,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.40.0.rc2
>