kernel/linux.git/tools/memory-model, branch v6.12.80

tools/memory-model: simple.txt: Fix stale reference to recipes-pairs.txt

2024-09-14T06:56:44+00:00

There has never been recipes-paris.txt at least since v5.11. Fix the typo. Signed-off-by: Akira Yokosawa Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney

tools/memory-model: Add locking.txt and glossary.txt to README

2024-09-14T06:56:44+00:00

locking.txt and glossary.txt have been in LKMM's documentation for quite a while. Add them in README's introduction of docs and the list of docs at the bottom. Add access-marking.txt in the former as well. Signed-off-by: Akira Yokosawa Acked-by: Andrea Parri Cc: Marco Elver Signed-off-by: Paul E. McKenney

tools/memory-model: Document herd7 (abstract) representation

2024-09-14T06:56:43+00:00

The Linux-kernel memory model (LKMM) source code and the herd7 tool are closely linked in that the latter is responsible for (pre)processing each C-like macro of a litmus test, and for providing the LKMM with a set of events, or "representation", corresponding to the given macro. This commit therefore provides herd-representation.txt to document the representations of the concurrency macros, following their "classification" in Documentation/atomic_t.txt. Link: https://lore.kernel.org/all/ZnFZPJlILp5B9scN@andrea/ Suggested-by: Hernan Ponce de Leon Signed-off-by: Andrea Parri Reviewed-by: Boqun Feng Reviewed-by: Hernan Ponce de Leon Signed-off-by: Paul E. McKenney

Merge tag 'kcsan.2024.07.12a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu

2024-07-15T22:44:40+00:00

Pull KCSAN updates from Paul McKenney: - improve the documentation for the new __data_racy type qualifier to the data_race() macro's kernel-doc header and to the LKMM's access-marking documentation - add missing MODULE_DESCRIPTION * tag 'kcsan.2024.07.12a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu: kcsan: Add missing MODULE_DESCRIPTION() macro kcsan: Add example to data_race() kerneldoc header

tools/memory-model: Code reorganization in lock.cat

2024-06-06T18:24:58+00:00

Code reorganization for the lock.cat file in tools/memory-model: Improve the efficiency by ruling out right at the start RU events (spin_is_locked() calls that return False) inside a critical section for the same lock. Improve the organization of the code for handling LF and RU events by pulling the definitions of the pair-to-relation macro out from two different complicated compound expressions, using a single standalone definition instead. Rewrite the calculations of the rf relation for LF and RU events, for greater clarity. Signed-off-by: Alan Stern Tested-by: Andrea Parri Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney

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

2024-06-06T18:24:58+00:00

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

tools/memory-model: Add access-marking.txt to README

2024-06-06T18:24:58+00:00

Given that access-marking.txt exists, this commit makes it easier to find. Reported-by: Akira Yokosawa Signed-off-by: Paul E. McKenney

tools/memory-model: Add KCSAN LF mentorship session citation

2024-06-06T18:23:35+00:00

Add a citation to Marco's LF mentorship session presentation entitled "The Kernel Concurrency Sanitizer" [ paulmck: Apply Marco Elver feedback. ] Reported-by: Marco Elver Signed-off-by: Paul E. McKenney Acked-by: Andrea Parri Reviewed-by: Akira Yokosawa Acked-by: Marco Elver Cc: Alan Stern Cc: Will Deacon Cc: Peter Zijlstra Cc: Boqun Feng Cc: Nicholas Piggin Cc: David Howells Cc: Jade Alglave Cc: Luc Maranget Cc: Daniel Lustig Cc: Joel Fernandes Cc:

kcsan: Add example to data_race() kerneldoc header

2024-05-30T22:06:26+00:00

Although the data_race() kerneldoc header accurately states what it does, some of the implications and usage patterns are non-obvious. Therefore, add a brief locking example and also state how to have KCSAN ignore accesses while also preventing the compiler from folding, spindling, or otherwise mutilating the access. [ paulmck: Apply Bart Van Assche feedback. ] [ paulmck: Apply feedback from Marco Elver. ] Reported-by: Bart Van Assche Signed-off-by: Paul E. McKenney Cc: Marco Elver Cc: Breno Leitao Cc: Jens Axboe

Merge tag 'lkmm-scripting.2023.04.07a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu

2023-04-24T19:02:25+00:00

Pull Linux Kernel Memory Model scripting updates from Paul McKenney: "This improves litmus-test documentation and improves the ability to do before/after tests on the https://github.com/paulmckrcu/litmus repo" * tag 'lkmm-scripting.2023.04.07a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu: (32 commits) tools/memory-model: Remove out-of-date SRCU documentation tools/memory-model: Document LKMM test procedure tools/memory-model: Use "grep -E" instead of "egrep" tools/memory-model: Use "-unroll 0" to keep --hw runs finite tools/memory-model: Make judgelitmus.sh handle scripted Result: tag tools/memory-model: Add data-race capabilities to judgelitmus.sh tools/memory-model: Add checktheselitmus.sh to run specified litmus tests tools/memory-model: Repair parseargs.sh header comment tools/memory-model: Add "--" to parseargs.sh for additional arguments tools/memory-model: Make history-check scripts use mselect7 tools/memory-model: Make checkghlitmus.sh use mselect7 tools/memory-model: Fix scripting --jobs argument tools/memory-model: Implement --hw support for checkghlitmus.sh tools/memory-model: Add -v flag to jingle7 runs tools/memory-model: Make runlitmus.sh check for jingle errors tools/memory-model: Allow herd to deduce CPU type tools/memory-model: Keep assembly-language litmus tests tools/memory-model: Move from .AArch64.litmus.out to .litmus.AArch.out tools/memory-model: Make runlitmus.sh generate .litmus.out for --hw tools/memory-model: Split runlitmus.sh out of checklitmus.sh ...