kernel/linux.git/tools/memory-model, branch v5.10.257

tools/memory-model: Fix bug in lock.cat

2024-08-19T03:40:58+00:00

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 Reported-by: Andrea Parri Closes: https://lore.kernel.org/linux-arch/ZlC0IkzpQdeGj+a3@andrea/ Tested-by: Andrea Parri Acked-by: Andrea Parri Fixes: 15553dcbca06 ("tools/memory-model: Add model support for spin_is_locked()") CC: Signed-off-by: Paul E. McKenney Signed-off-by: Greg Kroah-Hartman

tools/memory-model: Expand the cheatsheet.txt notion of relaxed

2020-09-04T18:58:15+00:00

This commit adds a key entry enumerating the various types of relaxed operations. While in the area, it also renames the relaxed rows. [ paulmck: Apply Boqun Feng feedback. ] Acked-by: Boqun Feng Signed-off-by: Paul E. McKenney

tools/memory-model: Add a simple entry point document

2020-09-03T16:51:01+00:00

Current LKMM documentation assumes that the reader already understands concurrency in the Linux kernel, which won't necessarily always be the case. This commit supplies a simple.txt file that provides a starting point for someone who is new to concurrency in the Linux kernel. That said, this file might also useful as a reminder to experienced developers of simpler approaches to dealing with concurrency. Link: Link: https://lwn.net/Articles/827180/ [ paulmck: Apply feedback from Joel Fernandes. ] Co-developed-by: Dave Chinner Signed-off-by: Dave Chinner Co-developed-by: Paul E. McKenney Signed-off-by: Paul E. McKenney

tools/memory-model: Improve litmus-test documentation

2020-09-03T16:51:01+00:00

The current LKMM documentation says very little about litmus tests, and worse yet directs people to the herd7 documentation for more information. Now, the herd7 documentation is quite voluminous and educational, but it is intended for people creating and modifying memory models, not those attempting to use them. This commit therefore updates README and creates a litmus-tests.txt file that gives an overview of litmus-test format and describes ways of modeling various special cases, illustrated with numerous examples. [ paulmck: Add Alan Stern feedback. ] [ paulmck: Apply Dave Chinner feedback. ] [ paulmck: Apply Andrii Nakryiko feedback. ] [ paulmck: Apply Johannes Weiner feedback. ] Link: https://lwn.net/Articles/827180/ Reported-by: Dave Chinner Acked-by: Peter Zijlstra (Intel) Signed-off-by: Paul E. McKenney

tools/memory-model: Update recipes.txt prime_numbers.c path

2020-09-03T16:51:00+00:00

The expand_to_next_prime() and next_prime_number() functions have moved from lib/prime_numbers.c to lib/math/prime_numbers.c, so this commit updates recipes.txt to reflect this change. Signed-off-by: Paul E. McKenney

Replace HTTP links with HTTPS ones: LKMM

2020-09-03T16:51:00+00:00

Rationale: Reduces attack surface on kernel devs opening the links for MITM as HTTPS traffic is much harder to manipulate. Deterministic algorithm: For each file: If not .svg: For each line: If doesn't contain `\bxmlns\b`: For each link, `\bhttp://[^# \t\r\n]*(?:\w|/)`: If both the HTTP and HTTPS versions return 200 OK and serve the same content: Replace HTTP with HTTPS. Signed-off-by: Alexander A. Klimov Signed-off-by: Paul E. McKenney

Merge tag 'locking-core-2020-08-03' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip

2020-08-03T21:39:35+00:00

Pull locking updates from Ingo Molnar: - LKMM updates: mostly documentation changes, but also some new litmus tests for atomic ops. - KCSAN updates: the most important change is that GCC 11 now has all fixes in place to support KCSAN, so GCC support can be enabled again. Also more annotations. - futex updates: minor cleanups and simplifications - seqlock updates: merge preparatory changes/cleanups for the 'associated locks' facilities. - lockdep updates: - simplify IRQ trace event handling - add various new debug checks - simplify header dependencies, split out , decouple lockdep from other low level headers some more - fix NMI handling - misc cleanups and smaller fixes * tag 'locking-core-2020-08-03' of git://git.kernel.org/pub/scm/linux/kernel/git/tip/tip: (60 commits) kcsan: Improve IRQ state trace reporting lockdep: Refactor IRQ trace events fields into struct seqlock: lockdep assert non-preemptibility on seqcount_t write lockdep: Add preemption enabled/disabled assertion APIs seqlock: Implement raw_seqcount_begin() in terms of raw_read_seqcount() seqlock: Add kernel-doc for seqcount_t and seqlock_t APIs seqlock: Reorder seqcount_t and seqlock_t API definitions seqlock: seqcount_t latch: End read sections with read_seqcount_retry() seqlock: Properly format kernel-doc code samples Documentation: locking: Describe seqlock design and usage locking/qspinlock: Do not include atomic.h from qspinlock_types.h locking/atomic: Move ATOMIC_INIT into linux/types.h lockdep: Move list.h inclusion into lockdep.h locking/lockdep: Fix TRACE_IRQFLAGS vs. NMIs futex: Remove unused or redundant includes futex: Consistently use fshared as boolean futex: Remove needless goto's futex: Remove put_futex_key() rwsem: fix commas in initialisation docs: locking: Replace HTTP links with HTTPS ones ...

tools/memory-model: Remove smp_read_barrier_depends() from informal doc

2020-07-21T09:50:37+00:00

smp_read_barrier_depends() has gone the way of mmiowb() and so many esoteric memory barriers before it. Drop the two mentions of this deceased barrier from the LKMM informal explanation document. Acked-by: Peter Zijlstra (Intel) Acked-by: Alan Stern Acked-by: Paul E. McKenney Signed-off-by: Will Deacon

tools/memory-model/README: Mention herdtools7 7.56 in compatibility table

2020-06-29T19:05:18+00:00

herdtools7 7.56 is going to be released in the week of 22 Jun 2020. This commit therefore adds the exact version in the compatibility table. Acked-by: Andrea Parri Signed-off-by: Akira Yokosawa Signed-off-by: Paul E. McKenney

tools/memory-model/README: Expand dependency of klitmus7

2020-06-29T19:05:18+00:00

klitmus7 is independent of the memory model but depends on the build-target kernel release. It occasionally lost compatibility due to kernel API changes [1, 2, 3]. It was remedied in a backwards-compatible manner respectively [4, 5, 6]. Reflect this fact in README. [1]: b899a850431e ("compiler.h: Remove ACCESS_ONCE()") [2]: 0bb95f80a38f ("Makefile: Globally enable VLA warning") [3]: d56c0d45f0e2 ("proc: decouple proc from VFS with "struct proc_ops"") [4]: https://github.com/herd/herdtools7/commit/e87d7f9287d1 ("klitmus: Use WRITE_ONCE and READ_ONCE in place of deprecated ACCESS_ONCE") [5]: https://github.com/herd/herdtools7/commit/a0cbb10d02be ("klitmus: Avoid variable length array") [6]: https://github.com/herd/herdtools7/commit/46b9412d3a58 ("klitmus: Linux kernel v5.6.x compat") NOTE: [5] was ahead of herdtools7 7.53, which did not make an official release. Code generated by klitmus7 without [5] can still be built targeting Linux 4.20--5.5 if you don't care VLA warnings. Acked-by: Andrea Parri Signed-off-by: Akira Yokosawa Signed-off-by: Paul E. McKenney