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).
Notice that herd7 installations strictly older than version 7.49
do not handle the new constructs.
Signed-off-by: Luc Maranget <luc.maranget@inria.fr>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will.deacon@arm.com>
Cc: Peter Zijlstra <peterz@infradead.org>
Cc: Boqun Feng <boqun.feng@gmail.com>
Cc: Nicholas Piggin <npiggin@gmail.com>
Cc: David Howells <dhowells@redhat.com>
Cc: Jade Alglave <j.alglave@ucl.ac.uk>
Cc: Luc Maranget <luc.maranget@inria.fr>
Cc: "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>
Cc: Akira Yokosawa <akiyks@gmail.com>
Cc: Ingo Molnar <mingo@redhat.com>
Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index 397e4e6..2012104 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -37,6 +37,7 @@
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}; }
diff --git a/tools/memory-model/lock.cat b/tools/memory-model/lock.cat
index ba4a4ec..0227b07 100644
--- a/tools/memory-model/lock.cat
+++ b/tools/memory-model/lock.cat
@@ -5,7 +5,11 @@
*)
(* Generate coherence orders and handle lock operations *)
-
+(*
+ * Warning, crashes with herd7 versions strictly before 7.48.
+ * spin_islocked is functional from version 7.49.
+ *
+ *)
include "cross.cat"
(* From lock reads to their partner lock writes *)
@@ -32,12 +36,16 @@
(* The final value of a spinlock should not be tested *)
flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
-
+(*
+ * Backward compatibility
+ *)
+let RL = try RL with emptyset (* defined herd7 >= 7.49 *)
+let RU = try RU with emptyset (* defined herd7 >= 7.49 *)
(*
* Put lock operations in their appropriate classes, but leave UL out of W
* until after the co relation has been generated.
*)
-let R = R | LKR | LF
+let R = R | LKR | LF | RL | RU
let W = W | LKW
let Release = Release | UL
@@ -72,8 +80,45 @@
(* Generate all rf relations for LF events *)
with rfe-lf from cross(all-possible-rfe-lf)
-let rf = rf | rfi-lf | rfe-lf
+let rf-lf = rfe-lf | rfi-lf
+
+(* rf for RL events, ie islocked returning true, similar to LF above *)
+
+(* islocked returning true inside a critical section
+ * must read from the opening lock *)
+ *)
+let rfi-rl = ([LKW] ; po-loc ; [RL]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
+
+(* islocked returning true outside critical sections can match any
+ * external lock.
+ *)
+let all-possible-rfe-rl =
+ let possible-rfe-lf r =
+ let pair-to-relation p = p ++ 0
+ in map pair-to-relation ((LKW * {r}) & loc & ext)
+ in map possible-rfe-lf (RL \ range(rfi-rl))
+
+with rfe-rl from cross(all-possible-rfe-rl)
+let rf-rl = rfe-rl | rfi-rl
+
+(* Read from unlock, ie islocked returning false, slightly different *)
+
+(* islocked returning false can read from the last po-previous unlock *)
+let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
+
+(* any islocked returning false can read from any external unlock *)
+let all-possible-rfe-ru =
+ let possible-rfe-ru r =
+ let pair-to-relation p = p ++ 0
+ in map pair-to-relation (((UL|IW) * {r}) & loc & ext)
+ in map possible-rfe-ru RU
+
+with rfe-ru from cross(all-possible-rfe-ru)
+let rf-ru = rfe-ru | rfi-ru
+
+(* Final rf relation *)
+let rf = rf | rf-lf | rf-rl | rf-ru
(* Generate all co relations, including LKW events but not UL *)
let co0 = co0 | ([IW] ; loc ; [LKW]) |
