From 38908de90a8c24c949505958f1d09812bb3b64aa Mon Sep 17 00:00:00 2001 From: "Paul E. McKenney" Date: Wed, 22 Jan 2020 13:38:57 -0800 Subject: tools/memory-model: Add recent references This commit updates the list of LKMM-related publications in Documentation/references.txt. Signed-off-by: Paul E. McKenney Acked-by: Andrea Parri --- tools/memory-model/Documentation/references.txt | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) (limited to 'tools/memory-model') diff --git a/tools/memory-model/Documentation/references.txt b/tools/memory-model/Documentation/references.txt index b177f3e4a614..ecbbaa5396d4 100644 --- a/tools/memory-model/Documentation/references.txt +++ b/tools/memory-model/Documentation/references.txt @@ -73,6 +73,18 @@ o Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Linux-kernel memory model ========================= +o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel + Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas + Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra. + 2019. "Calibrating your fear of big bad optimizing compilers" + Linux Weekly News. https://lwn.net/Articles/799218/ + +o Jade Alglave, Will Deacon, Boqun Feng, David Howells, Daniel + Lustig, Luc Maranget, Paul E. McKenney, Andrea Parri, Nicholas + Piggin, Alan Stern, Akira Yokosawa, and Peter Zijlstra. + 2019. "Who's afraid of a big bad optimizing compiler?" + Linux Weekly News. https://lwn.net/Articles/793253/ + o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan Stern. 2018. "Frightening small children and disconcerting grown-ups: Concurrency in the Linux kernel". In Proceedings of @@ -88,6 +100,11 @@ o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and Alan Stern. 2017. "A formal kernel memory-ordering model (part 2)" Linux Weekly News. https://lwn.net/Articles/720550/ +o Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, and + Alan Stern. 2017-2019. "A Formal Model of Linux-Kernel Memory + Ordering" (backup material for the LWN articles) + https://mirrors.edge.kernel.org/pub/linux/kernel/people/paulmck/LWNLinuxMM/ + Memory-model tooling ==================== @@ -110,5 +127,5 @@ Memory-model comparisons ======================== o Paul E. McKenney, Ulrich Weigand, Andrea Parri, and Boqun - Feng. 2016. "Linux-Kernel Memory Model". (6 June 2016). - http://open-std.org/JTC1/SC22/WG21/docs/papers/2016/p0124r2.html. + Feng. 2018. "Linux-Kernel Memory Model". (27 September 2018). + http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0124r6.html. -- cgit v1.2.3 From c1b14609013a6b4c4b2d73583bde645540ebd9b7 Mon Sep 17 00:00:00 2001 From: Marco Elver Date: Mon, 2 Mar 2020 18:21:01 +0100 Subject: tools/memory-model: Fix "conflict" definition 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 Co-developed-by: Alan Stern Signed-off-by: Alan Stern Acked-by: Andrea Parri Signed-off-by: Paul E. McKenney --- tools/memory-model/Documentation/explanation.txt | 83 +++++++++++++----------- 1 file changed, 45 insertions(+), 38 deletions(-) (limited to 'tools/memory-model') diff --git a/tools/memory-model/Documentation/explanation.txt b/tools/memory-model/Documentation/explanation.txt index e91a2eb19592..993f800659c6 100644 --- a/tools/memory-model/Documentation/explanation.txt +++ b/tools/memory-model/Documentation/explanation.txt @@ -1987,28 +1987,36 @@ outcome undefined. In technical terms, the compiler is allowed to assume that when the program executes, there will not be any data races. A "data race" -occurs when two conflicting memory accesses execute concurrently; -two memory accesses "conflict" if: +occurs when there are two memory accesses such that: - they access the same location, +1. they access the same location, - they occur on different CPUs (or in different threads on the - same CPU), +2. at least one of them is a store, - at least one of them is a plain access, +3. at least one of them is plain, - and at least one of them is a store. +4. they occur on different CPUs (or in different threads on the + same CPU), and -The LKMM tries to determine whether a program contains two conflicting -accesses which may execute concurrently; if it does then the LKMM says -there is a potential data race and makes no predictions about the -program's outcome. +5. they execute concurrently. -Determining whether two accesses conflict is easy; you can see that -all the concepts involved in the definition above are already part of -the memory model. The hard part is telling whether they may execute -concurrently. The LKMM takes a conservative attitude, assuming that -accesses may be concurrent unless it can prove they cannot. +In the literature, two accesses are said to "conflict" if they satisfy +1 and 2 above. We'll go a little farther and say that two accesses +are "race candidates" if they satisfy 1 - 4. Thus, whether or not two +race candidates actually do race in a given execution depends on +whether they are concurrent. + +The LKMM tries to determine whether a program contains race candidates +which may execute concurrently; if it does then the LKMM says there is +a potential data race and makes no predictions about the program's +outcome. + +Determining whether two accesses are race candidates is easy; you can +see that all the concepts involved in the definition above are already +part of the memory model. The hard part is telling whether they may +execute concurrently. The LKMM takes a conservative attitude, +assuming that accesses may be concurrent unless it can prove they +are not. If two memory accesses aren't concurrent then one must execute before the other. Therefore the LKMM decides two accesses aren't concurrent @@ -2171,8 +2179,8 @@ again, now using plain accesses for buf: } This program does not contain a data race. Although the U and V -accesses conflict, the LKMM can prove they are not concurrent as -follows: +accesses are race candidates, the LKMM can prove they are not +concurrent as follows: The smp_wmb() fence in P0 is both a compiler barrier and a cumul-fence. It guarantees that no matter what hash of @@ -2326,12 +2334,11 @@ could now perform the load of x before the load of ptr (there might be a control dependency but no address dependency at the machine level). Finally, it turns out there is a situation in which a plain write does -not need to be w-post-bounded: when it is separated from the -conflicting access by a fence. At first glance this may seem -impossible. After all, to be conflicting the second access has to be -on a different CPU from the first, and fences don't link events on -different CPUs. Well, normal fences don't -- but rcu-fence can! -Here's an example: +not need to be w-post-bounded: when it is separated from the other +race-candidate access by a fence. At first glance this may seem +impossible. After all, to be race candidates the two accesses must +be on different CPUs, and fences don't link events on different CPUs. +Well, normal fences don't -- but rcu-fence can! Here's an example: int x, y; @@ -2367,7 +2374,7 @@ concurrent and there is no race, even though P1's plain store to y isn't w-post-bounded by any marked accesses. Putting all this material together yields the following picture. For -two conflicting stores W and W', where W ->co W', the LKMM says the +race-candidate stores W and W', where W ->co W', the LKMM says the stores don't race if W can be linked to W' by a w-post-bounded ; vis ; w-pre-bounded @@ -2380,8 +2387,8 @@ sequence, and if W' is plain then they also have to be linked by a w-post-bounded ; vis ; r-pre-bounded -sequence. For a conflicting load R and store W, the LKMM says the two -accesses don't race if R can be linked to W by an +sequence. For race-candidate load R and store W, the LKMM says the +two accesses don't race if R can be linked to W by an r-post-bounded ; xb* ; w-pre-bounded @@ -2413,20 +2420,20 @@ is, the rules governing the memory subsystem's choice of a store to satisfy a load request and its determination of where a store will fall in the coherence order): - If R and W conflict and it is possible to link R to W by one - of the xb* sequences listed above, then W ->rfe R is not - allowed (i.e., a load cannot read from a store that it + If R and W are race candidates and it is possible to link R to + W by one of the xb* sequences listed above, then W ->rfe R is + not allowed (i.e., a load cannot read from a store that it executes before, even if one or both is plain). - If W and R conflict and it is possible to link W to R by one - of the vis sequences listed above, then R ->fre W is not - allowed (i.e., if a store is visible to a load then the load - must read from that store or one coherence-after it). + If W and R are race candidates and it is possible to link W to + R by one of the vis sequences listed above, then R ->fre W is + not allowed (i.e., if a store is visible to a load then the + load must read from that store or one coherence-after it). - If W and W' conflict and it is possible to link W to W' by one - of the vis sequences listed above, then W' ->co W is not - allowed (i.e., if one store is visible to a second then the - second must come after the first in the coherence order). + If W and W' are race candidates and it is possible to link W + to W' by one of the vis sequences listed above, then W' ->co W + is not allowed (i.e., if one store is visible to a second then + the second must come after the first in the coherence order). This is the extent to which the LKMM deals with plain accesses. Perhaps it could say more (for example, plain accesses might -- cgit v1.2.3 From 4a9cc65f7a715ba1f4f58529f7bf6f1548d8701f Mon Sep 17 00:00:00 2001 From: Boqun Feng Date: Thu, 26 Mar 2020 10:40:19 +0800 Subject: tools/memory-model: Add an exception for limitations on _unless() family 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 Acked-by: Andrea Parri Reviewed-by: Joel Fernandes (Google) Signed-off-by: Boqun Feng Signed-off-by: Paul E. McKenney --- tools/memory-model/README | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'tools/memory-model') diff --git a/tools/memory-model/README b/tools/memory-model/README index fc07b52f2028..b9c562e92981 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -207,11 +207,15 @@ The Linux-kernel memory model (LKMM) has the following limitations: case as a store release. b. The "unless" RMW operations are not currently modeled: - atomic_long_add_unless(), atomic_add_unless(), - atomic_inc_unless_negative(), and - atomic_dec_unless_positive(). These can be emulated + atomic_long_add_unless(), atomic_inc_unless_negative(), + and atomic_dec_unless_positive(). These can be emulated in litmus tests, for example, by using atomic_cmpxchg(). + One exception of this limitation is atomic_add_unless(), + which is provided directly by herd7 (so no corresponding + definition in linux-kernel.def). atomic_add_unless() is + modeled by herd7 therefore it can be used in litmus tests. + c. The call_rcu() function is not modeled. It can be emulated in litmus tests by adding another process that invokes synchronize_rcu() and the body of the callback -- cgit v1.2.3 From 9725dd55512772422e195cf0cfbca1eda6778358 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Sun, 10 May 2020 13:37:14 +0900 Subject: tools/memory-model: Fix reference to litmus test in recipes.txt The name of litmus test doesn't match the one described below. Fix the name of litmus test. Acked-by: Andrea Parri Acked-by: Joel Fernandes (Google) Signed-off-by: Akira Yokosawa Signed-off-by: Paul E. McKenney --- tools/memory-model/Documentation/recipes.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools/memory-model') diff --git a/tools/memory-model/Documentation/recipes.txt b/tools/memory-model/Documentation/recipes.txt index 7fe8d7aa3029..63c4adfed884 100644 --- a/tools/memory-model/Documentation/recipes.txt +++ b/tools/memory-model/Documentation/recipes.txt @@ -126,7 +126,7 @@ However, it is not necessarily the case that accesses ordered by locking will be seen as ordered by CPUs not holding that lock. Consider this example: - /* See Z6.0+pooncerelease+poacquirerelease+fencembonceonce.litmus. */ + /* See Z6.0+pooncelock+pooncelock+pombonce.litmus. */ void CPU0(void) { spin_lock(&mylock); -- cgit v1.2.3 From d075a78a5ab19389d5600923d6ad5391d7cd1be8 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Sun, 31 May 2020 20:04:32 +0900 Subject: tools/memory-model/README: Expand dependency of klitmus7 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 --- tools/memory-model/README | 30 ++++++++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) (limited to 'tools/memory-model') diff --git a/tools/memory-model/README b/tools/memory-model/README index b9c562e92981..90af203c3cf1 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -28,8 +28,34 @@ downloaded separately: See "herdtools7/INSTALL.md" for installation instructions. Note that although these tools usually provide backwards compatibility, -this is not absolutely guaranteed. Therefore, if a later version does -not work, please try using the exact version called out above. +this is not absolutely guaranteed. + +For example, a future version of herd7 might not work with the model +in this release. A compatible model will likely be made available in +a later release of Linux kernel. + +If you absolutely need to run the model in this particular release, +please try using the exact version called out above. + +klitmus7 is independent of the model provided here. It has its own +dependency on a target kernel release where converted code is built +and executed. Any change in kernel APIs essential to klitmus7 will +necessitate an upgrade of klitmus7. + +If you find any compatibility issues in klitmus7, please inform the +memory model maintainers. + +klitmus7 Compatibility Table +---------------------------- + + ============ ========== + target Linux herdtools7 + ------------ ---------- + -- 4.18 7.48 -- + 4.15 -- 4.19 7.49 -- + 4.20 -- 5.5 7.54 -- + 5.6 -- HEAD + ============ ========== ================== -- cgit v1.2.3 From 2bfa5c62debe43e3779e03bfc66b75ab72098db1 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Wed, 24 Jun 2020 06:56:43 +0900 Subject: tools/memory-model/README: Mention herdtools7 7.56 in compatibility table 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 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tools/memory-model') diff --git a/tools/memory-model/README b/tools/memory-model/README index 90af203c3cf1..ecb7385376bf 100644 --- a/tools/memory-model/README +++ b/tools/memory-model/README @@ -54,7 +54,7 @@ klitmus7 Compatibility Table -- 4.18 7.48 -- 4.15 -- 4.19 7.49 -- 4.20 -- 5.5 7.54 -- - 5.6 -- HEAD + 5.6 -- 7.56 -- ============ ========== -- cgit v1.2.3