Re: Question about PB rule of LKMM

[Alan Stern]

On Wed, Mar 06, 2024 at 06:36:09PM +0100, Andrea Parri wrote:
> > > In this sense, the propagation rule (like other "acyclicity"-constraints of
> > > the LKMM) expresses "temporal ordering", and any pb-link is (by definition)
> > > an "execute-before"-link.  The file explanation.txt can provide additional
> > > context/information, based on the (informal) operational model described in
> > > that file, about this matter.
> > 
> > So it is just a rule in the sence of mathematics? I think it would be better
> > if there were some explaination in the explaination file. It is
> > descripted in nature language, the reader might not notify it is just a
> > mathematics rule. And you cannot say an action executes before another
> > because they are in the pb link. It becomes a cycling in logic...

This _is_ described in the explanation.txt file.

The first paragraph in the section named "THE PROPAGATES-BEFORE 
RELATION: pb" mentions the mathematical rule:

---------------------------------------------------------------------
The propagates-before (pb) relation capitalizes on the special
features of strong fences.  It links two events E and F whenever some
store is coherence-later than E and propagates to every CPU and to RAM
before F executes.  The formal definition requires that E be linked to
F via a coe or fre link, an arbitrary number of cumul-fences, an
optional rfe link, a strong fence, and an arbitrary number of hb
links.  Let's see how this definition works out.
---------------------------------------------------------------------

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

Alan Stern

> I think you're on to something, explaining mathematical axioms or rules has
> never been an easy task AFAIU.  ;-)  (and that's why feedback is welcome)
> 
> The remark could be to continue to consider such rules "generalizations" of
> properties met by several hardware models or other specific contexts, rather
> than (mere) logically-derived facts.
> 
>   Andrea