[PATCH] tools/memory-model: Amend the description of the pb relation

[Andrea Parri]

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.
 
 A good example illustrating how pb works is the SB pattern with strong
 fences:
-- 
2.34.1