Received-SPF: pass (google.com: domain of linux-kernel+bounces-97601-linux.lists.archive=gmail.com@vger.kernel.org designates 139.178.88.99 as permitted sender) client-ip=139.178.88.99;
Date: Fri, 8 Mar 2024 22:29:20 +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: <ZeuDMKtVotRefSm3@andrea>
References: <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>
 <ZeosQDNK8hN/KgJR@andrea>
 <198f16f6-1d61-4868-b522-1bc5d34bf7af@rowland.harvard.edu>
Precedence: bulk
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <198f16f6-1d61-4868-b522-1bc5d34bf7af@rowland.harvard.edu>

> 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