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 majord...@vger.kernel.org More majordomo info at http://vger.kernel.org/majordomo-info.html Please read the FAQ at http://www.tux.org/lkml/