[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <Y/0HEESX2wDWtPS1@andrea>
Date: Mon, 27 Feb 2023 20:40:00 +0100
From: Andrea Parri <parri.andrea@...il.com>
To: Alan Stern <stern@...land.harvard.edu>
Cc: "Paul E. McKenney" <paulmck@...nel.org>,
Jonas Oberhauser <jonas.oberhauser@...wei.com>,
will@...nel.org, peterz@...radead.org, boqun.feng@...il.com,
npiggin@...il.com, dhowells@...hat.com, j.alglave@....ac.uk,
luc.maranget@...ia.fr, akiyks@...il.com, dlustig@...dia.com,
joel@...lfernandes.org, urezki@...il.com, quic_neeraju@...cinc.com,
frederic@...nel.org, linux-kernel@...r.kernel.org
Subject: Re: [PATCH v3] tools/memory-model: Make ppo a subrelation of po
> The LKMM doesn't believe that a control or data dependency orders a
> plain write after a marked read. Hence in this test it thinks that P1's
> store to u0 can happen before the load of x1. I don't remember why we
> did it this way -- probably we just wanted to minimize the restrictions
> on when plain accesses can execute. (I do remember the reason for
> making address dependencies induce order; it was so RCU would work.)
>
> The patch below will change what the LKMM believes. It eliminates the
> positive outcome of the litmus test and the data race. Should it be
> adopted into the memory model?
(Unpopular opinion I know,) it should drop dependencies ordering, not
add/promote it.
Andrea
Powered by blists - more mailing lists