Alan Stern 4b89bfaefb tools/memory-model: Fix bug in lock.cat ... commit 4c830eef80 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: 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> Signed-off-by: Greg Kroah-Hartman <gregkh@linuxfoundation.org>		2024-08-03 09:00:43 +02:00
..
accounting
arch	tools headers arm64: Sync arm64's cputype.h with the kernel sources	2024-06-04 16:46:40 -03:00
bootconfig
bpf	bpftool: Mount bpffs when pinmaps path not under the bpffs	2024-08-03 08:59:42 +02:00
build
certs
cgroup	proc: rewrite stable_page_flags()	2024-04-25 20:56:15 -07:00
counter
crypto
debugging
firewire
firmware
gpio
hv	tools: hv: suppress the invalid warning for packed member alignment	2024-05-28 05:27:35 +00:00
iio
include	perf tools fixes for v6.10: 2nd batch	2024-06-09 09:04:51 -07:00
kvm/kvm_stat
laptop
leds
lib	libbpf: Skip base btf sanity checks	2024-08-03 08:59:40 +02:00
memory-model	tools/memory-model: Fix bug in lock.cat	2024-08-03 09:00:43 +02:00
mm
net/ynl	ynl: ensure exact-len value is resolved	2024-05-13 14:59:24 -07:00
objtool	x86/syscall: Mark exit[_group] syscall handlers __noreturn	2024-08-03 08:59:12 +02:00
pci
pcmcia
perf	perf dso: Fix address sanitizer build	2024-08-03 09:00:05 +02:00
power	tools/power turbostat: Add local build_bug.h header for snapshot target	2024-06-27 23:53:27 -04:00
rcu
scripts
sound	ASoC: dapm-graph: new tool to visualize DAPM state	2024-04-21 09:58:17 +09:00
spi
testing	selftests/nolibc: fix printf format mismatch in expect_str_buf_eq()	2024-08-03 09:00:33 +02:00
thermal
time
tracing	tools/latency-collector: Fix -Wformat-security compile warns	2024-05-23 10:46:01 -04:00
usb
verification
virtio
wmi
workqueue
writeback	writeback: add wb_monitor.py script to monitor writeback info on bdi	2024-05-05 17:53:51 -07:00
Makefile