Date Sat, 3 Dec 2022 10:20:28 -0500 From Alan Stern <> 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@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=...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`

Last update: 2022-12-03 16:21    [W:0.059 / U:0.240 seconds]