user/sven/linux.git/tools/memory-model, branch v6.1.149

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

2024-08-03T06:49:36Z

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: Clarify LKMM's limitations in litmus-tests.txt

2022-08-31T12:15:31Z

As discussed, clarify LKMM not recognizing certain kinds of orderings. In particular, highlight the fact that LKMM might deliberately make weaker guarantees than compilers and architectures. [ paulmck: Fix whitespace issue noted by checkpatch.pl. ] Link: https://lore.kernel.org/all/YpoW1deb%2FQeeszO1@ethstick13.dse.in.tum.de/T/#u Co-developed-by: Alan Stern Signed-off-by: Alan Stern Signed-off-by: Paul Heidekrüger Reviewed-by: Marco Elver Reviewed-by: Joel Fernandes (Google) Cc: Charalampos Mainas Cc: Pramod Bhatotia Cc: Soham Chakraborty Cc: Martin Fink Signed-off-by: Paul E. McKenney

tools/memory-model/README: Update klitmus7 compat table

2022-05-03T17:12:48Z

EXPORT_SYMBOL of do_exec() was removed in v5.17. Unfortunately, kernel modules from klitmus7 7.56 have do_exec() at the end of each kthread. herdtools7 7.56.1 has addressed the issue. Update the compatibility table accordingly. Signed-off-by: Akira Yokosawa Cc: Luc Maranget Cc: Jade Alglave Cc: stable@vger.kernel.org # v5.17+ Signed-off-by: Paul E. McKenney

tools/memory-model: Explain syntactic and semantic dependencies

2022-02-02T01:32:30Z

Paul Heidekrüger pointed out that the Linux Kernel Memory Model documentation doesn't mention the distinction between syntactic and semantic dependencies. This is an important difference, because the compiler can easily break dependencies that are only syntactic, not semantic. This patch adds a few paragraphs to the LKMM documentation explaining these issues and illustrating how they can matter. Suggested-by: Paul Heidekrüger Reviewed-by: Akira Yokosawa Signed-off-by: Alan Stern Signed-off-by: Paul E. McKenney

tools/memory-model: litmus: Add two tests for unlock(A)+lock(B) ordering

2021-12-01T01:47:08Z

The memory model has been updated to provide a stronger ordering guarantee for unlock(A)+lock(B) on the same CPU/thread. Therefore add two litmus tests describing this new guarantee, these tests are simple yet can clearly show the usage of the new guarantee, also they can serve as the self tests for the modification in the model. Co-developed-by: Alan Stern Signed-off-by: Alan Stern Signed-off-by: Boqun Feng Acked-by: Peter Zijlstra (Intel) Signed-off-by: Paul E. McKenney

tools/memory-model: doc: Describe the requirement of the litmus-tests directory

2021-12-01T01:47:08Z

It's better that we have some "standard" about which test should be put in the litmus-tests directory because it helps future contributors understand whether they should work on litmus-tests in kernel or Paul's GitHub repo. Therefore explain a little bit on what a "representative" litmus test is. Signed-off-by: Boqun Feng Acked-by: Peter Zijlstra (Intel) Signed-off-by: Paul E. McKenney

tools/memory-model: Provide extra ordering for unlock+lock pair on the same CPU

2021-12-01T01:47:08Z

A recent discussion[1] shows that we are in favor of strengthening the ordering of unlock + lock on the same CPU: a unlock and a po-after lock should provide the so-called RCtso ordering, that is a memory access S po-before the unlock should be ordered against a memory access R po-after the lock, unless S is a store and R is a load. The strengthening meets programmers' expection that "sequence of two locked regions to be ordered wrt each other" (from Linus), and can reduce the mental burden when using locks. Therefore add it in LKMM. [1]: https://lore.kernel.org/lkml/20210909185937.GA12379@rowland.harvard.edu/ Co-developed-by: Alan Stern Signed-off-by: Alan Stern Signed-off-by: Boqun Feng Reviewed-by: Michael Ellerman (powerpc) Acked-by: Palmer Dabbelt (RISC-V) Acked-by: Peter Zijlstra (Intel) Signed-off-by: Paul E. McKenney

tools/memory-model: Document data_race(READ_ONCE())

2021-07-27T18:48:55Z

It is possible to cause KCSAN to ignore marked accesses by applying __no_kcsan to the function or applying data_race() to the marked accesses. These approaches allow the developer to restrict compiler optimizations while also causing KCSAN to ignore diagnostic accesses. This commit therefore updates the documentation accordingly. Signed-off-by: Paul E. McKenney

tools/memory-model: Heuristics using data_race() must handle all values

2021-07-27T18:48:55Z

Data loaded for use by some sorts of heuristics can tolerate the occasional erroneous value. In this case the loads may use data_race() to give the compiler full freedom to optimize while also informing KCSAN of the intent. However, for this to work, the heuristic needs to be able to tolerate any erroneous value that could possibly arise. This commit therefore adds a paragraph spelling this out. Signed-off-by: Manfred Spraul Signed-off-by: Paul E. McKenney

tools/memory-model: Add example for heuristic lockless reads

2021-07-27T18:47:34Z

This commit adds example code for heuristic lockless reads, based loosely on the sem_lock() and sem_unlock() functions. [ paulmck: Apply Alan Stern and Manfred Spraul feedback. ] Reported-by: Manfred Spraul [ paulmck: Update per Manfred Spraul and Hillf Danton feedback. ] Signed-off-by: Paul E. McKenney