Messages in this thread Patch in this message | | | From | "Paul E. McKenney" <> | Subject | [PATCH memory-model 4/8] tools/memory-model: Restrict to-r to read-read address dependency | Date | Mon, 20 Mar 2023 18:02:42 -0700 |
| |
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> --- 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
| |