From 15553dcbca0638de57047e79b9fb4ea77aa04db3 Mon Sep 17 00:00:00 2001 From: Luc Maranget Date: Mon, 14 May 2018 16:33:48 -0700 Subject: tools/memory-model: Add model support for spin_is_locked() 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/linux-kernel.def | 1 + 1 file changed, 1 insertion(+) (limited to 'tools/memory-model/linux-kernel.def') diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index 6bd3bc431b3d..f0553bd37c08 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -38,6 +38,7 @@ cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W) spin_lock(X) { __lock(X); } spin_unlock(X) { __unlock(X); } spin_trylock(X) __trylock(X) +spin_is_locked(X) __islocked(X) // RCU rcu_read_lock() { __fence{rcu-lock}; } -- cgit v1.2.3