* [PATCH RFC] tools/memory-model: Restrict to-r to read-read address dependency
@ 2023-02-03 20:19 Joel Fernandes (Google)
2023-02-04 1:29 ` Alan Stern
0 siblings, 1 reply; 3+ messages in thread
From: Joel Fernandes (Google) @ 2023-02-03 20:19 UTC (permalink / raw)
To: linux-kernel
Cc: Joel Fernandes (Google),
Akira Yokosawa, Alan Stern, Andrea Parri, Boqun Feng,
Daniel Lustig, David Howells, Jade Alglave, linux-arch,
Luc Maranget, Nicholas Piggin, Paul E. McKenney, Peter Zijlstra,
Will Deacon
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
^ permalink raw reply related [flat|nested] 3+ messages in thread
* Re: [PATCH RFC] tools/memory-model: Restrict to-r to read-read address dependency
2023-02-03 20:19 [PATCH RFC] tools/memory-model: Restrict to-r to read-read address dependency Joel Fernandes (Google)
@ 2023-02-04 1:29 ` Alan Stern
2023-02-04 1:51 ` Paul E. McKenney
0 siblings, 1 reply; 3+ messages in thread
From: Alan Stern @ 2023-02-04 1:29 UTC (permalink / raw)
To: Joel Fernandes (Google)
Cc: linux-kernel, Akira Yokosawa, Andrea Parri, Boqun Feng,
Daniel Lustig, David Howells, Jade Alglave, linux-arch,
Luc Maranget, Nicholas Piggin, Paul E. McKenney, Peter Zijlstra,
Will Deacon
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>
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: [PATCH RFC] tools/memory-model: Restrict to-r to read-read address dependency
2023-02-04 1:29 ` Alan Stern
@ 2023-02-04 1:51 ` Paul E. McKenney
0 siblings, 0 replies; 3+ messages in thread
From: Paul E. McKenney @ 2023-02-04 1:51 UTC (permalink / raw)
To: Alan Stern
Cc: Joel Fernandes (Google),
linux-kernel, Akira Yokosawa, Andrea Parri, Boqun Feng,
Daniel Lustig, David Howells, Jade Alglave, linux-arch,
Luc Maranget, Nicholas Piggin, Peter Zijlstra, Will Deacon
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
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2023-02-04 1:51 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-02-03 20:19 [PATCH RFC] tools/memory-model: Restrict to-r to read-read address dependency Joel Fernandes (Google)
2023-02-04 1:29 ` Alan Stern
2023-02-04 1:51 ` Paul E. McKenney
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).