b7431b3afd
commit 4c830eef806679dc243e191f962c488dd9d00708 upstream.
Andrea reported that the following innocuous litmus test:
C T
{}
P0(spinlock_t *x)
{
int r0;
spin_lock(x);
spin_unlock(x);
r0 = spin_is_locked(x);
}
gives rise to a nonsensical empty result with no executions:
$ herd7 -conf linux-kernel.cfg T.litmus
Test T Required
States 0
Ok
Witnesses
Positive: 0 Negative: 0
Condition forall (true)
Observation T Never 0 0
Time T 0.00
Hash=6fa204e139ddddf2cb6fa963bad117c0
The problem is caused by a bug in the lock.cat part of the LKMM. Its
computation of the rf relation for RU (read-unlocked) events is
faulty; it implicitly assumes that every RU event must read from
either a UL (unlock) event in another thread or from the lock's
initial state. Neither is true in the litmus test above, so the
computation yields no possible executions.
The lock.cat code tries to make up for this deficiency by allowing RU
events outside of critical sections to read from the last po-previous
UL event. But it does this incorrectly, trying to keep these rfi links
separate from the rfe links that might also be needed, and passing only
the latter to herd7's cross() macro.
The problem is fixed by merging the two sets of possible rf links for
RU events and using them all in the call to cross().
Signed-off-by: Alan Stern <stern@rowland.harvard.edu>
Reported-by: Andrea Parri <parri.andrea@gmail.com>
Closes: https://lore.kernel.org/linux-arch/ZlC0IkzpQdeGj+a3@andrea/
Tested-by: Andrea Parri <parri.andrea@gmail.com>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Fixes: 15553dcbca06 ("tools/memory-model: Add model support for spin_is_locked()")
CC: <stable@vger.kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Signed-off-by: Greg Kroah-Hartman <gregkh@linuxfoundation.org>
143 lines
4.5 KiB
Text
Executable file
143 lines
4.5 KiB
Text
Executable file
// SPDX-License-Identifier: GPL-2.0+
|
|
(*
|
|
* Copyright (C) 2016 Luc Maranget <luc.maranget@inria.fr> for Inria
|
|
* Copyright (C) 2017 Alan Stern <stern@rowland.harvard.edu>
|
|
*)
|
|
|
|
(*
|
|
* Generate coherence orders and handle lock operations
|
|
*)
|
|
|
|
include "cross.cat"
|
|
|
|
(*
|
|
* The lock-related events generated by herd7 are as follows:
|
|
*
|
|
* LKR Lock-Read: the read part of a spin_lock() or successful
|
|
* spin_trylock() read-modify-write event pair
|
|
* LKW Lock-Write: the write part of a spin_lock() or successful
|
|
* spin_trylock() RMW event pair
|
|
* UL Unlock: a spin_unlock() event
|
|
* LF Lock-Fail: a failed spin_trylock() event
|
|
* RL Read-Locked: a spin_is_locked() event which returns True
|
|
* RU Read-Unlocked: a spin_is_locked() event which returns False
|
|
*
|
|
* LKR and LKW events always come paired, like all RMW event sequences.
|
|
*
|
|
* LKR, LF, RL, and RU are read events; LKR has Acquire ordering.
|
|
* LKW and UL are write events; UL has Release ordering.
|
|
* LKW, LF, RL, and RU have no ordering properties.
|
|
*)
|
|
|
|
(* Backward compatibility *)
|
|
let RL = try RL with emptyset
|
|
let RU = try RU with emptyset
|
|
|
|
(* Treat RL as a kind of LF: a read with no ordering properties *)
|
|
let LF = LF | RL
|
|
|
|
(* There should be no ordinary R or W accesses to spinlocks *)
|
|
let ALL-LOCKS = LKR | LKW | UL | LF | RU
|
|
flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses
|
|
|
|
(* Link Lock-Reads to their RMW-partner Lock-Writes *)
|
|
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
|
|
|
|
(*
|
|
* 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 ; [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
|
|
|
|
(*
|
|
* 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 | RU
|
|
let W = W | LKW
|
|
|
|
let Release = Release | UL
|
|
let Acquire = Acquire | LKR
|
|
|
|
(* Match LKW events to their corresponding UL events *)
|
|
let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc)
|
|
|
|
flag ~empty UL \ range(critical) as unmatched-unlock
|
|
|
|
(* Allow up to one unmatched LKW per location; more must deadlock *)
|
|
let UNMATCHED-LKW = LKW \ domain(critical)
|
|
empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks
|
|
|
|
(* rfi for LF events: link each LKW to the LF events in its critical section *)
|
|
let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc)
|
|
|
|
(* rfe for LF events *)
|
|
let all-possible-rfe-lf =
|
|
(*
|
|
* Given an LF event r, compute the possible rfe edges for that event
|
|
* (all those starting from LKW events in other threads),
|
|
* and then convert that relation to a set of single-edge relations.
|
|
*)
|
|
let possible-rfe-lf r =
|
|
let pair-to-relation p = p ++ 0
|
|
in map pair-to-relation ((LKW * {r}) & loc & ext)
|
|
(* Do this for each LF event r that isn't in rfi-lf *)
|
|
in map possible-rfe-lf (LF \ range(rfi-lf))
|
|
|
|
(* Generate all rf relations for LF events *)
|
|
with rfe-lf from cross(all-possible-rfe-lf)
|
|
let rf-lf = rfe-lf | rfi-lf
|
|
|
|
(*
|
|
* RU, i.e., spin_is_locked() returning False, is slightly different.
|
|
* We rely on the memory model to rule out cases where spin_is_locked()
|
|
* within one of the lock's critical sections returns False.
|
|
*)
|
|
|
|
(*
|
|
* rf for RU events: an RU may read from an external UL or the initial write,
|
|
* or from the last po-previous UL
|
|
*)
|
|
let all-possible-rf-ru =
|
|
let possible-rf-ru r =
|
|
let pair-to-relation p = p ++ 0
|
|
in map pair-to-relation ((((UL | IW) * {r}) & loc & ext) |
|
|
(((UL * {r}) & po-loc) \ ([UL] ; po-loc ; [LKW] ; po-loc)))
|
|
in map possible-rf-ru RU
|
|
|
|
(* Generate all rf relations for RU events *)
|
|
with rf-ru from cross(all-possible-rf-ru)
|
|
|
|
(* Final rf relation *)
|
|
let rf = rf | rf-lf | rf-ru
|
|
|
|
(* Generate all co relations, including LKW events but not UL *)
|
|
let co0 = co0 | ([IW] ; loc ; [LKW]) |
|
|
(([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW])
|
|
include "cos-opt.cat"
|
|
let W = W | UL
|
|
let M = R | W
|
|
|
|
(* Merge UL events into co *)
|
|
let co = (co | critical | (critical^-1 ; co))+
|
|
let coe = co & ext
|
|
let coi = co & int
|
|
|
|
(* Merge LKR events into rf *)
|
|
let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1)
|
|
let rfe = rf & ext
|
|
let rfi = rf & int
|
|
|
|
let fr = rf^-1 ; co
|
|
let fre = fr & ext
|
|
let fri = fr & int
|
|
|
|
show co,rf,fr
|