From: "Paul E. McKenney" <paulmck@kernel.org>
To: Alan Stern <stern@rowland.harvard.edu>
Cc: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>,
parri.andrea@gmail.com, will@kernel.org, peterz@infradead.org,
boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com,
j.alglave@ucl.ac.uk, luc.maranget@inria.fr, akiyks@gmail.com,
dlustig@nvidia.com, joel@joelfernandes.org, urezki@gmail.com,
quic_neeraju@quicinc.com, frederic@kernel.org,
linux-kernel@vger.kernel.org, lkmm@lists.linux.dev,
hernan.poncedeleon@huaweicloud.com
Subject: Re: [RFC] tools/memory-model: Rule out OOTA
Date: Tue, 7 Jan 2025 10:47:43 -0800 [thread overview]
Message-ID: <68f98254-daf9-4197-a7cb-ef9fca0ef158@paulmck-laptop> (raw)
In-Reply-To: <a3bf910f-509a-4ad3-a1cc-4b14ef9b3259@rowland.harvard.edu>
On Tue, Jan 07, 2025 at 11:09:55AM -0500, Alan Stern wrote:
> On Mon, Jan 06, 2025 at 10:40:03PM +0100, Jonas Oberhauser wrote:
> > The current LKMM allows out-of-thin-air (OOTA), as evidenced in the following
> > example shared on this list a few years ago:
> >
> > P0(int *a, int *b, int *x, int *y) {
> > int r1;
> >
> > r1 = READ_ONCE(*x);
> > smp_rmb();
> > if (r1 == 1) {
> > *a = *b;
> > }
> > smp_wmb();
> > WRITE_ONCE(*y, 1);
> > }
> >
> > P1(int *a, int *b, int *x, int *y) {
> > int r1;
> >
> > r1 = READ_ONCE(*y);
> > smp_rmb();
> > if (r1 == 1) {
> > *b = *a;
> > }
> > smp_wmb();
> > WRITE_ONCE(*x, 1);
> > }
> >
> > exists b=42
> >
> > The root cause is an interplay between plain accesses and rw-fences, i.e.,
> > smp_rmb() and smp_wmb(): while smp_rmb() and smp_wmb() provide sufficient
> > ordering for plain accesses to rule out data races, they do not in the current
> > formalization generally actually order the plain accesses, allowing, e.g., the
> > load and stores to *b to proceed in any order even if P1 reads from P0; and in
> > particular, the marked accesses around those plain accesses are also not
> > ordered, which causes this OOTA.
>
> That's right. The memory model deliberately tries to avoid placing
> restrictions on plain accesses, whenever it can.
>
> In the example above, for instance, I think it's more interesting to ask
>
> exists 0:r1=1 /\ 1:r1=1
>
> than to concentrate on a and b.
>
> OOTA is a very difficult subject. It can be approached only by making
> the memory model take all sorts of compiler optimizations into account,
> and doing this for all possible optimizations is not feasible.
Mark Batty and his students believe otherwise, but I am content to let
them make that argument. As in I agree with you rather than them. At
least unless and until they make their argument. ;-)
> (For example, in a presentation to the C++ working group last year, Paul
> and I didn't try to show how to extend the C++ memory model to exclude
> OOTA [other than by fiat, as it does now]. Instead we argued that with
> the existing memory model, no reasonable compiler would ever produce an
> executable that could exhibit OOTA and so the memory model didn't need
> to be changed.)
Furthermore, the LKMM design choice was that if a given litmus test was
flagged as having a data race, anything might happen, including OOTA.
In case there is interest, that presentation may be found here:
https://drive.google.com/file/d/1ZeJlUJfH90S2uf2wRvNXQvM4jNVSlZI8/view?usp=sharing
The most recent version of the working paper may be found here:
https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2024/p3064r2.pdf
Thanx, Paul
> > In this patch, we choose the rather conservative approach of forcing only the
> > order of these marked accesses, specifically, when a marked read r is
> > separated from a plain read r' by an smp_rmb() (or r' has an address
> > dependency on r or is r'), on which a write w' depends, and w' is either plain
> > and seperated by a subsequent write w by an smp_wmb() (or w' is w), then r
> > precedes w in ppo.
>
> Is this really valid? In the example above, if there were no other
> references to a or b in the rest of the program, the compiler could
> eliminate them entirely. (Whether the result could count as OOTA is
> open to question, but that's not the point.) Is it not possible that a
> compiler might find other ways to defeat your intentions?
>
> In any case, my feeling is that memory models for higher languages
> (i.e., anything above the assembler level) should not try very hard to
> address the question of OOTA. And for LKMM, OOTA involving _plain_
> accesses is doubly out of bounds.
>
> Your proposed change seems to add a significant complication to the
> memory model for a not-very-clear benefit.
>
> Alan
next prev parent reply other threads:[~2025-01-07 18:47 UTC|newest]
Thread overview: 59+ messages / expand[flat|nested] mbox.gz Atom feed top
2025-01-06 21:40 [RFC] tools/memory-model: Rule out OOTA Jonas Oberhauser
2025-01-07 10:06 ` Peter Zijlstra
2025-01-07 11:02 ` Jonas Oberhauser
2025-01-07 15:46 ` Jonas Oberhauser
2025-01-07 16:09 ` Alan Stern
2025-01-07 18:47 ` Paul E. McKenney [this message]
2025-01-08 17:39 ` Jonas Oberhauser
2025-01-08 18:09 ` Paul E. McKenney
2025-01-08 19:17 ` Jonas Oberhauser
2025-01-09 17:54 ` Paul E. McKenney
2025-01-09 18:35 ` Jonas Oberhauser
2025-01-10 14:54 ` Paul E. McKenney
2025-01-10 16:21 ` Jonas Oberhauser
2025-01-13 22:04 ` Paul E. McKenney
2025-01-16 18:40 ` Paul E. McKenney
2025-01-16 19:13 ` Jonas Oberhauser
2025-01-16 19:31 ` Paul E. McKenney
2025-01-16 20:21 ` Jonas Oberhauser
2025-01-16 19:28 ` Jonas Oberhauser
2025-01-16 19:39 ` Paul E. McKenney
2025-01-17 12:08 ` Jonas Oberhauser
2025-01-16 19:08 ` Jonas Oberhauser
2025-01-16 23:02 ` Alan Stern
2025-01-17 8:34 ` Hernan Ponce de Leon
2025-01-17 11:29 ` Jonas Oberhauser
2025-01-17 20:01 ` Alan Stern
2025-01-21 10:36 ` Jonas Oberhauser
2025-01-21 16:39 ` Alan Stern
2025-01-22 3:46 ` Jonas Oberhauser
2025-01-22 19:11 ` Alan Stern
2025-01-17 15:52 ` Alan Stern
2025-01-17 16:45 ` Jonas Oberhauser
2025-01-17 19:02 ` Alan Stern
2025-01-09 20:37 ` Peter Zijlstra
2025-01-09 21:13 ` Paul E. McKenney
2025-01-08 17:33 ` Jonas Oberhauser
2025-01-08 18:47 ` Alan Stern
2025-01-08 19:22 ` Jonas Oberhauser
2025-01-09 16:17 ` Alan Stern
2025-01-09 16:44 ` Jonas Oberhauser
2025-01-09 19:27 ` Alan Stern
2025-01-09 20:09 ` Jonas Oberhauser
2025-01-10 3:12 ` Alan Stern
2025-01-10 12:21 ` Jonas Oberhauser
2025-01-10 21:51 ` Alan Stern
2025-01-11 12:46 ` Jonas Oberhauser
2025-01-11 21:19 ` Alan Stern
2025-01-12 15:55 ` Jonas Oberhauser
2025-01-13 19:43 ` Alan Stern
2025-07-23 0:43 ` Paul E. McKenney
2025-07-23 7:26 ` Hernan Ponce de Leon
2025-07-23 16:39 ` Paul E. McKenney
2025-07-24 14:14 ` Paul E. McKenney
2025-07-25 5:23 ` Hernan Ponce de Leon
2025-07-29 20:34 ` Paul E. McKenney
2025-07-23 17:13 ` Alan Stern
2025-07-23 17:27 ` Paul E. McKenney
2025-07-23 19:25 ` Alan Stern
2025-07-23 19:57 ` Paul E. McKenney
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=68f98254-daf9-4197-a7cb-ef9fca0ef158@paulmck-laptop \
--to=paulmck@kernel.org \
--cc=akiyks@gmail.com \
--cc=boqun.feng@gmail.com \
--cc=dhowells@redhat.com \
--cc=dlustig@nvidia.com \
--cc=frederic@kernel.org \
--cc=hernan.poncedeleon@huaweicloud.com \
--cc=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=jonas.oberhauser@huaweicloud.com \
--cc=linux-kernel@vger.kernel.org \
--cc=lkmm@lists.linux.dev \
--cc=luc.maranget@inria.fr \
--cc=npiggin@gmail.com \
--cc=parri.andrea@gmail.com \
--cc=peterz@infradead.org \
--cc=quic_neeraju@quicinc.com \
--cc=stern@rowland.harvard.edu \
--cc=urezki@gmail.com \
--cc=will@kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).