6.1-stable review patch. If anyone has any objections, please let me know.
------------------
From: Alan Stern stern@rowland.harvard.edu
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 --- tools/memory-model/lock.cat | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-)
--- a/tools/memory-model/lock.cat +++ b/tools/memory-model/lock.cat @@ -102,19 +102,19 @@ let rf-lf = rfe-lf | rfi-lf * 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) - -(* rfe for RU events: an RU may read from an external UL or the initial write *) -let all-possible-rfe-ru = - let possible-rfe-ru r = +(* + * 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) - in map possible-rfe-ru RU + 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 rfe-ru from cross(all-possible-rfe-ru) -let rf-ru = rfe-ru | rfi-ru +with rf-ru from cross(all-possible-rf-ru)
(* Final rf relation *) let rf = rf | rf-lf | rf-ru