Re: Question about PB rule of LKMM

[Andrea Parri <parri.andrea@gmail.com>]

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

From c13fd76cd62638cbe197431a16aeea001f80f6ec Mon Sep 17 00:00:00 2001
From: Andrea Parri <parri.andrea@gmail.com>
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@foxmail.com>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
---
 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.
 
 A good example illustrating how pb works is the SB pattern with strong
 fences:
-- 
2.34.1