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]

Date: Thu, 7 Mar 2024 22:06:08 +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

> > C test
> > 
> > {}
> > 
> > P0(int *x)
> > {
> > 	*x = 1;
> > }
> > 
> > P1(int *x)
> > {
> > 	*x = 2;
> > }
> 
> Ah, but you see, any time you run this program one of those statements
> will execute before the other.  Which will go first is indeterminate,
> but the chance of them executing at _exactly_ the same moment is zero.

TBH, I don't.  But I trust you know your memory controller.  ;-)

> > This appears to be the key observation.  For if, in the operational model,
> > (not F ->xb E) implies (E ->xb F) then I'll apologize for the noise.  :-)
> 
> Okay, so it looks like we're in violent agreement.  :-)

Fiuu!!  ;-)

> The way you put it also relies on argument by contradiction.  This
> just wasn't visible, because you omitted a lot of intermediate steps in
> the reasoning.
> 
> If you want to see this in detail, try explaining why it is that "W is
> coherence-later than E" implies "E must execute before W propagates to
> E's CPU" in the operational model.

But that's all over in explanation.txt??  FWIW, a quick search returned
(wrt fre):

  R ->fre W means that W overwrites the value which R reads, but it
  doesn't mean that W has to execute after R.  All that's necessary
  is for the memory subsystem not to propagate W to R's CPU until
  after R has executed

I really don't see how the operational model could explain even a simple
MP without "knowing" this fact.

IAC, I'm pretty sure my "intermediate steps" wouldn't be using the same
forcing condition.  :-)

  Andrea