Re: [PATCH v2] barriers: introduce smp_mb__release_acquire and update documentation

[Paul E. McKenney]

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

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