Re: Question about PB rule of LKMM

[Alan Stern]

On Thu, Mar 07, 2024 at 07:18:46PM +0100, Andrea Parri wrote:
> > So I guess you're talking about the second, intuitive meaning.  That's 
> > very simple to explain.  Since every instruction executes at _some_ 
> > time, and since we can safely assume that no two instructions execute at 
> > exactly the _same_ time, if F doesn't execute before E then E must 
> > execute before F.  Or using your terms, (not F ->xb E) implies (E ->xb 
> > F).  Would that answer the original question satisfactorily?
> 
> I'd disagree with these premises: certain instructions can and do execute
> at the same time.

Can you give an example?

>  FWIW, in the formal model, it is not that difficult to
> provide examples of "(not F ->xb E) and (not E ->xb F)".

That's because the xb relation in the formal model does not fully 
capture our intuitive notion of "executes at the same time" in the 
informal operational model.

Also, it's important to distinguish between:

(1)	Two instructions that are forced (say by a dependency) or known 
	(say by an rfe link) to execute in a particular order; versus

(2)	Two instructions that may execute in either order but do execute
	in some particular order during a given run of the program.

The formal xb relation corresponds more to (1), whereas the informal 
notion corresponds more to (2).

> > The new text says the same thing as the original, just in a more 
> > condensed way.  It skips the detailed explanation of why E must execute 
> > before W propagates to E's CPU, merely saying that it is because "W is 
> > coherence-later than E".  I'm not sure this is an improvement; the 
> > reader might want to know exactly how this reasoning goes.
> 
> The current text relies on an argument by contradiction.  A contradiction
> is reached by "forcing" (F ->xb E), hence all it can be concluded is that
> (not F ->xb E).  Again, AFAICS, this doesn't match the claim in the text.

That's why I suggested adding an extra sentence to the paragraph (which 
you did not quote in your reply).  That sentence gave a direct argument.

Alan