• Luc Maranget's avatar
    tools/memory-model: Add model support for spin_is_locked() · 15553dcb
    Luc Maranget authored
    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: default avatarLuc Maranget <luc.maranget@inria.fr>
    Signed-off-by: default avatarPaul E. McKenney <paulmck@linux.vnet.ibm.com>
    Reviewed-by: default avatarAlan Stern <stern@rowland.harvard.edu>
    Cc: Akira Yokosawa <akiyks@gmail.com>
    Cc: Andrea Parri <parri.andrea@gmail.com>
    Cc: Andrew Morton <akpm@linux-foundation.org>
    Cc: Boqun Feng <boqun.feng@gmail.com>
    Cc: David Howells <dhowells@redhat.com>
    Cc: Jade Alglave <j.alglave@ucl.ac.uk>
    Cc: Linus Torvalds <torvalds@linux-foundation.org>
    Cc: Luc Maranget <Luc.Maranget@inria.fr>
    Cc: Nicholas Piggin <npiggin@gmail.com>
    Cc: Peter Zijlstra <peterz@infradead.org>
    Cc: Thomas Gleixner <tglx@linutronix.de>
    Cc: Will Deacon <will.deacon@arm.com>
    Cc: linux-arch@vger.kernel.org
    Link: http://lkml.kernel.org/r/1526340837-12222-10-git-send-email-paulmck@linux.vnet.ibm.comSigned-off-by: default avatarIngo Molnar <mingo@kernel.org>
    15553dcb
lock.cat 4.35 KB