Re: Documentation for plain accesses and data races

[Alan Stern]

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