Re: Documentation for plain accesses and data races

[Boqun Feng <boqun.feng@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2325 bytes --]

On Mon, Sep 16, 2019 at 11:22:18AM -0400, Alan Stern wrote:
> On Mon, 16 Sep 2019, Boqun Feng wrote:
> 
> > > executes if Y is a store.)  This is expressed by the visibility
> > > relation (vis), where X ->vis Y is defined to hold if there is an
> > > intermediate event Z such that:
> > > 
> > > 	X is connected to Z by a possibly empty sequence of
> > > 	cumul-fence links followed by an optional rfe link (if none of
> > > 	these links are present, X and Z are the same event),
> > > 
> > 
> > I wonder whehter we could add an optional ->coe or ->fre between X and
> > the possibly empty sequence of cumul-fence, smiliar to the definition
> > of ->prop. This makes sense because if we have
> > 
> > 	X ->coe X' (and X' in on CPU C)
> > 
> > , X must be already propagated to C before X' executed, according to our
> > operation model:
> > 
> > "... In particular, it must arrange for the store to be co-later than
> > (i.e., to overwrite) any other store to the same location which has
> > already propagated to CPU C."
> 
> You have misinterpreted the text.  The operational model says that if X 
> propagates to CPU C before X' executes then X ->coe X'.  It does _not_ 
> say that if X ->coe X' then X propagates to CPU C before X' executes.
> 

Alright, I got confused. If X ->coe X', we only have "X must execute
before X' propagated to the CPU of X" (otherwise, we will have X' ->coe
X), so we will only know the execution time of X (not the propagation
time) is before the propagation of X' to the CPU of X, and that won't
help build the visiblity, because we know zero about the propagation
time of X to any CPU.

> > In other words, we can define ->vis as:
> > 
> > 	let vis = prop ; ((strong-fence ; [Marked] ; xbstar) | (xbstar & int))
> > 
> > , and for this document, reference the "prop" section in
> > explanation.txt. This could make the model simple (both for description
> > and explanation), and one better thing is that we won't need commit in
> > Paul's dev branch:
> > 	
> > 	c683f2c807d2 "tools/memory-model: Fix data race detection for unordered store and load"
> > 
> > , and data race rules will look more symmetrical ;-)
> > 
> > Thoughts? Or am I missing something subtle here?
> 
> See above.
> 

Thanks!

Regards,
Boqun

> Alan
> 

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]