[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <Y4tpPCWyt3zfQljk@rowland.harvard.edu>
Date: Sat, 3 Dec 2022 10:20:28 -0500
From: Alan Stern <stern@...land.harvard.edu>
To: Jonas Oberhauser <jonas.oberhauser@...wei.com>
Cc: Jonas Oberhauser <jonas.oberhauser@...weicloud.com>,
"paulmck@...nel.org" <paulmck@...nel.org>,
"parri.andrea@...il.com" <parri.andrea@...il.com>,
"will@...nel.org" <will@...nel.org>,
"peterz@...radead.org" <peterz@...radead.org>,
"boqun.feng@...il.com" <boqun.feng@...il.com>,
"npiggin@...il.com" <npiggin@...il.com>,
"dhowells@...hat.com" <dhowells@...hat.com>,
"j.alglave@....ac.uk" <j.alglave@....ac.uk>,
"luc.maranget@...ia.fr" <luc.maranget@...ia.fr>,
"akiyks@...il.com" <akiyks@...il.com>,
"dlustig@...dia.com" <dlustig@...dia.com>,
"joel@...lfernandes.org" <joel@...lfernandes.org>,
"urezki@...il.com" <urezki@...il.com>,
"quic_neeraju@...cinc.com" <quic_neeraju@...cinc.com>,
"frederic@...nel.org" <frederic@...nel.org>,
"linux-kernel@...r.kernel.org" <linux-kernel@...r.kernel.org>
Subject: Re: [PATCH] tools: memory-model: Make plain accesses carry
dependencies
On Sat, Dec 03, 2022 at 11:47:06AM +0000, Jonas Oberhauser wrote:
>
>
> -----Original Message-----
> From: Alan Stern [mailto:stern@...land.harvard.edu]
> Sent: Friday, December 2, 2022 9:22 PM
>
> > > 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].
>
> Unfortunately, this kind of inductive reasoning (arguing about what happens based on what happened "before") is not possible with memory models that allow OOTA; as you put it, one must allow for loads reading from stores that haven't happened yet.
> One such store (I promise!(*)) is a store to x[0] which writes &x[1]. Let's consider the alternative universe where we read from this future store, so now t holds a pointer to x[1].
>
> > > *t = (void*)(t-1);
>
> > And now y[1] holds a pointer to y[0].
>
> In our alternative universe, x[1] now holds a pointer to x[0].
>
>
> > > }
> > > P1() {
> > > void **u = (void**)(x[1]);
>
> > Now u holds a pointer to y[0].
>
> In our alternative universe, u holds the pointer to x[0] stored by P0().
>
> > > *u = (void*)(u+1);
>
> > And now y[0] holds a pointer to y[1].
>
> In our alternative universe, now x[0] holds a pointer to x[1]. Behold, the store I promised would happen!
>
> > > }
>
> > The contents of x[] never get changed, so there's no question about the values of t and u.
>
> They might get changed, by the stores *t=... and *u=...
Okay, now I understand. Yes, this counts as an example of values
appearing out of thin air, even though the values are constrained. The
same sort of thing can happen in a less exotic form, such as:
P0 P1
------ -----------
x = y; y = x & ~1;
Then in an OOTA execution, x and y can end up holding any _even_ value.
Yes, constraining a value to be even is less drastic than constraining
it to be &x[0] as in your example, but it's still a constraint. One
can easily extend this example in various directions.
Alan
Powered by blists - more mailing lists