Re: Question about PB rule of LKMM

[Andrea Parri <parri.andrea@gmail.com>]

> > C test
> > 
> > {}
> > 
> > P0(int *x)
> > {
> > 	*x = 1;
> > }
> > 
> > P1(int *x)
> > {
> > 	*x = 2;
> > }
> 
> Ah, but you see, any time you run this program one of those statements
> will execute before the other.  Which will go first is indeterminate,
> but the chance of them executing at _exactly_ the same moment is zero.

TBH, I don't.  But I trust you know your memory controller.  ;-)


> > This appears to be the key observation.  For if, in the operational model,
> > (not F ->xb E) implies (E ->xb F) then I'll apologize for the noise.  :-)
> 
> Okay, so it looks like we're in violent agreement.  :-)

Fiuu!!  ;-)


> The way you put it also relies on argument by contradiction.  This
> just wasn't visible, because you omitted a lot of intermediate steps in
> the reasoning.
> 
> If you want to see this in detail, try explaining why it is that "W is
> coherence-later than E" implies "E must execute before W propagates to
> E's CPU" in the operational model.

But that's all over in explanation.txt??  FWIW, a quick search returned
(wrt fre):

  R ->fre W means that W overwrites the value which R reads, but it
  doesn't mean that W has to execute after R.  All that's necessary
  is for the memory subsystem not to propagate W to R's CPU until
  after R has executed

I really don't see how the operational model could explain even a simple
MP without "knowing" this fact.

IAC, I'm pretty sure my "intermediate steps" wouldn't be using the same
forcing condition.  :-)

  Andrea