Received-SPF: pass (google.com: domain of linux-kernel+bounces-96233-linux.lists.archive=gmail.com@vger.kernel.org designates 139.178.88.99 as permitted sender) client-ip=139.178.88.99;
Date: Thu, 7 Mar 2024 22:06:08 +0100
From: Andrea Parri <parri.andrea@gmail.com>
To: Alan Stern <stern@rowland.harvard.edu>
Cc: Kenneth-Lee-2012@foxmail.com, linux-kernel@vger.kernel.org,
	paulmck@kernel.org
Subject: Re: Question about PB rule of LKMM
Message-ID: <ZeosQDNK8hN/KgJR@andrea>
References: <tencent_744E0AF832049C200F96FD6582D5114D7F0A@qq.com>
 <ZeipiSVLR01jmM6b@andrea>
 <e05fa6a9-c810-46cb-b033-b91ae7a5c382@rowland.harvard.edu>
 <ZejC+lutRuwXQrMz@andrea>
 <Zenip+8BDM3p+MUh@andrea>
 <eb8f2a21-d388-424d-8504-ccd7bdb53a93@rowland.harvard.edu>
 <ZeoFBkB1BeTdEQsn@andrea>
 <bde188b0-1c5b-4b3b-94de-395a52fc37ce@rowland.harvard.edu>
 <ZeoQvj3l6moF9KdQ@andrea>
 <b3137a9b-0776-421f-8b3b-b5ddd6bce96a@rowland.harvard.edu>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <b3137a9b-0776-421f-8b3b-b5ddd6bce96a@rowland.harvard.edu>

> > 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