- Jul 27, 2021
-
-
Paul E. McKenney authored
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 <paulmck@kernel.org>
-
Manfred Spraul authored
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 <manfred@colorfullife.com> Signed-off-by:
-
Paul E. McKenney authored
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:
-
- Jul 20, 2021
-
-
Paul E. McKenney authored
The current definition of read_foo_diagnostic() in the "Lock Protection With Lockless Diagnostic Access" section returns a value, which could be use for any purpose. This could mislead people into incorrectly using data_race() in cases where READ_ONCE() is required. This commit therefore makes read_foo_diagnostic() simply print the value read. Reported-by:
-
- May 10, 2021
-
-
Björn Töpel authored
A misspelled git-grep regex revealed that smp_mb__after_spinlock() was misspelled in explanation.txt. This commit adds the missing "_". Fixes: 1c27b644 ("Automate memory-barriers.txt; provide Linux-kernel memory model") [ paulmck: Apply Alan Stern commit-log feedback. ] Signed-off-by:
Björn Töpel <bjorn.topel@intel.com> Signed-off-by:
-
- Apr 06, 2021
-
-
Mauro Carvalho Chehab authored
Changeset b00aedf9 ("doc: Convert to rcu_dereference.txt to rcu_dereference.rst") renamed: Documentation/RCU/rcu_dereference.txt to: Documentation/RCU/rcu_dereference.rst. Update its cross-reference accordingly. Fixes: b00aedf9 ("doc: Convert to rcu_dereference.txt to rcu_dereference.rst") Signed-off-by:
Mauro Carvalho Chehab <mchehab+huawei@kernel.org>
-
- Mar 15, 2021
-
-
Paul E. McKenney authored
This commit adapts the "Concurrency bugs should fear the big bad data-race detector (part 2)" LWN article (https://lwn.net/Articles/816854/ ) to kernel-documentation form. This allows more easily updating the material as needed. Suggested-by:
Thomas Gleixner <tglx@linutronix.de> [ paulmck: Apply Marco Elver feedback. ] [ paulmck: Update per Akira Yokosawa feedback. ] Reviewed-by:
Marco Elver <elver@google.com> Signed-off-by:
-
- Mar 08, 2021
-
-
Akira Yokosawa authored
atomic_ops.rst was removed by commit f0400a77 ("atomic: Delete obsolete documentation"). Remove the broken link in tools/memory-model/Documentation/simple.txt. Cc: Peter Zijlstra <peterz@infradead.org> Signed-off-by:
Akira Yokosawa <akiyks@gmail.com> Signed-off-by:
-
Mauro Carvalho Chehab authored
Changeset b00aedf9 ("doc: Convert to rcu_dereference.txt to rcu_dereference.rst") renamed: Documentation/RCU/rcu_dereference.txt to: Documentation/RCU/rcu_dereference.rst. Update its cross-reference accordingly. Signed-off-by:
-
- Jan 04, 2021
-
-
Akira Yokosawa authored
klitmus7 of herdtools7 7.48 or earlier depends on ACCESS_ONCE(), which was removed in Linux v4.15. Fix the obvious typo in the table. Fixes: d075a78a ("tools/memory-model/README: Expand dependency of klitmus7") Signed-off-by:
-
Akira Yokosawa authored
This is a revert of commit 1947bfcf ("tools/memory-model: Add types to litmus tests") with conflict resolutions. klitmus7 [1] is aware of default types of "int" and "int*". It accepts litmus tests for herd7 without extra type info unless non-"int" variables are referenced by an "exists", "locations", or "filter" directive. [1]: Tested with klitmus7 versions 7.49 or later. Suggested-by:
-
Paul E. McKenney authored
This commit explicitly makes the connection between acquire loads and the reads-from relation. It also adds an entry for happens-before, and refers to the corresponding section of explanation.txt. Reported-by:
Boqun Feng <boqun.feng@gmail.com> Signed-off-by:
-
- Nov 07, 2020
-
-
Paul E. McKenney authored
This commit adds comments that label the MP tests' producer and consumer processes, and also that label the "exists" clause as the bad outcome. Reported-by:
Johannes Weiner <hannes@cmpxchg.org> Signed-off-by:
-
Paul E. McKenney authored
The use of "x" and "y" for message-passing tests is fine for people familiar with memory models and litmus-test nomenclature, but is a bit obtuse for others. This commit therefore substitutes "buf" for "x" and "flag" for "y" for the MP tests. There are a few special-case MP tests that use locks and these are unchanged. There is another MP test that uses pointers, and this is changed to name the pointer "p". Reported-by:
-
Paul E. McKenney authored
This commit adds type information for global variables in the litmus tests in order to allow easier use with klitmus7. Signed-off-by: -
Paul E. McKenney authored
[ paulmck: Apply Alan Stern feedback. ] Signed-off-by: -
Paul E. McKenney authored
The Linux kernel has a number of categories of ordering primitives, which are recorded in the LKMM implementation and hinted at by cheatsheet.txt. But there is no overview of these categories, and such an overview is needed in order to understand multithreaded LKMM litmus tests. This commit therefore adds an ordering.txt as well as extracting a control-dependencies.txt from memory-barriers.txt. It also updates the README file. [ paulmck: Apply Akira Yokosawa file-placement feedback. ] [ paulmck: Apply Alan Stern feedback. ] [ paulmck: Apply self-review feedback. ] Signed-off-by:
-
- Oct 26, 2020
-
-
Paul E. McKenney authored
This commit moves the descriptions of the files residing in tools/memory-model/Documentation to a README file in that directory, leaving behind the description of tools/memory-model/Documentation/README itself. After this change, tools/memory-model/Documentation/README provides a guide to the files in the tools/memory-model/Documentation directory, guiding people with different skills and needs to the most appropriate starting point. Signed-off-by: -
Alan Stern authored
Add a small section to the litmus-tests.txt documentation file for the Linux Kernel Memory Model explaining that the memory model often fails to recognize certain control dependencies. Suggested-by:
Alan Stern <stern@rowland.harvard.edu> Reviewed-by:
Joel Fernandes (Google) <joel@joelfernandes.org> Signed-off-by:
-
- Sep 04, 2020
-
-
Paul E. McKenney authored
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:
-
- Sep 03, 2020
-
-
Paul E. McKenney authored
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 <dchinner@redhat.com> Signed-off-by:
-
Paul E. McKenney authored
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 <david@fromorbit.com> Acked-by:
Peter Zijlstra (Intel) <peterz@infradead.org> Signed-off-by:
-
Paul E. McKenney authored
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: -
Alexander A. Klimov authored
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 <grandmaster@al2klimov.de> Signed-off-by:
-
- Jul 21, 2020
-
-
Will Deacon authored
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:
Will Deacon <will@kernel.org>
-
- Jun 29, 2020
-
-
Akira Yokosawa authored
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 <parri.andrea@gmail.com> Signed-off-by:
-
Akira Yokosawa authored
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]: b899a850 ("compiler.h: Remove ACCESS_ONCE()") [2]: 0bb95f80 ("Makefile: Globally enable VLA warning") [3]: d56c0d45 ("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:
-
Akira Yokosawa authored
The name of litmus test doesn't match the one described below. Fix the name of litmus test. Acked-by:
-
Boqun Feng authored
According to Luc, atomic_add_unless() is directly provided by herd7, therefore it can be used in litmus tests. So change the limitation section in README to unlimit the use of atomic_add_unless(). Cc: Luc Maranget <luc.maranget@inria.fr> Acked-by:
-
Marco Elver authored
The definition of "conflict" should not include the type of access nor whether the accesses are concurrent or not, which this patch addresses. The definition of "data race" remains unchanged. The definition of "conflict" as we know it and is cited by various papers on memory consistency models appeared in [1]: "Two accesses to the same variable conflict if at least one is a write; two operations conflict if they execute conflicting accesses." The LKMM as well as the C11 memory model are adaptations of data-race-free, which are based on the work in [2]. Necessarily, we need both conflicting data operations (plain) and synchronization operations (marked). For example, C11's definition is based on [3], which defines a "data race" as: "Two memory operations conflict if they access the same memory location, and at least one of them is a store, atomic store, or atomic read-modify-write operation. In a sequentially consistent execution, two memory operations from different threads form a type 1 data race if they conflict, at least one of them is a data operation, and they are adjacent in <T (i.e., they may be executed concurrently)." [1] D. Shasha, M. Snir, "Efficient and Correct Execution of Parallel Programs that Share Memory", 1988. URL: http://snir.cs.illinois.edu/listed/J21.pdf [2] S. Adve, "Designing Memory Consistency Models for Shared-Memory Multiprocessors", 1993. URL: http://sadve.cs.illinois.edu/Publications/thesis.pdf [3] H.-J. Boehm, S. Adve, "Foundations of the C++ Concurrency Memory Model", 2008. URL: https://www.hpl.hp.com/techreports/2008/HPL-2008-56.pdf Signed-off-by: -
Paul E. McKenney authored
This commit updates the list of LKMM-related publications in Documentation/references.txt. Signed-off-by:
-
- Mar 25, 2020
-
-
Masahiro Yamada authored
Add SPDX License Identifier to all .gitignore files. Signed-off-by:
Masahiro Yamada <masahiroy@kernel.org> Signed-off-by:
Greg Kroah-Hartman <gregkh@linuxfoundation.org>
-
- Oct 05, 2019
-
-
Alan Stern authored
This patch updates the Linux Kernel Memory Model's explanation.txt file by adding a section devoted to the model's handling of plain accesses and data-race detection. Signed-off-by:
-
Alan Stern authored
This patch updates the Linux Kernel Memory Model's explanation.txt file to incorporate the introduction of the rcu-order relation and the redefinition of rcu-fence made by commit 15aa25cb ("tools/memory-model: Change definition of rcu-fence"). Signed-off-by:
-
Alan Stern authored
This patch fixes a few minor typos and improves word usage in a few places in the Linux Kernel Memory Model's explanation.txt file. Signed-off-by:
-
Alan Stern authored
Currently the Linux Kernel Memory Model gives an incorrect response for the following litmus test: C plain-WWC {} P0(int *x) { WRITE_ONCE(*x, 2); } P1(int *x, int *y) { int r1; int r2; int r3; r1 = READ_ONCE(*x); if (r1 == 2) { smp_rmb(); r2 = *x; } smp_rmb(); r3 = READ_ONCE(*x); WRITE_ONCE(*y, r3 - 1); } P2(int *x, int *y) { int r4; r4 = READ_ONCE(*y); if (r4 > 0) WRITE_ONCE(*x, 1); } exists (x=2 /\ 1:r2=2 /\ 2:r4=1) The memory model says that the plain read of *x in P1 races with the WRITE_ONCE(*x) in P2. The problem is that we have a write W and a read R related by neither fre or rfe, but rather W ->coe W' ->rfe R, where W' is an intermediate write (the WRITE_ONCE() in P0). In this situation there is no particular ordering between W and R, so either a wr-vis link from W to R or an rw-xbstar link from R to W would prove that the accesses aren't concurrent. But the LKMM only looks for a wr-vis link, which is equivalent to assuming that W must execute before R. This is not necessarily true on non-multicopy-atomic systems, as the WWC pattern demonstrates. This patch changes the LKMM to accept either a wr-vis or a reverse rw-xbstar link as a proof of non-concurrency. Signed-off-by:
-
- Aug 09, 2019
-
-
Andrea Parri authored
The formal memory consistency model has added support for plain accesses (and data races). While updating the informal documentation to describe this addition to the model is highly desirable and important future work, update the informal documentation to at least acknowledge such addition. Signed-off-by:
Andrea Parri <andrea.parri@amarulasolutions.com> Cc: Will Deacon <will.deacon@arm.com> Cc: Peter Zijlstra <peterz@infradead.org> Cc: Boqun Feng <boqun.feng@gmail.com> Cc: Nicholas Piggin <npiggin@gmail.com> Cc: David Howells <dhowells@redhat.com> Cc: Jade Alglave <j.alglave@ucl.ac.uk> Cc: Luc Maranget <luc.maranget@inria.fr> Cc: "Paul E. McKenney" <paulmck@linux.ibm.com> Cc: Akira Yokosawa <akiyks@gmail.com> Cc: Daniel Lustig <dlustig@nvidia.com> Signed-off-by:
Paul E. McKenney <paulmck@linux.ibm.com> Acked-by:
-
Joel Fernandes (Google) authored
To reduce ambiguity in the more exotic ->prop ordering example, this commit uses the term cumul-fence instead of the term fence for the two fences, so that the implict ->rfe on loads/stores to Y are covered by the description. Link: https://lore.kernel.org/lkml/20190729121745.GA140682@google.com Suggested-by:
-
- Aug 01, 2019
-
-
Paul E. McKenney authored
This commit simplifies life a bit by making all of the scripts in tools/memory-model/scripts be executable. Signed-off-by:
-
- Jun 24, 2019
-
-
Alan Stern authored
Herbert Xu recently reported a problem concerning RCU and compiler barriers. In the course of discussing the problem, he put forth a litmus test which illustrated a serious defect in the Linux Kernel Memory Model's data-race-detection code [1]. The defect was that the LKMM assumed visibility and executes-before ordering of plain accesses had to be mediated by marked accesses. In Herbert's litmus test this wasn't so, and the LKMM claimed the litmus test was allowed and contained a data race although neither is true. In fact, plain accesses can be ordered by fences even in the absence of marked accesses. In most cases this doesn't matter, because most fences only order accesses within a single thread. But the rcu-fence relation is different; it can order (and induce visibility between) accesses in different threads -- events which otherwise might be concurrent. This makes it relevant to data-race detection. This patch makes two changes to the memory model to incorporate the new insight: If a store is separated by a fence from another access, the store is necessarily visible to the other access (as reflected in the ww-vis and wr-vis relations). Similarly, if a load is separated by a fence from another access then the load necessarily executes before the other access (as reflected in the rw-xbstar relation). If a store is separated by a strong fence from a marked access then it is necessarily visible to any access that executes after the marked access (as reflected in the ww-vis and wr-vis relations). With these changes, the LKMM gives the desired result for Herbert's litmus test and other related ones [2]. [1] https://lore.kernel.org/lkml/Pine.LNX.4.44L0.1906041026570.1731-100000@iolanthe.rowland.org/ [2] https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-1.litmus https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-2.litmus https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-3.litmus https://github.com/paulmckrcu/litmus/blob/master/manual/plain/C-S-rcunoderef-4.litmus https://github.com/paulmckrcu/litmus/blob/master/manual/plain/strong-vis.litmus Reported-by:
Herbert Xu <herbert@gondor.apana.org.au> Signed-off-by:
-
