lkml.org 
[lkml]   [2023]   [Mar]   [20]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    Patch in this message
    /
    From
    Subject[PATCH memory-model 4/8] tools/memory-model: Restrict to-r to read-read address dependency
    Date
    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
    \
     
     \ /
      Last update: 2023-03-27 01:10    [W:3.307 / U:0.036 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site