Re: Question about PB rule of LKMM

[Alan Stern]

On Thu, Mar 07, 2024 at 10:06:08PM +0100, Andrea Parri wrote:
> > > 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.  ;-)

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.

> > 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

(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.

Alan