Messages in this thread | | | Date | Mon, 16 Sep 2019 11:25:07 -0400 (EDT) | From | Alan Stern <> | Subject | Re: Documentation for plain accesses and data races |
| |
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
| |