Re: Question about PB rule of LKMM

[Alan Stern]

On Thu, Mar 07, 2024 at 04:52:07PM +0100, Andrea Parri wrote:
> 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.

Are we talking about the formal xb relation (as mentioned in a comment 
in linux-kernel.cat), or the informal notion of "executing before" as 
used in the operational model?  In the first case, it's true by 
definition that pb implies xb, since xb would be defined by:

	let xb = hb | pb | rb

if it were in the memory model.

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?

> 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
> 
> From c13fd76cd62638cbe197431a16aeea001f80f6ec Mon Sep 17 00:00:00 2001
> From: Andrea Parri <parri.andrea@xxxxxxxxx>
> Date: Thu, 7 Mar 2024 16:31:57 +0100
> Subject: [PATCH] tools/memory-model: Amend the description of the pb relation
> 
> To convey why E ->pb F implies E ->xb F in the operational model of
> explanation.txt.
> 
> Reported-by: Kenneth Lee <Kenneth-Lee-2012@xxxxxxxxxxx>
> Signed-off-by: Andrea Parri <parri.andrea@xxxxxxxxx>
> ---
>  tools/memory-model/Documentation/explanation.txt | 12 +++++-------
>  1 file changed, 5 insertions(+), 7 deletions(-)
> 
> diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt
> index 6dc8b3642458e..68af5effadbbb 100644
> --- a/tools/memory-model/Documentation/explanation.txt
> +++ b/tools/memory-model/Documentation/explanation.txt
> @@ -1461,13 +1461,11 @@ The case where E is a load is exactly the same, except that the first
>  link in the sequence is fre instead of coe.
>  
>  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.
> +before F.  To see why, let W be a store coherence-later than E and
> +propagating to every CPU and to RAM before F executes.  Then E must
> +execute before W propagates to E's CPU (since W is coherence-later
> +than E).  In turn, W propagates to E's CPU (and every CPU) before F
> +executes.

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.

Would it suit you to instead add an extra sentence to the end of the 
paragraph, something like this?

	These contradictions show that E must execute before W 
	propagates to E's CPU, hence before W propagates to every
	CPU, and hence before F executes.

Alan Stern