From: Alan Stern <stern@rowland.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@huawei.com>
Cc: Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>,
"paulmck@kernel.org" <paulmck@kernel.org>,
"parri.andrea@gmail.com" <parri.andrea@gmail.com>,
"will@kernel.org" <will@kernel.org>,
"peterz@infradead.org" <peterz@infradead.org>,
"boqun.feng@gmail.com" <boqun.feng@gmail.com>,
"npiggin@gmail.com" <npiggin@gmail.com>,
"dhowells@redhat.com" <dhowells@redhat.com>,
"j.alglave@ucl.ac.uk" <j.alglave@ucl.ac.uk>,
"luc.maranget@inria.fr" <luc.maranget@inria.fr>,
"akiyks@gmail.com" <akiyks@gmail.com>,
"dlustig@nvidia.com" <dlustig@nvidia.com>,
"joel@joelfernandes.org" <joel@joelfernandes.org>,
"urezki@gmail.com" <urezki@gmail.com>,
"quic_neeraju@quicinc.com" <quic_neeraju@quicinc.com>,
"frederic@kernel.org" <frederic@kernel.org>,
"linux-kernel@vger.kernel.org" <linux-kernel@vger.kernel.org>
Subject: Re: [PATCH] tools: memory-model: Make plain accesses carry dependencies
Date: Fri, 2 Dec 2022 15:22:11 -0500 [thread overview]
Message-ID: <Y4pec7lfQHwmH4V/@rowland.harvard.edu> (raw)
In-Reply-To: <4905c14d2bc547a391d626416a20a2e9@huawei.com>
On Fri, Dec 02, 2022 at 05:22:57PM +0000, Jonas Oberhauser wrote:
> > but to me OOTA suggests something more: a value arising as if by
> > magic rather than as a result of a computation. In your version of
> > the litmus test there is WRITE_ONCE(*y, 1), so it's a little
> > understandable that you could end up with 1 as the final values of x
> > and y. But in my version, no values get computed anywhere, so the
> > final value of x and y might just as easily be 1 or 56789 -- it
> > literally arises "out of thin air".
>
> Maybe one can distinguish further between OOTA values (which are
> arbitrary, not-computed values) and more generally OOTA behaviors.
>
> How do you feel about examples like the one below:
There's something wrong with this example.
> void *y[2];
> void *x[2] = { (void*)&y[1], (void*)&y[0] };
>
> P0() {
> void **t = (void**)(x[0]);
Now t holds a pointer to y[1].
> *t = (void*)(t-1);
And now y[1] holds a pointer to y[0].
> }
> P1() {
> void **u = (void**)(x[1]);
Now u holds a pointer to y[0].
> *u = (void*)(u+1);
And now y[0] holds a pointer to y[1].
> }
>
> In this test case the locations x[0] and x[1] exist in the program and
> are accessed, but their addresses are never (explicitly) taken or
> stored anywhere.
Although they are dereferened.
> Nevertheless t=&x[1] and u=&x[0] could happen in an appropriately weak
> memory model (if the data races make you unhappy, you can add relaxed
> atomic/marked accesses); but not arbitrary values --- if t is not
> &x[1], it must be &y[1].
I don't see how. The comments I added above show what values t and u
must hold, regardless of how the program executes. The contents of x[]
never get changed, so there's no question about the values of t and u.
> To me, OOTA suggests simply that the computation can not happen
> "organically" in a step-by-step way, but can only pop into existence
> as a whole, "out of thin air" (unless one allows for very aggressive
> speculation and rollback).
All right, this is more a matter of personal taste and interpretation.
Is it the computation or the values that pops into existence? You can
think of these OOTA computations as arising in a (sort of) ordinary
step-by-step way, provided you allow loads to read from stores that
haven't happened yet (a very aggressive form of speculation indeed!).
> In this context I always picture the famous Baron Münchhausen, who
> pulled himself from mire by his own hair. (Which is an obviously false
> story because gentlemen at that time were wearing wigs, and a wig
> could not possibly carry his weight...)
There is a comparable American expression, "pull oneself up by one's
bootstraps", from which is derived the term "boot" for starting up a
computer. :-)
Alan
next prev parent reply other threads:[~2022-12-02 20:22 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2022-12-01 12:18 Jonas Oberhauser
2022-12-01 16:02 ` Alan Stern
2022-12-01 17:21 ` Jonas Oberhauser
2022-12-01 20:21 ` Alan Stern
2022-12-02 17:22 ` Jonas Oberhauser
2022-12-02 20:22 ` Alan Stern [this message]
2022-12-03 11:47 ` Jonas Oberhauser
2022-12-03 15:20 ` Alan Stern
2022-12-03 19:04 ` 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=Y4pec7lfQHwmH4V/@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=j.alglave@ucl.ac.uk \
--cc=joel@joelfernandes.org \
--cc=jonas.oberhauser@huawei.com \
--cc=jonas.oberhauser@huaweicloud.com \
--cc=linux-kernel@vger.kernel.org \
--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
all inboxes | Powered by JetHome®