Re: Question about PB rule of LKMM

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

> I can't tell which aspect of this bothers you more: the fact that the 
> text uses an argument by contradiction, or the fact that it ignores the 
> possibility of two instructions executing at the same time.
> 
> If it's the latter, consider this: Although the text doesn't say so, 
> the reasoning it gives also covers the case where F executes at the same 
> time as E.  You can still deduce that W must have propagated to E's 
> CPU before E executed, because W must propagate to every CPU before F 
> executes.

Agreed.  I suspect this exchange would have been much shorter if we did
say/write so, but I'll leave it up to you.


> (In fact, that sentence isn't entirely accurate.  It should say "... not 
> to propagate W (or a co-later store)...".)
> 
> Let's consider coe instead of fre.  The description of how the 
> operational model manages the coherence order of stores is found in 
> section 13 (AN OPERATIONAL MODEL):
> 
> 	When CPU C executes a store instruction, it tells the memory 
> 	subsystem to store a certain value at a certain location.  The 
> 	memory subsystem propagates the store to all the other CPUs as 
> 	well as to RAM.  (As a special case, we say that the store 
> 	propagates to its own CPU at the time it is executed.)  The 
> 	memory subsystem also determines where the store falls in the 
> 	location's coherence order.  In particular, it must arrange for 
> 	the store to be co-later than (i.e., to overwrite) any other 
> 	store to the same location which has already propagated to CPU 
> 	C.
> 
> So now if E is a store and is co-before W, how do we know that W didn't 
> propagate to E's CPU before E executed?  It's clear from the last 
> sentence of the text above: If W had propagated to E's CPU before E 
> executed then the memory subsystem would have arranged for E to be 
> co-later than W.  That's an argument by contradiction, and there's no 
> way to avoid it here.

I can live with that.

  Andrea