tools/memory-model: Fix bug in lock.cat
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: 15553dcbca
("tools/memory-model: Add model support for spin_is_locked()")
CC: <stable@vger.kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
This commit is contained in:
parent
520c637bf0
commit
4c830eef80
@ -102,19 +102,19 @@ let rf-lf = rfe-lf | rfi-lf
|
|||||||
* within one of the lock's critical sections returns False.
|
* within one of the lock's critical sections returns False.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
(* rfi for RU events: an RU may read from the last po-previous UL *)
|
(*
|
||||||
let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc)
|
* rf for RU events: an RU may read from an external UL or the initial write,
|
||||||
|
* or from the last po-previous UL
|
||||||
(* rfe for RU events: an RU may read from an external UL or the initial write *)
|
*)
|
||||||
let all-possible-rfe-ru =
|
let all-possible-rf-ru =
|
||||||
let possible-rfe-ru r =
|
let possible-rf-ru r =
|
||||||
let pair-to-relation p = p ++ 0
|
let pair-to-relation p = p ++ 0
|
||||||
in map pair-to-relation (((UL | IW) * {r}) & loc & ext)
|
in map pair-to-relation ((((UL | IW) * {r}) & loc & ext) |
|
||||||
in map possible-rfe-ru RU
|
(((UL * {r}) & po-loc) \ ([UL] ; po-loc ; [LKW] ; po-loc)))
|
||||||
|
in map possible-rf-ru RU
|
||||||
|
|
||||||
(* Generate all rf relations for RU events *)
|
(* Generate all rf relations for RU events *)
|
||||||
with rfe-ru from cross(all-possible-rfe-ru)
|
with rf-ru from cross(all-possible-rf-ru)
|
||||||
let rf-ru = rfe-ru | rfi-ru
|
|
||||||
|
|
||||||
(* Final rf relation *)
|
(* Final rf relation *)
|
||||||
let rf = rf | rf-lf | rf-ru
|
let rf = rf | rf-lf | rf-ru
|
||||||
|
Loading…
Reference in New Issue
Block a user