Re: Question about PB rule of LKMM

[Andrea Parri]

On Wed, Mar 06, 2024 at 08:24:42PM +0100, Andrea Parri wrote:
> > Later on, the file includes this paragraph, which answers the question 
> > you were asking:
> > 
> > ---------------------------------------------------------------------
> > The existence of a pb link from E to F implies that E must execute
> > before F.  To see why, suppose that F executed first.  Then W would
> > have propagated to E's CPU before E executed.  If E was a store, the
> > memory subsystem would then be forced to make E come after W in the
> > coherence order, contradicting the fact that E ->coe W.  If E was a
> > load, the memory subsystem would then be forced to satisfy E's read
> > request with the value stored by W or an even later store,
> > contradicting the fact that E ->fre W.
> > ---------------------------------------------------------------------
> 
> TBF, that just explains (not F ->xb E), or I guess that was the origin
> of the question.

So perhaps as in the diff below.  (Alan, feel free to manipulate to better
align with the current contents and style of explanation.txt.)

  Andrea