This is the mail archive of the
gcc@gcc.gnu.org
mailing list for the GCC project.
Re: [RFC][PATCH 0/5] arch: atomic rework
- From: Torvald Riegel <triegel at redhat dot com>
- To: paulmck at linux dot vnet dot ibm dot com
- Cc: Will Deacon <will dot deacon at arm dot com>, Ramana Radhakrishnan <Ramana dot Radhakrishnan at arm dot com>, David Howells <dhowells at redhat dot com>, Peter Zijlstra <peterz at infradead dot org>, "linux-arch at vger dot kernel dot org" <linux-arch at vger dot kernel dot org>, "linux-kernel at vger dot kernel dot org" <linux-kernel at vger dot kernel dot org>, "torvalds at linux-foundation dot org" <torvalds at linux-foundation dot org>, "akpm at linux-foundation dot org" <akpm at linux-foundation dot org>, "mingo at kernel dot org" <mingo at kernel dot org>, "gcc at gcc dot gnu dot org" <gcc at gcc dot gnu dot org>
- Date: Fri, 07 Feb 2014 10:13:40 +0100
- Subject: Re: [RFC][PATCH 0/5] arch: atomic rework
- Authentication-results: sourceware.org; auth=none
- References: <20140206134825 dot 305510953 at infradead dot org> <21984 dot 1391711149 at warthog dot procyon dot org dot uk> <52F3DA85 dot 1060209 at arm dot com> <20140206185910 dot GE27276 at mudshark dot cambridge dot arm dot com> <1391720965 dot 23421 dot 3884 dot camel at triegel dot csb> <20140206215521 dot GI4250 at linux dot vnet dot ibm dot com> <1391727502 dot 23421 dot 4017 dot camel at triegel dot csb> <20140207040628 dot GK4250 at linux dot vnet dot ibm dot com>
On Thu, 2014-02-06 at 20:06 -0800, Paul E. McKenney wrote:
> On Thu, Feb 06, 2014 at 11:58:22PM +0100, Torvald Riegel wrote:
> > On Thu, 2014-02-06 at 13:55 -0800, Paul E. McKenney wrote:
> > > On Thu, Feb 06, 2014 at 10:09:25PM +0100, Torvald Riegel wrote:
> > > > On Thu, 2014-02-06 at 18:59 +0000, Will Deacon wrote:
> > > > > To answer that question, you need to go and look at the definitions of
> > > > > synchronises-with, happens-before, dependency_ordered_before and a whole
> > > > > pile of vaguely written waffle to realise that you don't know.
> > > >
> > > > Are you familiar with the formalization of the C11/C++11 model by Batty
> > > > et al.?
> > > > http://www.cl.cam.ac.uk/~mjb220/popl085ap-sewell.pdf
> > > > http://www.cl.cam.ac.uk/~mjb220/n3132.pdf
> > > >
> > > > They also have a nice tool that can run condensed examples and show you
> > > > all allowed (and forbidden) executions (it runs in the browser, so is
> > > > slow for larger examples), including nice annotated graphs for those:
> > > > http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/
> > > >
> > > > It requires somewhat special syntax, but the following, which should be
> > > > equivalent to your example above, runs just fine:
> > > >
> > > > int main() {
> > > > atomic_int foo = 0;
> > > > atomic_int bar = 0;
> > > > atomic_int baz = 0;
> > > > {{{ {
> > > > foo.store(42, memory_order_relaxed);
> > > > bar.store(1, memory_order_seq_cst);
> > > > baz.store(42, memory_order_relaxed);
> > > > }
> > > > ||| {
> > > > r1=baz.load(memory_order_seq_cst).readsvalue(42);
> > > > r2=foo.load(memory_order_seq_cst).readsvalue(0);
> > > > }
> > > > }}};
> > > > return 0; }
> > > >
> > > > That yields 3 consistent executions for me, and likewise if the last
> > > > readsvalue() is using 42 as argument.
> > > >
> > > > If you add a "fence(memory_order_seq_cst);" after the store to foo, the
> > > > program can't observe != 42 for foo anymore, because the seq-cst fence
> > > > is adding a synchronizes-with edge via the baz reads-from.
> > > >
> > > > I think this is a really neat tool, and very helpful to answer such
> > > > questions as in your example.
> > >
> > > Hmmm... The tool doesn't seem to like fetch_add(). But let's assume that
> > > your substitution of store() for fetch_add() is correct. Then this shows
> > > that we cannot substitute fetch_add() for atomic_add_return().
> >
> > It should be in this example, I believe.
>
> You lost me on this one.
I mean that in this example, substituting fetch_add() with store()
should not change meaning, given that what the fetch_add reads-from
seems irrelevant.