From: Alan Stern <stern@rowland.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>
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: Thu, 9 Jan 2025 22:12:57 -0500 [thread overview]
Message-ID: <8306ac43-fb00-4e58-bdeb-81ea9993c262@rowland.harvard.edu> (raw)
In-Reply-To: <582102b0-ee94-4160-95ec-4d44815cc39e@huaweicloud.com>
On Thu, Jan 09, 2025 at 09:09:00PM +0100, Jonas Oberhauser wrote:
> > > So for example, in
> > >
> > > int a = 1;
> > > barrier();
> > > a = 2;
> > > //...
> > >
> > > the compiler does not know how the code inside barrier() accesses memory,
> > > including volatile memory.
> >
> > I would say rather that the compiler does not know that the values
> > stored in memory are the same before and after the barrier().
> >
> > Even the
> > values of local variables whose addresses have not been exported.
>
> No, this is not true. I used to think so too until a short while ago.
>
> But if you look at the output of gcc -o3 you will see that it does happily
> remove `a` in this function.
Isn't that consistent with what I said?
> > > But it knows that it can not access `a`, because the address of `a` has
> > > never escaped before the barrier().
> >
> > I don't think this is right. barrier is (or can be) a macro, not a
> > function call with its own scope. As such, it has -- in principle --
> > the ability to export the address of a.
>
> See above. Please test it for yourself, but for your convenience here is the
> code
Oh, I believe that gcc does what you say. I'm just not sure your
explanation is entirely accurate.
> If you wanted to avoid this, you would need to expose the address of `a` to
> the asm block using one of its clobber arguments (but I'm not familiar with
> the syntax to produce a working example on the spot).
>
> >
> > Question: Can the compiler assume that no other threads access a between
> > the two stores, on the grounds that this would be a data race? I'd
> > guess that it can't make that assumption, but it would be nice to know
> > for sure.
>
> It can not make the assumption if &a has escaped. In that case, barrier()
> could be so:
>
> barrier(){
> store_release(OTHER_THREAD_PLEASE_MODIFY,&a);
>
> while (! load_acquire(OTHER_THREAD_IS_DONE));
> }
>
> with another thread doing
>
> while (! load_acquire(OTHER_THREAD_PLEASE_MODIFY)) yield();
> *OTHER_THREAD_PLEASE_MODIFY ++;
> store_release(OTHER_THREAD_IS_DONE, 1);
Bear in mind that there's a difference between what a compiler _can do_
and what gcc _currently does_.
> > I think you're giving the compiler too much credit. The one thing the
> > compiler is allowed to assume is that the code, as written, does not
> > contain a data race or other undefined behavior.
>
> Apologies, the way I used "assume" is misleading.
> I should have said that the compiler has to ensure that even if the code of
> foo() and barrier() were so, that the behavior of the code it generates is
> the same (w.r.t. observable side effects) as if the program were executed by
> the abstract machine. Or I should have said that it can *not* assume that
> the functions are *not* as defined above.
>
> Which means that TURN_THE_BREAKS_ON would need to be assigned 1.
> The only way the compiler can achieve that guarantee (while treating barrier
> as a black box) is to make sure that the value of `a` before barrier() is 1.
Who says the compiler has to treat barrier() as a black box? As far as
I know, gcc makes no such guarantee.
> > > That's why I said such a language model should just exclude global OOTA by
> > > fiat.
> >
> > One problem with doing this is that there is no widely agreed-upon
> > formal definition of OOTA. A cycle in (rwdep ; rfe) isn't the answer
> > because rwdep does not encapsulate the notion of semantic dependency.
>
> rwdep does not encapsulate any specific notion.
> It is herd7 which decides which dependency edges to add to the graphs it
> generates.
Sorry, that's what I meant: rwdep plus the decisions that herd7 makes
about which edges are dependencies.
> If herd7 would generate edges for semantic dependencies instead of for its
> version of syntactic dependencies, then rwdep is the answer.
That statement is meaningless (or at least, impossible to implement)
because there is no widely agreed-upon formal definition for semantic
dependency.
> Given that we can not define dep inside the cat model, one may as well
> define it as rwdep;rfe with the intended meaning of the dependencies being
> the semantic ones; then it is an inaccuracy of herd7 that it does not
> provide the proper dependencies.
Perhaps so. LKMM does include other features which the compiler can
defeat if the programmer isn't sufficiently careful. Still, I suspect
that changing the memory model solely with the goal of eliminating OOTA
may not be a good idea.
> Anyways LKMM should not care about syntactic dependencies, e.g.
>
>
> if (READ_ONCE(*a)) {
> WRITE_ONCE(*b,1);
> } else {
> WRITE_ONCE(*b,1);
> }
>
> has no semantic dependency and gcc does not guarantee the order between
> these two accesses, even though herd7 does give us a dependency edge.
Like I said.
> > > I have to read your paper again (I think I read it a few months ago) to
> > > understand if the trivial OOTA would make even that vague axiom unsound
> > > (my intuition says that if the OOTA is never observed by influencing the
> > > side-effect, then forbidding OOTA makes no difference to the set of
> > > "observable behaviors" of a C++ program even there is a trivial OOTA, and if
> > > the OOTA has visible side-effects, then it is acceptable for the compiler
> > > not to do the "optimization" that turns it into a trivial OOTA and choose
> > > some other optimization instead, so we can as well forbid the compiler from
> > > doing it).
> >
> > If an instance of OOTA is never observed, does it exist?
>
> :) :) :)
>
> > In the paper, I speculated that if a physical execution of a program
> > matches an abstract execution containing such a non-observed OOTA cycle,
> > then it also matches another abstract execution in which the cycle
> > doesn't exist. I don't know how to prove this conjecture, though.
>
> Yes, that also makes sense.
>
> Note that this speculation does not hold in the current LKMM though. In the
> Litmus test I shared in the opening e-mail, where the outcome 0:r1=1 /\
> 1:r1=1 is only possible with an OOTA (even though the values from the OOTA
> are never used anywhere).
If the fact that the outcome 0:r1=1 /\ 1:r1=1 has occurred is proof that
there was OOTA, then the OOTA cycle _is_ observed, albeit indirectly --
at least, in the sense that I intended. (The situation mentioned in the
paper is better described as an execution where the compiler has elided
all the accesses in the OOTA cycle.)
> With C++'s non-local model I wouldn't be totally surprised if there were
> similar examples in C++, but given that its ordering definition is a lot
> more straightforward than LKMM in that it doesn't have all these cases of
> different barriers like wmb and rmb and corner cases like Noreturn etc., my
> intuition says that there aren't any.
I'll have to give this some thought.
Alan
> But I am not going to think deeply about it for the time being.
>
> Best wishes
> jonas
next prev parent reply other threads:[~2025-01-10 3:13 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
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 [this message]
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=8306ac43-fb00-4e58-bdeb-81ea9993c262@rowland.harvard.edu \
--to=stern@rowland.harvard.edu \
--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=paulmck@kernel.org \
--cc=peterz@infradead.org \
--cc=quic_neeraju@quicinc.com \
--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).