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
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 bogged down in
complexities. On the other hand, this is a complicated topic
13 matches
Mail list logo
