From: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
To: Alan Stern <stern@rowland.harvard.edu>
Cc: paulmck@kernel.org, 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: Wed, 8 Jan 2025 20:22:07 +0100 [thread overview]
Message-ID: <06854f97-a671-426e-8c73-78214da8fbf5@huaweicloud.com> (raw)
In-Reply-To: <b43269fd-0d4f-4d43-af88-433583ba73f7@rowland.harvard.edu>
Am 1/8/2025 um 7:47 PM schrieb Alan Stern:
> On Wed, Jan 08, 2025 at 06:33:05PM +0100, Jonas Oberhauser wrote:
>>
>>
>> Am 1/7/2025 um 5:09 PM schrieb Alan Stern:
>>> 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.
>>
>> In the example above, this is not possible, because the address of a/b have
>> escaped the function and are not deallocated before synchronization happens.
>> Therefore the compiler must assume that a/b are accessed inside the compiler
>> barrier.
>
> I'm not quite sure what you mean by that, but if the compiler has access
> to the entire program and can do a global analysis then it can recognize
> cases where accesses that may seem to be live aren't really.
Even for trivial enough cases where the compiler has access to all the
source, compiler barriers should be opaque to the compiler.
Since it is opaque,
*a = 1;
compiler_barrier();
might as well be
*a = 1;
*d = *a; // *d is in device memory
and so in my opinion the compiler needs to ensure that the value of *a
right before the compiler barrier is 1.
Of course, only if the address of *a could be possibly legally known to
the opaque code in the compiler barrier.
>
> However, I admit this objection doesn't really apply to Linux kernel
> programming.
>
>>> (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?
>>
>> The main point (which I already mentioned in the previous e-mail) is if the
>> object is deallocated without synchronization (or never escapes the function
>> in the first place).
>>
>> And indeed, any such case renders the added rule unsound. It is in a sense
>> unrelated to OOTA; cases where the load/store can be elided are never OOTA.
>
> That is a matter of definition. In our paper, Paul and I described
> instances of OOTA in which all the accesses have been optimized away as
> "trivial".
Yes, by OOTA I mean a rwdep;rfe cycle.
In the absence of data races, such a cycle can't be optimized away
because it is created with volatile/compiler-barrier-protected accesses.
>> If an access interacts with an access of another thread (by reading from it
>> or being read from it), it must be live.
>
> This is the sort of approximation I'm a little uncomfortable with. It
> would be better to say that a store which is read from by a live load
> must be live. I don't see why a load which reads from a live store has
> to be live.
You are right, and I was careless.
All we need is that a store that is read externally by a live load is
live, and that a load that reads from an external store and has its
value semantically depended-on by a live store is live.
>> The formulation in the patch is just based on a complicated and close but
>> imperfect approximation of Live.
>
> Maybe you can reformulate the patch to make this more explicit.
It would look something like this:
Live = R & rng(po \ po ; [W] ; (po-loc \ w_barrier)) | W & dom(po \
((po-loc \ w_barrier) ; [W] ; po))
let to-w = (overwrite & int) | (addr | rmb ; [Live])? ; rwdep ; ([Live]
; wmb)?
> In any case, it seems that any approximation we can make to Live will be
> subject to various sorts of errors.
Probably (this is certainly true for trying to approximate dependencies,
for example), but what I know for certain is that the approximations of
Live inside cat get more ugly the more precise they become. In the above
definition of Live I have not included that the address must escape, nor
that it must not be freed.
A non-local definition that suffices for OOTA would be so:
Live = R & rng(rfe) & dom(rwdep ; rfe) | W & dom(rfe)
It seems the ideal solution is to let Live be defined by the tools,
which should keep up with or exceed the analysis done by state-of-art
compilers.
Best wishes,
jonas
next prev parent reply other threads:[~2025-01-08 19:22 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
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 [this message]
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=06854f97-a671-426e-8c73-78214da8fbf5@huaweicloud.com \
--to=jonas.oberhauser@huaweicloud.com \
--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=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=paulmck@kernel.org \
--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).