Question about PB rule of LKMM
From: Kenneth-Lee-2012
Date: Thu Feb 29 2024 - 22:20:00 EST
Hi, there,
I'm new to LKMM. May I ask a may-be-stupid question?
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?
Can anyone explain this? Thank you in advance.
- Kenneth Lee