Re: Question about PB rule of LKMM

[Kenneth-Lee-2012]

On Tue, Mar 05, 2024 at 07:00:55PM +0100, Andrea Parri wrote:
> Date: Tue, 5 Mar 2024 19:00:55 +0100
> From: Andrea Parri <parri.andrea@xxxxxxxxx>
> To: Kenneth-Lee-2012@xxxxxxxxxxx
> Cc: linux-kernel@xxxxxxxxxxxxxxx, stern@xxxxxxxxxxxxxxxxxxx,
>  paulmck@xxxxxxxxxx
> Subject: Re: Question about PB rule of LKMM
> 
> (Expanding Cc:,)
> 
> > In the LKMM document, it said the pb link:
> > 
> >    E ->coe W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F
> > 
> > can make sure E execute before F. But the cat file define pb as follow:
> > 
> >   let pb = prop ; strong-fence ; hb* ; [Marked]
> >   acyclic pb as propagation
> > 
> > So the acyclic rule is only on pb relationshit itself. So it won't
> > forbid F -rfe-> E, will it? It only forgit F -pb-> E. So how can
> > propagation rule ensure E execute before F?
> 
> With regard to your first question, the propagation rule does indeed forbid
> F ->rfe E.  To see why, suppose that F ->rfe E (in particular, E is a load
> and the first link in your sequence is fre instead of coe).  Then
> 
>    E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F ->rfe E.
> 
> Since any rfe-link is an hb-link (by definition of the hb-relation), the
> previous expression can be written as follows:
> 
>    E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* F ->hb E,
> 
> that is, given that hb* is the reflexive transitive closure of hb,
> 
>    E ->fre W ->cumul-fence* X ->rfe? Y ->strong-fence Z ->hb* E,
> 
> contradicting the fact that pb is acyclic.  An argument similar to the one
> reported above can show that the propagation rule forbids F ->hb E.
> 

Wow, my gosh, I didn't expect the last "hb*" works like this:). Very clear
explaination, thank you very much.

> To address the second question, I'd start by first remarking that the CAT
> file doesn't define an "execute-before" relation currently.  This file does
> however include the following comment:
> 
> (*
>  * The happens-before, propagation, and rcu constraints are all
>  * expressions of temporal ordering.  They could be replaced by
>  * a single constraint on an "executes-before" relation, xb:
>  *
>  * let xb = hb | pb | rb
>  * acyclic xb as executes-before
>  *)
> 
> In this sense, the propagation rule (like other "acyclicity"-constraints of
> the LKMM) expresses "temporal ordering", and any pb-link is (by definition)
> an "execute-before"-link.  The file explanation.txt can provide additional
> context/information, based on the (informal) operational model described in
> that file, about this matter.

So it is just a rule in the sence of mathematics? I think it would be better
if there were some explaination in the explaination file. It is
descripted in nature language, the reader might not notify it is just a
mathematics rule. And you cannot say an action executes before another
because they are in the pb link. It becomes a cycling in logic...

But anyway, now I understand. Thank you very much.

> 
> Notice that, as examples in tools/memory-model/litmus-tests/ can illustrate,
> none of the three components of the xb-relation is redundant.  Specifically,
> there do exist pb-links/cycles which are not hb-link/cycles (and viceversa).
> 
> Maintaining three distinct/separate constraints (happens-before, propagation,
> and rcu) instead of a single "executes-before" constraint, although formally
> unnecessary, highlights the modularity and eases the debugging of the LKMM.

-- 
			-Kenneth Lee