[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <b0bac412-cfc4-4334-8d8e-2fb080fe6e3e@rowland.harvard.edu>
Date: Fri, 17 Jan 2025 10:52:18 -0500
From: Alan Stern <stern@...land.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>
Cc: paulmck@...nel.org, parri.andrea@...il.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, lkmm@...ts.linux.dev,
hernan.poncedeleon@...weicloud.com
Subject: Re: [RFC] tools/memory-model: Rule out OOTA
On Thu, Jan 16, 2025 at 06:02:18PM -0500, Alan Stern wrote:
> On Thu, Jan 16, 2025 at 08:08:22PM +0100, Jonas Oberhauser wrote:
> > I would say that the approach with volatile is overzealous because it tries
> > to create a "local" order solution to the problem that only requires a
> > "global" ordering solution. Since not every semantic dependency needs to
> > provide order in C++ -- only the cycle of dependencies -- it is totally ok
> > to add too many semantic dependency edges to a program, even those that are
> > not going to be exactly maintained by every compiler, as long as we can
> > ensure that globally, no dependency cycle occurs.
>
> But then how would you characterize semantic dependencies, if you want
> to allow the definition to include some dependencies that aren't
> semantic but not so many that you ever create a cycle? This sounds like
> an even worse problem than we started with!
An interesting side comment on this issue...
This is a slight variation of the example on page 19 (section 4.3) of
the paper. (Pretend this is actually C++ code, the shared variables are
all atomic, and their accesses are all relaxed.)
bool x, y, z;
void P0(bool *x, bool *y, bool *z) {
bool r1, r2;
r1 = *x;
r2 = *y;
*z = (r1 != r2);
}
The paper points out that although there is an apparent semantic
dependency from the load of x to the store to z, if the compiler is
allowed not to handle atomics as quasi volatile then the dependency
can be broken. Nevertheless, I am not able to think of a program that
could exhibit OOTA as a result of breaking the semantic dependency. The
best I can come up with is this:
[P0 as above]
void P1(bool *x, bool *y, bool *z) {
bool r3;
r3 = z;
x = r3;
}
void P2(bool *x, bool *y, bool *z) {
y = true;
}
exists (x=true /\ z=true)
If P2 were not present, this result could not occur in any physical
execution, even if the dependency in P0 is broken. With P2 this result
isn't OOTA, even in executions where P0 ends up storing z before loading
x, because P2 could have executed first, then P0, then P1.
So perhaps this is an example of what you were talking about -- a
dependency which may or may not be semantic, but either way cannot lead
to OOTA.
Alan
Powered by blists - more mailing lists