On Mon, 16 Sep 2019, Boqun Feng wrote:
> > In other words, we can define ->vis as:
> >
> > let vis = prop ; ((strong-fence ; [Marked] ; xbstar) | (xbstar & int))
> >
>
> Hmm.. so the problem with this approach is that the (xbstar & int) part
> doesn't satisfy the requirement of visibility... i.e.
>
> X ->prop Z ->(xbstar & int) Y
>
> may not guarantee when Y executes, X is already propagated to Y's CPU.
Yes, it doesn't guarantee this. But the reason it doesn't guarantee
this is because of the prop. The (xbstar & int) part is okay. In
other words, if
Z ->(xbstar & int) Y
then it is certainly true that any store propagating to Z's CPU before
Z executes also propagates to Y's CPU (which is the same one) before Y
executes.
Alan
