Re: Question about PB rule of LKMM

[Andrea Parri]

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

I think you're on to something, explaining mathematical axioms or rules has
never been an easy task AFAIU.  ;-)  (and that's why feedback is welcome)

The remark could be to continue to consider such rules "generalizations" of
properties met by several hardware models or other specific contexts, rather
than (mere) logically-derived facts.

  Andrea