android_kernel_motorola_sm6375/tools
Repository files (latest commit first)
Filename Latest commit message Latest commit date
Alan Stern 1ca78a7c47 tools/memory-model: Fix bug in lock.cat
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: 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-19 05:33:37 +02:00
..
accounting
arch x86/insn: Fix PUSH instruction in x86 instruction decoder opcode map 2024-06-16 13:28:39 +02:00
bpf bpftool: Fix bug for long instructions in program CFG dumps 2023-05-17 11:35:42 +02:00
build tools features: Add feature test to check if libbfd has buildid support 2023-09-23 11:00:05 +02:00
cgroup
debugging
firewire
firmware
gpio
hv
iio tools: iio: replace seekdir() in iio_generic_buffer 2024-04-13 12:51:39 +02:00
include hugetlb_encode.h: fix undefined behaviour (34 << 26) 2024-07-05 09:08:20 +02:00
io_uring
kvm/kvm_stat
laptop
leds
lib libsubcmd: Fix parse-options memory leak 2024-06-16 13:28:43 +02:00
memory-model tools/memory-model: Fix bug in lock.cat 2024-08-19 05:33:37 +02:00
nfsd
objtool objtool: Add support for intra-function calls 2024-04-13 12:51:29 +02:00
pci
pcmcia
perf perf report: Fix condition in sort__sym_cmp() 2024-08-19 05:33:31 +02:00
power tools/power turbostat: Fix Bzy_MHz documentation typo 2024-05-17 11:43:51 +02:00
scripts
spi
testing selftests: forwarding: devlink_lib: Wait for udev events after reloading 2024-08-19 05:33:30 +02:00
thermal/tmon
time
usb
virtio tools/virtio: fix the vringh test for virtio ring changes 2023-02-22 12:50:34 +01:00
vm
wmi
Makefile