Re: Question about PB rule of LKMM

[Kenneth-Lee-2012]

On Thu, Mar 07, 2024 at 08:08:46PM +0100, Andrea Parri wrote:
> Date: Thu, 7 Mar 2024 20:08:46 +0100
> From: Andrea Parri <parri.andrea@xxxxxxxxx>
> To: Alan Stern <stern@xxxxxxxxxxxxxxxxxxx>
> Cc: Kenneth-Lee-2012@xxxxxxxxxxx, linux-kernel@xxxxxxxxxxxxxxx,
>  paulmck@xxxxxxxxxx
> Subject: Re: Question about PB rule of LKMM
> 
> > > I'd disagree with these premises: certain instructions can and do execute
> > > at the same time.
> > 
> > Can you give an example?
> 
> I think I'm starting to see where this is going..., but to address the
> question: really any example where the LKMM doesn't know better, say
> 
> C test
> 
> {}
> 
> P0(int *x)
> {
> 	*x = 1;
> }
> 
> P1(int *x)
> {
> 	*x = 2;
> }
> 

TBH, the concept "execute-before" gave me a lot of trouble when I read
explanation.txt at the very beginning. The name hints an absolute and
global timeline over everything. But that makes no sense because no one
can observe that order at all. So till now, I still need to translate
the concept to an order by particular observer , such as a CPU or the
memory system, for further understanding.

And speaking of example, can I ask another question?: 

In the "THE HAPPENS-BEFORE RELATION: hb" section of explanation.txt,
it uses the following example to explain the prop relation:

	P0()
	{
		int r1;

		WRITE_ONCE(x, 1);
		r1 = READ_ONCE(x);
	}

	P1()
	{
		WRITE_ONCE(x, 8);
	}

if r1 = 8, we can deduce P0:Wx1 ->coe P1:Wx8 ->rfe P0:Rx, this can be
explained with the operational model. But according to the definition of
prop,

  let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked]

The link should contain a cumul-fence, which doesn't exist in the
example.

This also makes me confuse on what explanation.txt explains: the
dependable rule/link deduced from operational model, or the physical
meaning of the concepts used in the cat definition?

Alan's discussion make feel the answer is former. If it is, my question is
closed. But I feel it should be latter. In this case, I think we cannot
just explain "it can be explained in the operational model";)

(CC Alan: I couldn't receive your previous email in this topic, I think
it is because I'm not a subscriber of lkml. I would be very grateful if
you could cc me in the follow-up email)

> 
> > >  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).
> 
> 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.  :-)
> 
> 
> > > > 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.
> 
> Well, I read that sentence but stopped at "These contradictions show that"
> for the reason I detailed above.
> 
>   Andrea

-- 
			-Kenneth Lee (Hisilicon)