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

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

2024-08-03T06:54:21+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

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 ...

tools/memory-model: Remove out-of-date SRCU documentation

2023-03-24T17:24:48+00:00

Commit 6cd244c87428 ("tools/memory-model: Provide exact SRCU semantics") changed the semantics of partially overlapping SRCU read-side critical sections (among other things), making such documentation out-of-date. The new, semantic changes are discussed in explanation.txt. Remove the out-of-date documentation. Signed-off-by: Andrea Parri Reviewed-by: Joel Fernandes (Google) Acked-by: Alan Stern Signed-off-by: Paul E. McKenney

tools/memory-model: Document LKMM test procedure

2023-03-24T17:24:15+00:00

This commit documents how to run the various scripts in order to test a potentially pervasive change to the memory model. Signed-off-by: Paul E. McKenney

tools/memory-model: Use "grep -E" instead of "egrep"

2023-03-24T17:24:15+00:00

The latest version of grep claims the egrep is now obsolete so the build now contains warnings that look like: egrep: warning: egrep is obsolescent; using grep -E fix this up by moving the related file to use "grep -E" instead. sed -i "s/egrep/grep -E/g" `grep egrep -rwl tools/memory-model` Here are the steps to install the latest grep: wget http://ftp.gnu.org/gnu/grep/grep-3.8.tar.gz tar xf grep-3.8.tar.gz cd grep-3.8 && ./configure && make sudo make install export PATH=/usr/local/bin:$PATH Signed-off-by: Tiezhu Yang Reviewed-by: Akira Yokosawa Signed-off-by: Paul E. McKenney

tools/memory-model: Use "-unroll 0" to keep --hw runs finite

2023-03-24T17:24:15+00:00

Litmus tests involving atomic operations produce LL/SC loops on a number of architectures, and unrolling these loops can result in excessive verification times or even stack overflows. This commit therefore uses the "-unroll 0" herd7 argument to avoid unrolling, on the grounds that additional passes through an LL/SC loop should not change the verification. Note however, that certain bugs in the mapping of the LL/SC loop to machine instructions may go undetected. On the other hand, herd7 might not be the best vehicle for finding such bugs in any case. (You do stress-test your architecture-specific code, don't you?) Suggested-by: Luc Maranget Signed-off-by: Paul E. McKenney

tools/memory-model: Make judgelitmus.sh handle scripted Result: tag

2023-03-24T17:24:15+00:00

The scripts that generate the litmus tests in the "auto" directory of the https://github.com/paulmckrcu/litmus archive place the "Result:" tag into a single-line ocaml comment, which judgelitmus.sh currently does not recognize. This commit therefore makes judgelitmus.sh recognize both the multiline comment format that it currently does and the automatically generated single-line format. Signed-off-by: Paul E. McKenney

tools/memory-model: Add data-race capabilities to judgelitmus.sh

2023-03-24T17:24:15+00:00

This commit adds functionality to judgelitmus.sh to allow it to handle both the "DATARACE" markers in the "Result:" comments in litmus tests and the "Flag data-race" markers in LKMM output. For C-language tests, if either marker is present, the other must also be as well, at least for litmus tests having a "Result:" comment. If the LKMM output indicates a data race, then failures of the Always/Sometimes/Never portion of the "Result:" prediction are forgiven. The reason for forgiving "Result:" mispredictions is that data races can result in "interesting" compiler optimizations, so that all bets are off in the data-race case. [ paulmck: Apply Akira Yokosawa feedback. ] Signed-off-by: Paul E. McKenney

tools/memory-model: Add checktheselitmus.sh to run specified litmus tests

2023-03-24T17:24:15+00:00

This commit adds a checktheselitmus.sh script that runs the litmus tests specified on the command line. This is useful for verifying fixes to specific litmus tests. Signed-off-by: Paul E. McKenney

tools/memory-model: Repair parseargs.sh header comment

2023-03-24T17:24:15+00:00

Signed-off-by: Paul E. McKenney