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. > 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. Alan
