pm24.git/tools/memory-model, branch v4.18-rc2

tools/memory-model: Add reference for 'Simplifying ARM concurrency'

2018-05-15T06:11:19Z

The paper discusses the revised ARMv8 memory model; such revision had an important impact on the design of the LKMM. Signed-off-by: Andrea Parri Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa Cc: Alan Stern 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 Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-19-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Update ASPLOS information

2018-05-15T06:11:18Z

ASPLOS 2018 was held in March: make sure this is reflected in header comments and references. Signed-off-by: Andrea Parri Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa Cc: Alan Stern 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 Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-18-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Fix coding style in 'lock.cat'

2018-05-15T06:11:18Z

This commit uses tabs for indentation and adds spaces around binary operator. Signed-off-by: Andrea Parri 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-16-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Remove out-of-date comments and code from lock.cat

2018-05-15T06:11:18Z

lock.cat contains old comments and code referring to the possibility of LKR events that are not part of an RMW pair. This is a holdover from when I though we might end up using LKR events to implement spin_is_locked(). Reword the comments to remove this assumption and replace domain(lk-rmw) in the code with LKR. Tested-by: Andrea Parri [ paulmck: Pulled as lock-nest into previous line as discussed. ] Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa 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 Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-15-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Improve mixed-access checking in lock.cat

2018-05-15T06:11:18Z

The code in lock.cat which checks for normal read/write accesses to spinlock variables doesn't take into account the newly added RL and RU events. Add them into the test, and move the resulting code up near the start of the file, since a violation would indicate a pretty severe conceptual error in a litmus test. Tested-by: Andrea Parri Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa 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 Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-14-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Improve comments in lock.cat

2018-05-15T06:11:18Z

This patch improves the comments in tools/memory-model/lock.cat. In addition to making the text more uniform and removing redundant comments, it adds a description of all the possible locking events that herd can generate. Tested-by: Andrea Parri Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa 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 Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-13-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

tools/memory-model: Remove duplicated code from lock.cat

2018-05-15T06:11:17Z

This patch simplifies the implementation of spin_is_locked in the LKMM. It capitalizes on the fact that a failed spin_trylock() and a spin_is_locked() which returns True have exactly the same semantics (those of READ_ONCE) and ordering properties (none). Therefore the two kinds of events can be combined and handled by the same code, instead of treated separately as they are currently. Tested-by: Andrea Parri Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney Cc: Akira Yokosawa 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 Cc: parri.andrea@gmail.com Link: http://lkml.kernel.org/r/1526340837-12222-12-git-send-email-paulmck@linux.vnet.ibm.com Signed-off-by: Ingo Molnar

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

2018-05-15T06:11:17Z

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:17Z

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:17Z

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