linux-kernel - Re: Question about PB rule of LKMM

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]

Message-ID: <Zenip+8BDM3p+MUh@andrea>
Date: Thu, 7 Mar 2024 16:52:07 +0100
From: Andrea Parri <parri.andrea@...il.com>
To: Alan Stern <stern@...land.harvard.edu>
Cc: Kenneth-Lee-2012@...mail.com, linux-kernel@...r.kernel.org,
	paulmck@...nel.org
Subject: Re: Question about PB rule of LKMM

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@...il.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@...mail.com>
Signed-off-by: Andrea Parri <parri.andrea@...il.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