On Fri, 27 Sep 2019, Andrea Parri wrote:
> On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
> > Folks:
> >
> > I have spent some time writing up a section for
> > tools/memory-model/Documentation/explanation.txt on plain accesses and
> > data races. The initial version is below.
> >
On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
> Folks:
>
> I have spent some time writing up a section for
> tools/memory-model/Documentation/explanation.txt on plain accesses and
> data races. The initial version is below.
>
> I'm afraid it's rather long and perhaps gets too bog
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:
> > >
> > >
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..
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
On Mon, Sep 16, 2019 at 01:17:53PM +0800, Boqun Feng wrote:
> Hi Alan,
>
> I spend some time reading this, really helpful! Thanks.
>
> Please see comments below:
>
> On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
> [...]
> > If two memory accesses aren't concurrent then one must exe
Hi Alan,
I spend some time reading this, really helpful! Thanks.
Please see comments below:
On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
[...]
> If two memory accesses aren't concurrent then one must execute before
> the other. Therefore the LKMM decides two accesses aren't concu
On Fri, Sep 13, 2019 at 03:13:26PM -0400, Alan Stern wrote:
> On Thu, 12 Sep 2019, Paul E. McKenney wrote:
>
> > On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
>
> > > To this end, the LKMM imposes three extra restrictions, together
> > > called the "plain-coherence" axiom because of
On Fri, Sep 13, 2019 at 11:21:17AM -0400, Alan Stern wrote:
> On Thu, 12 Sep 2019, Paul E. McKenney wrote:
> > On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
> > > Folks:
> > >
> > > I have spent some time writing up a section for
> > > tools/memory-model/Documentation/explanation.tx
On Thu, 12 Sep 2019, Paul E. McKenney wrote:
> On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
> > To this end, the LKMM imposes three extra restrictions, together
> > called the "plain-coherence" axiom because of their resemblance to the
> > coherency rules:
> >
> > If R and W c
On Thu, 12 Sep 2019, Paul E. McKenney wrote:
> On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
> > Folks:
> >
> > I have spent some time writing up a section for
> > tools/memory-model/Documentation/explanation.txt on plain accesses and
> > data races. The initial version is below.
On Fri, Sep 06, 2019 at 02:11:29PM -0400, Alan Stern wrote:
> Folks:
>
> I have spent some time writing up a section for
> tools/memory-model/Documentation/explanation.txt on plain accesses and
> data races. The initial version is below.
>
> I'm afraid it's rather long and perhaps gets too bog
12 matches
Mail list logo
