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]
Date: Thu, 7 Mar 2024 13:30:22 -0500
From: Alan Stern <stern@...land.harvard.edu>
To: Andrea Parri <parri.andrea@...il.com>
Cc: Kenneth-Lee-2012@...mail.com, linux-kernel@...r.kernel.org,
  paulmck@...nel.org
Subject: Re: Question about PB rule of LKMM

On Thu, Mar 07, 2024 at 07:18:46PM +0100, Andrea Parri wrote:
> > 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?
> 
> I'd disagree with these premises: certain instructions can and do execute
> at the same time.

Can you give an example?

>  FWIW, in the formal model, it is not that difficult to
> provide examples of "(not F ->xb E) and (not E ->xb F)".

That's because the xb relation in the formal model does not fully 
capture our intuitive notion of "executes at the same time" in the 
informal operational model.

Also, it's important to distinguish between:

(1)	Two instructions that are forced (say by a dependency) or known 
	(say by an rfe link) to execute in a particular order; versus

(2)	Two instructions that may execute in either order but do execute
	in some particular order during a given run of the program.

The formal xb relation corresponds more to (1), whereas the informal 
notion corresponds more to (2).

> > 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.
> 
> The current text relies on an argument by contradiction.  A contradiction
> is reached by "forcing" (F ->xb E), hence all it can be concluded is that
> (not F ->xb E).  Again, AFAICS, this doesn't match the claim in the text.

That's why I suggested adding an extra sentence to the paragraph (which 
you did not quote in your reply).  That sentence gave a direct argument.

Alan

Powered by blists - more mailing lists

Powered by Openwall GNU/*/Linux Powered by OpenVZ