| From 4c830eef806679dc243e191f962c488dd9d00708 Mon Sep 17 00:00:00 2001 |
| From: Alan Stern <stern@rowland.harvard.edu> |
| Date: Thu, 6 Jun 2024 09:57:55 -0400 |
| Subject: tools/memory-model: Fix bug in lock.cat |
| |
| 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 |
