lkml.org 
[lkml]   [2019]   [Sep]   [16]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
/
Date
From
SubjectRe: 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

\
 
 \ /
  Last update: 2019-09-16 17:25    [W:0.634 / U:0.044 seconds]
©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site