Re: Question about PB rule of LKMM

[Andrea Parri <parri.andrea@gmail.com>]

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

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.

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.