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: <ZeuDMKtVotRefSm3@andrea>
Date: Fri, 8 Mar 2024 22:29:20 +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

> I can't tell which aspect of this bothers you more: the fact that the 
> text uses an argument by contradiction, or the fact that it ignores the 
> possibility of two instructions executing at the same time.
> 
> If it's the latter, consider this: Although the text doesn't say so, 
> the reasoning it gives also covers the case where F executes at the same 
> time as E.  You can still deduce that W must have propagated to E's 
> CPU before E executed, because W must propagate to every CPU before F 
> executes.

Agreed.  I suspect this exchange would have been much shorter if we did
say/write so, but I'll leave it up to you.


> (In fact, that sentence isn't entirely accurate.  It should say "... not 
> to propagate W (or a co-later store)...".)
> 
> Let's consider coe instead of fre.  The description of how the 
> operational model manages the coherence order of stores is found in 
> section 13 (AN OPERATIONAL MODEL):
> 
> 	When CPU C executes a store instruction, it tells the memory 
> 	subsystem to store a certain value at a certain location.  The 
> 	memory subsystem propagates the store to all the other CPUs as 
> 	well as to RAM.  (As a special case, we say that the store 
> 	propagates to its own CPU at the time it is executed.)  The 
> 	memory subsystem also determines where the store falls in the 
> 	location's coherence order.  In particular, it must arrange for 
> 	the store to be co-later than (i.e., to overwrite) any other 
> 	store to the same location which has already propagated to CPU 
> 	C.
> 
> So now if E is a store and is co-before W, how do we know that W didn't 
> propagate to E's CPU before E executed?  It's clear from the last 
> sentence of the text above: If W had propagated to E's CPU before E 
> executed then the memory subsystem would have arranged for E to be 
> co-later than W.  That's an argument by contradiction, and there's no 
> way to avoid it here.

I can live with that.

  Andrea