linuxppc-dev.lists.ozlabs.org archive mirror
 help / color / mirror / Atom feed
From: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
To: Will Deacon <will.deacon@arm.com>
Cc: Peter Zijlstra <peterz@infradead.org>,
	Michael Ellerman <mpe@ellerman.id.au>,
	linux-arch@vger.kernel.org, linux-kernel@vger.kernel.org,
	Boqun Feng <boqun.feng@gmail.com>,
	Anton Blanchard <anton@samba.org>,
	Benjamin Herrenschmidt <benh@kernel.crashing.org>,
	Paul Mackerras <paulus@samba.org>,
	linuxppc-dev@lists.ozlabs.org
Subject: Re: [PATCH v2] barriers: introduce smp_mb__release_acquire and update documentation
Date: Mon, 12 Oct 2015 16:30:48 -0700	[thread overview]
Message-ID: <20151012233048.GK3910@linux.vnet.ibm.com> (raw)
In-Reply-To: <20151009183328.GV26278@arm.com>

On Fri, Oct 09, 2015 at 07:33:28PM +0100, Will Deacon wrote:
> On Fri, Oct 09, 2015 at 10:43:27AM -0700, Paul E. McKenney wrote:
> > On Fri, Oct 09, 2015 at 10:51:29AM +0100, Will Deacon wrote:
> > > How do people feel about including these in memory-barriers.txt? I find
> > > them considerably easier to read than our current kernel code + list of
> > > possible orderings + wall of text, but there's a good chance that my
> > > brain has been corrupted from staring at this stuff for too long.
> > > 
> > > The only snag is the ppc assembly code, but it's not *too* horrific ;)
> > 
> > Maybe we should include them as separate files in Documentation/litmus
> > or some such.  We could then use a litmus-test style with Linux-kernel
> > C code, and reference litmus tests for various architectures.  Maybe
> > Documentation/litmus/{arm,arm64,powerpc,x86}/ and so on.
> 
> I think that would be useful, particularly if we had a way to "compile"
> a kernel litmus test into one for a particular architecture.

Very useful!  Probably some limitations, especially for loops and lock
acquisition, but what else is new?

> > For example, the first example in memory-barriers.txt is this:
> > 
> > ------------------------------------------------------------------------
> > 	CPU 1		CPU 2
> > 	===============	===============
> > 	{ A == 1; B == 2 }
> > 	A = 3;		x = B;
> > 	B = 4;		y = A;
> > 
> > The set of accesses as seen by the memory system in the middle can be arranged
> > in 24 different combinations:
> > 
> > 	STORE A=3,	STORE B=4,	y=LOAD A->3,	x=LOAD B->4
> > 	STORE A=3,	STORE B=4,	x=LOAD B->4,	y=LOAD A->3
> > 	STORE A=3,	y=LOAD A->3,	STORE B=4,	x=LOAD B->4
> > 	STORE A=3,	y=LOAD A->3,	x=LOAD B->2,	STORE B=4
> > 	STORE A=3,	x=LOAD B->2,	STORE B=4,	y=LOAD A->3
> > 	STORE A=3,	x=LOAD B->2,	y=LOAD A->3,	STORE B=4
> > 	STORE B=4,	STORE A=3,	y=LOAD A->3,	x=LOAD B->4
> > 	STORE B=4, ...
> > 	...
> > 
> > and can thus result in four different combinations of values:
> > 
> > 	x == 2, y == 1
> > 	x == 2, y == 3
> > 	x == 4, y == 1
> > 	x == 4, y == 3
> > ------------------------------------------------------------------------
> > > > Maybe this changes to:
> > 
> > ------------------------------------------------------------------------
> > Linux MP
> > ""
> > {
> > a=1; b=2;
> > }
> >  P0               | P1                ;
> >  WRITE_ONCE(a, 3) | r1 = READ_ONCE(b) ;
> >  WRITE_ONCE(b, 4) | r2 = READ_ONCE(a) ;
> > 
> > exists (2:r1=4 /\ 2:r2=3)
> > ------------------------------------------------------------------------
> > 
> > We can then state that this assertion can fail.  We could include
> > either ppcmem or herd output along with the litmus tests, which would
> > allow the curious to see a full list of the possible outcomes.
> 
> More importantly, it would allow them to make small changes to the test
> and see what the outcome is, without us having to spawn another
> thread-of-death on LKML :)

Or perhaps we could at least hope for thread-of-tool-supported-death
on LKML.  ;-)

> > > We could also include a link to the ppcmem/herd web frontends and your
> > > lwn.net article. (ppcmem is already linked, but it's not obvious that
> > > you can run litmus tests in your browser).
> > 
> > I bet that the URLs for the web frontends are not stable long term.
> > Don't get me wrong, PPCMEM/ARMMEM has been there for me for a goodly
> > number of years, but professors do occasionally move from one institution
> > to another.  For but one example, Susmit Sarkar is now at University
> > of St. Andrews rather than at Cambridge.
> > 
> > So to make this work, we probably need to be thinking in terms of
> > asking the researchers for permission to include their ocaml code in the
> > Linux-kernel source tree.  I would be strongly in favor of this, actually.
> > 
> > Thoughts?
> 
> I'm extremely hesitant to import a bunch of dubiously licensed, academic
> ocaml code into the kernel. Even if we did, who would maintain it?
> 
> A better solution might be to host a mirror of the code on kernel.org,
> along with a web front-end for people to play with (the tests we're talking
> about here do seem to run ok in my browser).

I am not too worried about how this happens, but we should avoid
constraining the work of our academic partners.  The reason I was thinking
in terms of in the kernel was to avoid version-synchronization issues.
"Wait, this is Linux kernel v4.17, which means that you need to use
version 8.3.5.1 of the tooling...  And with these four patches as well."

							Thanx, Paul

  reply	other threads:[~2015-10-12 23:30 UTC|newest]

Thread overview: 32+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
     [not found] <1444215568-24732-1-git-send-email-will.deacon@arm.com>
     [not found] ` <20151007111915.GF17308@twins.programming.kicks-ass.net>
     [not found]   ` <20151007132317.GK16065@arm.com>
     [not found]     ` <20151007152501.GI3910@linux.vnet.ibm.com>
2015-10-08  3:50       ` [PATCH v2] barriers: introduce smp_mb__release_acquire and update documentation Michael Ellerman
2015-10-08 11:16         ` Peter Zijlstra
2015-10-08 12:59           ` Will Deacon
2015-10-08 22:17             ` Paul E. McKenney
2015-10-09  9:51               ` Will Deacon
2015-10-09 11:25                 ` Peter Zijlstra
2015-10-09 17:44                   ` Paul E. McKenney
2015-10-09 17:43                 ` Paul E. McKenney
2015-10-09 18:33                   ` Will Deacon
2015-10-12 23:30                     ` Paul E. McKenney [this message]
2015-10-20 14:20                       ` Boqun Feng
2015-10-08 21:44           ` Paul E. McKenney
2015-10-09  7:29             ` Peter Zijlstra
2015-10-09  8:31             ` Peter Zijlstra
2015-10-09  9:40               ` Will Deacon
2015-10-09 11:02                 ` Peter Zijlstra
2015-10-09 12:41                   ` Will Deacon
2015-10-09 11:12                 ` Peter Zijlstra
2015-10-09 12:51                   ` Will Deacon
2015-10-09 13:06                     ` Peter Zijlstra
2015-10-09 11:13                 ` Peter Zijlstra
2015-10-09 17:21                 ` Paul E. McKenney
2015-10-19  1:17                 ` Boqun Feng
2015-10-19 10:23                   ` Peter Zijlstra
2015-10-20  7:35                     ` Boqun Feng
2015-10-20 23:34                   ` Paul E. McKenney
2015-10-21  8:24                     ` Peter Zijlstra
2015-10-21 19:29                       ` Paul E. McKenney
2015-10-21 19:36                         ` Peter Zijlstra
2015-10-21 19:56                           ` Paul E. McKenney
2015-10-21 16:04                     ` David Laight
2015-10-21 19:34                       ` Paul E. McKenney

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=20151012233048.GK3910@linux.vnet.ibm.com \
    --to=paulmck@linux.vnet.ibm.com \
    --cc=anton@samba.org \
    --cc=benh@kernel.crashing.org \
    --cc=boqun.feng@gmail.com \
    --cc=linux-arch@vger.kernel.org \
    --cc=linux-kernel@vger.kernel.org \
    --cc=linuxppc-dev@lists.ozlabs.org \
    --cc=mpe@ellerman.id.au \
    --cc=paulus@samba.org \
    --cc=peterz@infradead.org \
    --cc=will.deacon@arm.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).