lkml.org 
[lkml]   [2022]   [Dec]   [3]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: [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@rowland.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=...
>
> Have fun,
> Jonas
>
> (*= because this example is provided free of charge, there is no actual promise, to the extent permitted by applicable law)

And another reason why I tend to err on marking more accesses rather
than marking fewer. You never know when some "clever" compiler writer
might add a really strange optimization...

Thanx, Paul

\
 
 \ /
  Last update: 2022-12-03 20:06    [W:0.059 / U:0.356 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site