tools/memory-model: Remove out-of-date comments and code from lock.cat
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 <andrea.parri@amarulasolutions.com> [ paulmck: Pulled as lock-nest into previous line as discussed. ] Signed-off-by: Alan Stern <stern@rowland.harvard.edu> Signed-off-by: Paul E. McKenney <paulmck@linux.vnet.ibm.com> Cc: Akira Yokosawa <akiyks@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 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 <mingo@kernel.org>
This commit is contained in:
parent
30b795df11
commit
cee0321a40
|
@ -47,18 +47,15 @@ flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
|
|||
let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po)
|
||||
let rmw = rmw | lk-rmw
|
||||
|
||||
(* The litmus test is invalid if an LKR/LKW event is not part of an RMW pair *)
|
||||
flag ~empty LKW \ range(lk-rmw) as unpaired-LKW
|
||||
flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
|
||||
|
||||
(*
|
||||
* A paired LKR must always see an unlocked value; spin_lock() calls nested
|
||||
* An LKR must always see an unlocked value; spin_lock() calls nested
|
||||
* inside a critical section (for the same lock) always deadlock.
|
||||
*)
|
||||
empty ([LKW] ; po-loc ; [domain(lk-rmw)]) \ (po-loc ; [UL] ; po-loc)
|
||||
as lock-nest
|
||||
|
||||
(* The litmus test is invalid if an LKW event is not part of an RMW pair *)
|
||||
flag ~empty LKW \ range(lk-rmw) as unpaired-LKW
|
||||
|
||||
(* This will be allowed if we implement spin_is_locked() *)
|
||||
flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR
|
||||
empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest
|
||||
|
||||
(* The final value of a spinlock should not be tested *)
|
||||
flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final
|
||||
|
|
Loading…
Reference in New Issue