[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <Y/uOA3umovz06/SV@rowland.harvard.edu>
Date: Sun, 26 Feb 2023 11:51:15 -0500
From: Alan Stern <stern@...land.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc: Boqun Feng <boqun.feng@...il.com>,
"Paul E. McKenney" <paulmck@...nel.org>,
Jonas Oberhauser <jonas.oberhauser@...wei.com>,
parri.andrea@...il.com, will@...nel.org, peterz@...radead.org,
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
On Sun, Feb 26, 2023 at 12:17:31PM +0100, Jonas Oberhauser wrote:
>
>
> On 2/26/2023 4:30 AM, Alan Stern wrote:
> > On Sat, Feb 25, 2023 at 07:09:05PM -0800, Boqun Feng wrote:
> > > On Sat, Feb 25, 2023 at 09:29:51PM -0500, Alan Stern wrote:
> > > > On Sat, Feb 25, 2023 at 05:01:10PM -0800, Paul E. McKenney wrote:
> > > > > A few other oddities:
> > > > >
> > > > > litmus/auto/C-LB-Lww+R-OC.litmus
> > > > >
> > > > > Both versions flag a data race, which I am not seeing. It appears
> > > > > to me that P1's store to u0 cannot happen unless P0's store
> > > > > has completed. So what am I missing here?
> > > > 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.)
> > > >
> > > Because plain store can be optimzed as an "store only if not equal"?
> > > As the following sentenses in the explanations.txt:
> > >
> > > The need to distinguish between r- and w-bounding raises yet another
> > > issue. When the source code contains a plain store, the compiler is
> > > allowed to put plain loads of the same location into the object code.
> > > For example, given the source code:
> > >
> > > x = 1;
> > >
> > > the compiler is theoretically allowed to generate object code that
> > > looks like:
> > >
> > > if (x != 1)
> > > x = 1;
> > >
> > > thereby adding a load (and possibly replacing the store entirely).
> > > For this reason, whenever the LKMM requires a plain store to be
> > > w-pre-bounded or w-post-bounded by a marked access, it also requires
> > > the store to be r-pre-bounded or r-post-bounded, so as to handle cases
> > > where the compiler adds a load.
> > Good guess; maybe that was the reason. [...]
> > So perhaps the original reason is not valid now
> > that the memory model explicitly includes tests for stores being
> > r-pre/post-bounded.
> >
> > Alan
>
> I agree, I think you could relax that condition.
Here's a related question to think about. Suppose a compiler does make
this change, adding a load-and-test in front of a store. Can that load
cause a data race?
Normally I'd say no, because compilers aren't allowed to create data
races where one didn't already exist. But that restriction is part of
the C/C++ standard, and what we consider to be a data race differs from
what the standard considers.
So what's the answer? Is the compiler allowed to translate:
r1 = READ_ONCE(*x);
if (r1)
*y = 1;
into something resembling:
r1 = READ_ONCE(*x);
rtemp = *y;
if (r1) {
if (rtemp != 1)
*y = 1;
}
(Note that whether the load to rtemp occurs inside the "if (r1)"
conditional or not makes no difference; either way the CPU can execute
it before testing the condition. Even before reading the value of *x.)
_If_ we assume that these manufactured loads can never cause a data race
then it should be safe to remove the r-pre/post-bounded tests for plain
writes.
But what if rtemp reads from a plain write that was torn, and the
intermediate value it observes happens to be 1, even though neither the
initial nor the final value of *y was 1?
> Note there's also rw-xbstar (used with fr) which doesn't check for
> r-pre-bounded, but it should be ok. That's because only reads would be
> unordered, as a result the read (in the if (x != ..) x=..) should provide
> the correct value. The store would be issued as necessary, and the issued
> store would still be ordered correctly w.r.t the read.
That isn't the reason I left r-pre-bounded out from rw-xbstar. If the
write gets changed to a read there's no need for rw-xbstar to check
r-pre-bounded, because then rw-race would be comparing a read with
another read (instead of with a write) and so there would be no
possibility of a race in any case.
Alan
Powered by blists - more mailing lists