Date: Fri, 7 Feb 2014 08:44:26 -0800
From: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
To: Torvald Riegel <triegel@redhat.com>
Cc: Will Deacon <will.deacon@arm.com>,
        Ramana Radhakrishnan <Ramana.Radhakrishnan@arm.com>,
        David Howells <dhowells@redhat.com>,
        Peter Zijlstra <peterz@infradead.org>,
        "linux-arch@vger.kernel.org" <linux-arch@vger.kernel.org>,
        "linux-kernel@vger.kernel.org" <linux-kernel@vger.kernel.org>,
        "torvalds@linux-foundation.org" <torvalds@linux-foundation.org>,
        "akpm@linux-foundation.org" <akpm@linux-foundation.org>,
        "mingo@kernel.org" <mingo@kernel.org>,
        "gcc@gcc.gnu.org" <gcc@gcc.gnu.org>
Subject: Re: [RFC][PATCH 0/5] arch: atomic rework
Message-ID: <20140207164425.GM4250@linux.vnet.ibm.com>
Reply-To: paulmck@linux.vnet.ibm.com
References: <20140206134825.305510953@infradead.org>
 <21984.1391711149@warthog.procyon.org.uk>
 <52F3DA85.1060209@arm.com>
 <20140206185910.GE27276@mudshark.cambridge.arm.com>
 <1391720965.23421.3884.camel@triegel.csb>
 <20140206215521.GI4250@linux.vnet.ibm.com>
 <1391727502.23421.4017.camel@triegel.csb>
 <20140207040628.GK4250@linux.vnet.ibm.com>
 <1391764420.23421.4226.camel@triegel.csb>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <1391764420.23421.4226.camel@triegel.csb>
User-Agent: Mutt/1.5.21 (2010-09-15)
Sender: linux-kernel-owner@vger.kernel.org

On Fri, Feb 07, 2014 at 10:13:40AM +0100, Torvald Riegel wrote:
> 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.

Got it.  Agreed, though your other suggestion of substituting CAS is
more convincing.  ;-)

							Thanx, Paul

--
To unsubscribe from this list: send the line "unsubscribe linux-kernel" in
the body of a message to majordomo@vger.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html
Please read the FAQ at  http://www.tux.org/lkml/