BMC/Intel-BMC/linux.git/tools/memory-model/litmus-tests, branch dev-4.19

tools/memory-model: Rename litmus tests to comply to norm7

2018-07-17T07:30:36+00:00

norm7 produces the 'normalized' name of a litmus test, when the test can be generated from a single cycle that passes through each process exactly once. The commit renames such tests in order to comply to the naming scheme implemented by this tool. Signed-off-by: Andrea Parri Signed-off-by: Paul E. McKenney Acked-by: Alan Stern Cc: Akira Yokosawa Cc: Boqun Feng Cc: David Howells Cc: Jade Alglave Cc: Linus Torvalds Cc: Luc Maranget Cc: Nicholas Piggin Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: linux-arch@vger.kernel.org Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/20180716180605.16115-14-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Fix ISA2+pooncelock+pooncelock+pombonce name

2018-07-17T07:29:31+00:00

The names on the first line of the litmus tests are arbitrary, but the convention is that they be the filename without the trailing ".litmus". This commit therefore removes the stray trailing ".litmus" from ISA2+pooncelock+pooncelock+pombonce.litmus's name. Reported-by: Andrea Parri Signed-off-by: Paul E. McKenney Acked-by: Alan Stern Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180716180605.16115-2-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Add litmus test for full multicopy atomicity

2018-07-17T07:29:29+00:00

This commit adds a litmus test suggested by Alan Stern that is forbidden on fully multicopy atomic systems, but allowed on other-multicopy and on non-multicopy atomic systems. For reference, s390 is fully multicopy atomic, x86 and ARMv8 are other-multicopy atomic, and ARMv7 and powerpc are non-multicopy atomic. Suggested-by: Alan Stern Signed-off-by: Paul E. McKenney Acked-by: Alan Stern Acked-by: Andrea Parri Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/20180716180605.16115-1-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Flag "cumulativity" and "propagation" tests

2018-05-15T06:11:17+00:00

This commit flags WRC+pooncerelease+rmbonceonce+Once.litmus as being forbidden by smp_store_release() A-cumulativity and IRIW+mbonceonces+OnceOnce.litmus as being forbidden by the LKMM propagation rule. Suggested-by: Andrea Parri Reported-by: Paolo Bonzini [ paulmck: Updated wording as suggested by Alan Stern. ] Signed-off-by: Paul E. McKenney Acked-by: Alan Stern Cc: Andrew Morton Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-11-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Add model support for spin_is_locked()

2018-05-15T06:11:17+00:00

This commit first adds a trivial macro for spin_is_locked() to linux-kernel.def. It also adds cat code for enumerating all possible matches of lock write events (set LKW) with islocked events returning true (set RL, for Read from Lock), and unlock write events (set UL) with islocked events returning false (set RU, for Read from Unlock). Note that this intentionally does not model uniprocessor kernels (CONFIG_SMP=n) built with CONFIG_DEBUG_SPINLOCK=n, in which spin_is_locked() unconditionally returns zero. It also adds a pair of litmus tests demonstrating the minimal ordering provided by spin_is_locked() in conjunction with spin_lock(). Will Deacon noted that this minimal ordering happens on ARMv8: https://lkml.kernel.org/r/20180226162426.GB17158@arm.com Notice that herd7 installations strictly older than version 7.49 do not handle the new constructs. Signed-off-by: Luc Maranget Signed-off-by: Paul E. McKenney Reviewed-by: Alan Stern Cc: Akira Yokosawa Cc: Andrea Parri Cc: Andrew Morton Cc: Boqun Feng Cc: David Howells Cc: Jade Alglave Cc: Linus Torvalds Cc: Luc Maranget Cc: Nicholas Piggin Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: linux-arch@vger.kernel.org Link: http://lkml.kernel.org/r/1526340837-12222-10-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Add scripts to test memory model

2018-05-15T06:11:17+00:00

This commit adds a pair of scripts that run the memory model on litmus tests, checking that the verification result of each litmus test matches the result flagged in the litmus test itself. These scripts permit easier checking of changes to the memory model against preconceived notions. To run the scripts, go to the tools/memory-model directory and type "scripts/checkalllitmus.sh". If all is well, the last line printed will be "All litmus tests verified as was expected." Signed-off-by: Paul E. McKenney Cc: Andrew Morton Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: Will Deacon Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Link: http://lkml.kernel.org/r/1526340837-12222-9-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Add documentation of new litmus test

2018-03-10T09:22:23+00:00

The litmus-tests/README file lacks any mention of the new litmus test ISA2+pooncelock+pooncelock+pombonce.litmus. This commit therefore adds a description of this test. Reported-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Linus Torvalds Cc: Peter Zijlstra Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1520443660-16858-3-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Add a S lock-based external-view litmus test

2018-02-21T08:58:15+00:00

This commit adds a litmus test in which P0() and P1() form a lock-based S litmus test, with the addition of P2(), which observes P0()'s and P1()'s accesses with a full memory barrier but without the lock. This litmus test asks whether writes carried out by two different processes under the same lock will be seen in order by a third process not holding that lock. The answer to this question is "yes" for all architectures supporting the Linux kernel, but is "no" according to the current version of LKMM. A patch to LKMM is under development. Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Acked-by: Peter Zijlstra Cc: Linus Torvalds Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-10-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

README: Fix a couple of punctuation errors

2018-02-21T08:58:14+00:00

Signed-off-by: Paul E. McKenney Acked-by: Peter Zijlstra Cc: Linus Torvalds Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-5-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

EXP litmus_tests: Add comments explaining tests' purposes

2018-02-21T08:58:13+00:00

This commit adds comments to the litmus tests summarizing what these tests are intended to demonstrate. [ paulmck: Apply Andrea's and Alan's feedback. ] Suggested-by: Ingo Molnar Signed-off-by: Paul E. McKenney Acked-by: Peter Zijlstra Cc: Linus Torvalds Cc: Thomas Gleixner Cc: akiyks@gmail.com Cc: boqun.feng@gmail.com Cc: dhowells@redhat.com Cc: j.alglave@ucl.ac.uk Cc: linux-arch@vger.kernel.org Cc: luc.maranget@inria.fr Cc: nborisov@suse.com Cc: npiggin@gmail.com Cc: parri.andrea@gmail.com Cc: stern@rowland.harvard.edu Cc: will.deacon@arm.com Link: http://lkml.kernel.org/r/1519169112-20593-4-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar