* [PATCH memory-model 0/7] LKMM updates for v6.12
@ 2024-08-02 0:22 Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 1/7] tools/memory-model: Add atomic_and()/or()/xor() and add_negative Paul E. McKenney
` (6 more replies)
0 siblings, 7 replies; 11+ messages in thread
From: Paul E. McKenney @ 2024-08-02 0:22 UTC (permalink / raw)
To: linux-kernel, linux-arch, lkmm, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks
Hello!
This series adds a few atomic operations, some documentation, and updates
the MAINTAINERS file.
1. Add atomic_and()/or()/xor() and add_negative, courtesy of
Puranjay Mohan.
2. Add atomic_andnot() with its variants, courtesy of Puranjay Mohan.
3. Document herd7 (abstract) representation, courtesy of Andrea
Parri.
4. Add locking.txt and glossary.txt to README, courtesy of Akira
Yokosawa.
5. simple.txt: Fix stale reference to recipes-pairs.txt, courtesy
of Akira Yokosawa.
6. docs/memory-barriers.txt: Remove left-over references to "CACHE
COHERENCY", courtesy of Akira Yokosawa.
7. MAINTAINERS: Add the dedicated maillist info for LKMM, courtesy
of Boqun Feng.
Thanx, Paul
------------------------------------------------------------------------
b/Documentation/memory-barriers.txt | 3
b/MAINTAINERS | 1
b/tools/memory-model/Documentation/README | 7
b/tools/memory-model/Documentation/herd-representation.txt | 110 +++++++++++++
b/tools/memory-model/Documentation/simple.txt | 2
b/tools/memory-model/linux-kernel.def | 21 ++
tools/memory-model/Documentation/README | 17 ++
tools/memory-model/linux-kernel.def | 6
8 files changed, 162 insertions(+), 5 deletions(-)
^ permalink raw reply [flat|nested] 11+ messages in thread
* [PATCH memory-model 1/7] tools/memory-model: Add atomic_and()/or()/xor() and add_negative
2024-08-02 0:22 [PATCH memory-model 0/7] LKMM updates for v6.12 Paul E. McKenney
@ 2024-08-02 0:22 ` Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 2/7] tools/memory-model: Add atomic_andnot() with its variants Paul E. McKenney
` (5 subsequent siblings)
6 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2024-08-02 0:22 UTC (permalink / raw)
To: linux-kernel, linux-arch, lkmm, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Puranjay Mohan,
Paul E . McKenney, Daniel Lustig, Joel Fernandes
From: Puranjay Mohan <puranjay@kernel.org>
Pull-849[1] added the support of '&', '|', and '^' to the herd7 tool's
atomics operations.
Use these in linux-kernel.def to implement atomic_and()/or()/xor() with
all their ordering variants.
atomic_add_negative() is already available so add its acquire, release,
and relaxed ordering variants.
[1] https://github.com/herd/herdtools7/pull/849
Signed-off-by: Puranjay Mohan <puranjay@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will@kernel.org>
Cc: Peter Zijlstra <peterz@infradead.org>
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: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: Joel Fernandes <joel@joelfernandes.org>
Cc: <linux-arch@vger.kernel.org>
---
tools/memory-model/linux-kernel.def | 21 +++++++++++++++++++++
1 file changed, 21 insertions(+)
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index 88a39601f5256..d1f11930ec512 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -65,6 +65,9 @@ atomic_set_release(X,V) { smp_store_release(X,V); }
atomic_add(V,X) { __atomic_op(X,+,V); }
atomic_sub(V,X) { __atomic_op(X,-,V); }
+atomic_and(V,X) { __atomic_op(X,&,V); }
+atomic_or(V,X) { __atomic_op(X,|,V); }
+atomic_xor(V,X) { __atomic_op(X,^,V); }
atomic_inc(X) { __atomic_op(X,+,1); }
atomic_dec(X) { __atomic_op(X,-,1); }
@@ -77,6 +80,21 @@ atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{once}(X,+,V)
atomic_fetch_add_acquire(V,X) __atomic_fetch_op{acquire}(X,+,V)
atomic_fetch_add_release(V,X) __atomic_fetch_op{release}(X,+,V)
+atomic_fetch_and(V,X) __atomic_fetch_op{mb}(X,&,V)
+atomic_fetch_and_relaxed(V,X) __atomic_fetch_op{once}(X,&,V)
+atomic_fetch_and_acquire(V,X) __atomic_fetch_op{acquire}(X,&,V)
+atomic_fetch_and_release(V,X) __atomic_fetch_op{release}(X,&,V)
+
+atomic_fetch_or(V,X) __atomic_fetch_op{mb}(X,|,V)
+atomic_fetch_or_relaxed(V,X) __atomic_fetch_op{once}(X,|,V)
+atomic_fetch_or_acquire(V,X) __atomic_fetch_op{acquire}(X,|,V)
+atomic_fetch_or_release(V,X) __atomic_fetch_op{release}(X,|,V)
+
+atomic_fetch_xor(V,X) __atomic_fetch_op{mb}(X,^,V)
+atomic_fetch_xor_relaxed(V,X) __atomic_fetch_op{once}(X,^,V)
+atomic_fetch_xor_acquire(V,X) __atomic_fetch_op{acquire}(X,^,V)
+atomic_fetch_xor_release(V,X) __atomic_fetch_op{release}(X,^,V)
+
atomic_inc_return(X) __atomic_op_return{mb}(X,+,1)
atomic_inc_return_relaxed(X) __atomic_op_return{once}(X,+,1)
atomic_inc_return_acquire(X) __atomic_op_return{acquire}(X,+,1)
@@ -117,3 +135,6 @@ atomic_sub_and_test(V,X) __atomic_op_return{mb}(X,-,V) == 0
atomic_dec_and_test(X) __atomic_op_return{mb}(X,-,1) == 0
atomic_inc_and_test(X) __atomic_op_return{mb}(X,+,1) == 0
atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0
+atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0
+atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0
+atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0
--
2.40.1
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH memory-model 2/7] tools/memory-model: Add atomic_andnot() with its variants
2024-08-02 0:22 [PATCH memory-model 0/7] LKMM updates for v6.12 Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 1/7] tools/memory-model: Add atomic_and()/or()/xor() and add_negative Paul E. McKenney
@ 2024-08-02 0:22 ` Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 3/7] tools/memory-model: Document herd7 (abstract) representation Paul E. McKenney
` (4 subsequent siblings)
6 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2024-08-02 0:22 UTC (permalink / raw)
To: linux-kernel, linux-arch, lkmm, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Puranjay Mohan,
Paul E . McKenney, Daniel Lustig, Joel Fernandes
From: Puranjay Mohan <puranjay@kernel.org>
Pull-855[1] added the support of atomic_andnot() to the herd tool. Use
this to add the implementation in the LKMM. All of the ordering variants
are also added.
Here is a small litmus-test that uses this operation:
C andnot
{
atomic_t u = ATOMIC_INIT(7);
}
P0(atomic_t *u)
{
r0 = atomic_fetch_andnot(3, u);
r1 = READ_ONCE(*u);
}
exists (0:r0=7 /\ 0:r1=4)
Test andnot Allowed
States 1
0:r0=7; 0:r1=4;
Ok
Witnesses
Positive: 1 Negative: 0
Condition exists (0:r0=7 /\ 0:r1=4)
Observation andnot Always 1 0
Time andnot 0.00
Hash=78f011a0b5a0c65fa1cf106fcd62c845
[1] https://github.com/herd/herdtools7/pull/855
Signed-off-by: Puranjay Mohan <puranjay@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will@kernel.org>
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: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: Joel Fernandes <joel@joelfernandes.org>
Cc: <linux-arch@vger.kernel.org>
---
tools/memory-model/linux-kernel.def | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index d1f11930ec512..a12b96c547b7a 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -70,6 +70,7 @@ atomic_or(V,X) { __atomic_op(X,|,V); }
atomic_xor(V,X) { __atomic_op(X,^,V); }
atomic_inc(X) { __atomic_op(X,+,1); }
atomic_dec(X) { __atomic_op(X,-,1); }
+atomic_andnot(V,X) { __atomic_op(X,&~,V); }
atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
@@ -138,3 +139,8 @@ atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0
atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0
atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0
atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0
+
+atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V)
+atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V)
+atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V)
+atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V)
--
2.40.1
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH memory-model 3/7] tools/memory-model: Document herd7 (abstract) representation
2024-08-02 0:22 [PATCH memory-model 0/7] LKMM updates for v6.12 Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 1/7] tools/memory-model: Add atomic_and()/or()/xor() and add_negative Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 2/7] tools/memory-model: Add atomic_andnot() with its variants Paul E. McKenney
@ 2024-08-02 0:22 ` Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 4/7] tools/memory-model: Add locking.txt and glossary.txt to README Paul E. McKenney
` (3 subsequent siblings)
6 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2024-08-02 0:22 UTC (permalink / raw)
To: linux-kernel, linux-arch, lkmm, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Hernan Ponce de Leon,
Paul E . McKenney
From: Andrea Parri <parri.andrea@gmail.com>
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 <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Andrea Parri <parri.andrea@gmail.com>
Reviewed-by: Boqun Feng <boqun.feng@gmail.com>
Reviewed-by: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
tools/memory-model/Documentation/README | 7 +-
.../Documentation/herd-representation.txt | 110 ++++++++++++++++++
2 files changed, 116 insertions(+), 1 deletion(-)
create mode 100644 tools/memory-model/Documentation/herd-representation.txt
diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README
index 304162743a5b8..44e7dae73b296 100644
--- a/tools/memory-model/Documentation/README
+++ b/tools/memory-model/Documentation/README
@@ -33,7 +33,8 @@ o You are familiar with Linux-kernel concurrency and the use of
o You are familiar with Linux-kernel concurrency and the use
of LKMM, and would like to learn about LKMM's requirements,
- rationale, and implementation: explanation.txt
+ rationale, and implementation: explanation.txt and
+ herd-representation.txt
o You are interested in the publications related to LKMM, including
hardware manuals, academic literature, standards-committee
@@ -61,6 +62,10 @@ control-dependencies.txt
explanation.txt
Detailed description of the memory model.
+herd-representation.txt
+ The (abstract) representation of the Linux-kernel concurrency
+ primitives in terms of events.
+
litmus-tests.txt
The format, features, capabilities, and limitations of the litmus
tests that LKMM can evaluate.
diff --git a/tools/memory-model/Documentation/herd-representation.txt b/tools/memory-model/Documentation/herd-representation.txt
new file mode 100644
index 0000000000000..ed988906f2b71
--- /dev/null
+++ b/tools/memory-model/Documentation/herd-representation.txt
@@ -0,0 +1,110 @@
+#
+# Legend:
+# R, a Load event
+# W, a Store event
+# F, a Fence event
+# LKR, a Lock-Read event
+# LKW, a Lock-Write event
+# UL, an Unlock event
+# LF, a Lock-Fail event
+# RL, a Read-Locked event
+# RU, a Read-Unlocked event
+# R*, a Load event included in RMW
+# W*, a Store event included in RMW
+# SRCU, a Sleepable-Read-Copy-Update event
+#
+# po, a Program-Order link
+# rmw, a Read-Modify-Write link - every rmw link is a po link
+#
+# By convention, a blank line in a cell means "same as the preceding line".
+#
+# Disclaimer. The table includes representations of "add" and "and" operations;
+# corresponding/identical representations of "sub", "inc", "dec" and "or", "xor",
+# "andnot" operations are omitted.
+#
+ ------------------------------------------------------------------------------
+ | C macro | Events |
+ ------------------------------------------------------------------------------
+ | Non-RMW ops | |
+ ------------------------------------------------------------------------------
+ | READ_ONCE | R[once] |
+ | atomic_read | |
+ | WRITE_ONCE | W[once] |
+ | atomic_set | |
+ | smp_load_acquire | R[acquire] |
+ | atomic_read_acquire | |
+ | smp_store_release | W[release] |
+ | atomic_set_release | |
+ | smp_store_mb | W[once] ->po F[mb] |
+ | smp_mb | F[mb] |
+ | smp_rmb | F[rmb] |
+ | smp_wmb | F[wmb] |
+ | smp_mb__before_atomic | F[before-atomic] |
+ | smp_mb__after_atomic | F[after-atomic] |
+ | spin_unlock | UL |
+ | spin_is_locked | On success: RL |
+ | | On failure: RU |
+ | smp_mb__after_spinlock | F[after-spinlock] |
+ | smp_mb__after_unlock_lock | F[after-unlock-lock] |
+ | rcu_read_lock | F[rcu-lock] |
+ | rcu_read_unlock | F[rcu-unlock] |
+ | synchronize_rcu | F[sync-rcu] |
+ | rcu_dereference | R[once] |
+ | rcu_assign_pointer | W[release] |
+ | srcu_read_lock | R[srcu-lock] |
+ | srcu_down_read | |
+ | srcu_read_unlock | W[srcu-unlock] |
+ | srcu_up_read | |
+ | synchronize_srcu | SRCU[sync-srcu] |
+ | smp_mb__after_srcu_read_unlock | F[after-srcu-read-unlock] |
+ ------------------------------------------------------------------------------
+ | RMW ops w/o return value | |
+ ------------------------------------------------------------------------------
+ | atomic_add | R*[noreturn] ->rmw W*[once] |
+ | atomic_and | |
+ | spin_lock | LKR ->po LKW |
+ ------------------------------------------------------------------------------
+ | RMW ops w/ return value | |
+ ------------------------------------------------------------------------------
+ | atomic_add_return | F[mb] ->po R*[once] |
+ | | ->rmw W*[once] ->po F[mb] |
+ | atomic_fetch_add | |
+ | atomic_fetch_and | |
+ | atomic_xchg | |
+ | xchg | |
+ | atomic_add_negative | |
+ | atomic_add_return_relaxed | R*[once] ->rmw W*[once] |
+ | atomic_fetch_add_relaxed | |
+ | atomic_fetch_and_relaxed | |
+ | atomic_xchg_relaxed | |
+ | xchg_relaxed | |
+ | atomic_add_negative_relaxed | |
+ | atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
+ | atomic_fetch_add_acquire | |
+ | atomic_fetch_and_acquire | |
+ | atomic_xchg_acquire | |
+ | xchg_acquire | |
+ | atomic_add_negative_acquire | |
+ | atomic_add_return_release | R*[once] ->rmw W*[release] |
+ | atomic_fetch_add_release | |
+ | atomic_fetch_and_release | |
+ | atomic_xchg_release | |
+ | xchg_release | |
+ | atomic_add_negative_release | |
+ ------------------------------------------------------------------------------
+ | Conditional RMW ops | |
+ ------------------------------------------------------------------------------
+ | atomic_cmpxchg | On success: F[mb] ->po R*[once] |
+ | | ->rmw W*[once] ->po F[mb] |
+ | | On failure: R*[once] |
+ | cmpxchg | |
+ | atomic_add_unless | |
+ | atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once] |
+ | | On failure: R*[once] |
+ | atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[once] |
+ | | On failure: R*[once] |
+ | atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release] |
+ | | On failure: R*[once] |
+ | spin_trylock | On success: LKR ->po LKW |
+ | | On failure: LF |
+ ------------------------------------------------------------------------------
--
2.40.1
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH memory-model 4/7] tools/memory-model: Add locking.txt and glossary.txt to README
2024-08-02 0:22 [PATCH memory-model 0/7] LKMM updates for v6.12 Paul E. McKenney
` (2 preceding siblings ...)
2024-08-02 0:22 ` [PATCH memory-model 3/7] tools/memory-model: Document herd7 (abstract) representation Paul E. McKenney
@ 2024-08-02 0:22 ` Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 5/7] tools/memory-model: simple.txt: Fix stale reference to recipes-pairs.txt Paul E. McKenney
` (2 subsequent siblings)
6 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2024-08-02 0:22 UTC (permalink / raw)
To: linux-kernel, linux-arch, lkmm, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Marco Elver, Paul E . McKenney
From: Akira Yokosawa <akiyks@gmail.com>
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 <akiyks@gmail.com>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Cc: Marco Elver <elver@google.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
tools/memory-model/Documentation/README | 17 +++++++++++++++++
1 file changed, 17 insertions(+)
diff --git a/tools/memory-model/Documentation/README b/tools/memory-model/Documentation/README
index 44e7dae73b296..9999c1effdb65 100644
--- a/tools/memory-model/Documentation/README
+++ b/tools/memory-model/Documentation/README
@@ -9,6 +9,8 @@ depending on what you know and what you would like to learn. Please note
that the documents later in this list assume that the reader understands
the material provided by documents earlier in this list.
+If LKMM-specific terms lost you, glossary.txt might help you.
+
o You are new to Linux-kernel concurrency: simple.txt
o You have some background in Linux-kernel concurrency, and would
@@ -21,6 +23,9 @@ o You are familiar with the Linux-kernel concurrency primitives
that you need, and just want to get started with LKMM litmus
tests: litmus-tests.txt
+o You would like to access lock-protected shared variables without
+ having their corresponding locks held: locking.txt
+
o You are familiar with Linux-kernel concurrency, and would
like a detailed intuitive understanding of LKMM, including
situations involving more than two threads: recipes.txt
@@ -28,6 +33,11 @@ o You are familiar with Linux-kernel concurrency, and would
o You would like a detailed understanding of what your compiler can
and cannot do to control dependencies: control-dependencies.txt
+o You would like to mark concurrent normal accesses to shared
+ variables so that intentional "racy" accesses can be properly
+ documented, especially when you are responding to complaints
+ from KCSAN: access-marking.txt
+
o You are familiar with Linux-kernel concurrency and the use of
LKMM, and would like a quick reference: cheatsheet.txt
@@ -62,6 +72,9 @@ control-dependencies.txt
explanation.txt
Detailed description of the memory model.
+glossary.txt
+ Brief definitions of LKMM-related terms.
+
herd-representation.txt
The (abstract) representation of the Linux-kernel concurrency
primitives in terms of events.
@@ -70,6 +83,10 @@ litmus-tests.txt
The format, features, capabilities, and limitations of the litmus
tests that LKMM can evaluate.
+locking.txt
+ Rules for accessing lock-protected shared variables outside of
+ their corresponding critical sections.
+
ordering.txt
Overview of the Linux kernel's low-level memory-ordering
primitives by category.
--
2.40.1
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH memory-model 5/7] tools/memory-model: simple.txt: Fix stale reference to recipes-pairs.txt
2024-08-02 0:22 [PATCH memory-model 0/7] LKMM updates for v6.12 Paul E. McKenney
` (3 preceding siblings ...)
2024-08-02 0:22 ` [PATCH memory-model 4/7] tools/memory-model: Add locking.txt and glossary.txt to README Paul E. McKenney
@ 2024-08-02 0:22 ` Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 6/7] docs/memory-barriers.txt: Remove left-over references to "CACHE COHERENCY" Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 7/7] MAINTAINERS: Add the dedicated maillist info for LKMM Paul E. McKenney
6 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2024-08-02 0:22 UTC (permalink / raw)
To: linux-kernel, linux-arch, lkmm, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E . McKenney
From: Akira Yokosawa <akiyks@gmail.com>
There has never been recipes-paris.txt at least since v5.11.
Fix the typo.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
tools/memory-model/Documentation/simple.txt | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tools/memory-model/Documentation/simple.txt b/tools/memory-model/Documentation/simple.txt
index 4c789ec8334fc..21f06c1d1b70d 100644
--- a/tools/memory-model/Documentation/simple.txt
+++ b/tools/memory-model/Documentation/simple.txt
@@ -266,5 +266,5 @@ More complex use cases
======================
If the alternatives above do not do what you need, please look at the
-recipes-pairs.txt file to peel off the next layer of the memory-ordering
+recipes.txt file to peel off the next layer of the memory-ordering
onion.
--
2.40.1
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH memory-model 6/7] docs/memory-barriers.txt: Remove left-over references to "CACHE COHERENCY"
2024-08-02 0:22 [PATCH memory-model 0/7] LKMM updates for v6.12 Paul E. McKenney
` (4 preceding siblings ...)
2024-08-02 0:22 ` [PATCH memory-model 5/7] tools/memory-model: simple.txt: Fix stale reference to recipes-pairs.txt Paul E. McKenney
@ 2024-08-02 0:22 ` Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 7/7] MAINTAINERS: Add the dedicated maillist info for LKMM Paul E. McKenney
6 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2024-08-02 0:22 UTC (permalink / raw)
To: linux-kernel, linux-arch, lkmm, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E . McKenney
From: Akira Yokosawa <akiyks@gmail.com>
Commit 8ca924aeb4f2 ("Documentation/barriers: Remove references to
[smp_]read_barrier_depends()") removed the entire section of "CACHE
COHERENCY", without getting rid of its traces.
Remove them.
Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
Cc: Will Deacon <will@kernel.org>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
---
Documentation/memory-barriers.txt | 3 ---
1 file changed, 3 deletions(-)
diff --git a/Documentation/memory-barriers.txt b/Documentation/memory-barriers.txt
index 4202174a6262c..93d58d9a428b8 100644
--- a/Documentation/memory-barriers.txt
+++ b/Documentation/memory-barriers.txt
@@ -88,7 +88,6 @@ CONTENTS
(*) The effects of the cpu cache.
- - Cache coherency.
- Cache coherency vs DMA.
- Cache coherency vs MMIO.
@@ -677,8 +676,6 @@ include/linux/rcupdate.h. This permits the current target of an RCU'd
pointer to be replaced with a new modified target, without the replacement
target appearing to be incompletely initialised.
-See also the subsection on "Cache Coherency" for a more thorough example.
-
CONTROL DEPENDENCIES
--------------------
--
2.40.1
^ permalink raw reply related [flat|nested] 11+ messages in thread
* [PATCH memory-model 7/7] MAINTAINERS: Add the dedicated maillist info for LKMM
2024-08-02 0:22 [PATCH memory-model 0/7] LKMM updates for v6.12 Paul E. McKenney
` (5 preceding siblings ...)
2024-08-02 0:22 ` [PATCH memory-model 6/7] docs/memory-barriers.txt: Remove left-over references to "CACHE COHERENCY" Paul E. McKenney
@ 2024-08-02 0:22 ` Paul E. McKenney
2024-08-02 9:46 ` Andrea Parri
6 siblings, 1 reply; 11+ messages in thread
From: Paul E. McKenney @ 2024-08-02 0:22 UTC (permalink / raw)
To: linux-kernel, linux-arch, lkmm, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Paul E . McKenney
From: Boqun Feng <boqun.feng@gmail.com>
A dedicated mail list has been created for Linux kernel memory model
discussion, which could help people more easily track memory model
related discussions. This could also help bring memory model discussions
to a broader audience. Therefore, add the list information to the LKMM
maintainers entry.
Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
---
MAINTAINERS | 1 +
1 file changed, 1 insertion(+)
diff --git a/MAINTAINERS b/MAINTAINERS
index 42decde383206..0a3a769148fd8 100644
--- a/MAINTAINERS
+++ b/MAINTAINERS
@@ -12993,6 +12993,7 @@ R: Daniel Lustig <dlustig@nvidia.com>
R: Joel Fernandes <joel@joelfernandes.org>
L: linux-kernel@vger.kernel.org
L: linux-arch@vger.kernel.org
+L: lkmm@lists.linux.dev
S: Supported
T: git git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu.git dev
F: Documentation/atomic_bitops.txt
--
2.40.1
^ permalink raw reply related [flat|nested] 11+ messages in thread
* Re: [PATCH memory-model 7/7] MAINTAINERS: Add the dedicated maillist info for LKMM
2024-08-02 0:22 ` [PATCH memory-model 7/7] MAINTAINERS: Add the dedicated maillist info for LKMM Paul E. McKenney
@ 2024-08-02 9:46 ` Andrea Parri
2024-08-02 17:47 ` Paul E. McKenney
0 siblings, 1 reply; 11+ messages in thread
From: Andrea Parri @ 2024-08-02 9:46 UTC (permalink / raw)
To: Paul E. McKenney
Cc: linux-kernel, linux-arch, lkmm, kernel-team, mingo, stern, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
On Thu, Aug 01, 2024 at 05:22:15PM -0700, Paul E. McKenney wrote:
> From: Boqun Feng <boqun.feng@gmail.com>
>
> A dedicated mail list has been created for Linux kernel memory model
> discussion, which could help people more easily track memory model
> related discussions. This could also help bring memory model discussions
> to a broader audience. Therefore, add the list information to the LKMM
> maintainers entry.
>
> Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Andrea
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: [PATCH memory-model 7/7] MAINTAINERS: Add the dedicated maillist info for LKMM
2024-08-02 9:46 ` Andrea Parri
@ 2024-08-02 17:47 ` Paul E. McKenney
0 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2024-08-02 17:47 UTC (permalink / raw)
To: Andrea Parri
Cc: linux-kernel, linux-arch, lkmm, kernel-team, mingo, stern, will,
peterz, boqun.feng, npiggin, dhowells, j.alglave, luc.maranget,
akiyks
On Fri, Aug 02, 2024 at 11:46:20AM +0200, Andrea Parri wrote:
> On Thu, Aug 01, 2024 at 05:22:15PM -0700, Paul E. McKenney wrote:
> > From: Boqun Feng <boqun.feng@gmail.com>
> >
> > A dedicated mail list has been created for Linux kernel memory model
> > discussion, which could help people more easily track memory model
> > related discussions. This could also help bring memory model discussions
> > to a broader audience. Therefore, add the list information to the LKMM
> > maintainers entry.
> >
> > Signed-off-by: Boqun Feng <boqun.feng@gmail.com>
> > Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
>
> Acked-by: Andrea Parri <parri.andrea@gmail.com>
Thank you! I will apply this on my next rebase.
Thanx, Paul
^ permalink raw reply [flat|nested] 11+ messages in thread
* [PATCH memory-model 2/7] tools/memory-model: Add atomic_andnot() with its variants
2025-02-20 16:13 [PATCH memory-model 0/7] LKMM updates for v6.15 Paul E. McKenney
@ 2025-02-20 16:13 ` Paul E. McKenney
0 siblings, 0 replies; 11+ messages in thread
From: Paul E. McKenney @ 2025-02-20 16:13 UTC (permalink / raw)
To: linux-kernel, linux-arch, lkmm, kernel-team, mingo
Cc: stern, parri.andrea, will, peterz, boqun.feng, npiggin, dhowells,
j.alglave, luc.maranget, akiyks, Puranjay Mohan,
Paul E . McKenney, Daniel Lustig, Joel Fernandes
From: Puranjay Mohan <puranjay@kernel.org>
Pull-855[1] added the support of atomic_andnot() to the herd tool. Use
this to add the implementation in the LKMM. All of the ordering variants
are also added.
Here is a small litmus-test that uses this operation:
C andnot
{
atomic_t u = ATOMIC_INIT(7);
}
P0(atomic_t *u)
{
r0 = atomic_fetch_andnot(3, u);
r1 = READ_ONCE(*u);
}
exists (0:r0=7 /\ 0:r1=4)
Test andnot Allowed
States 1
0:r0=7; 0:r1=4;
Ok
Witnesses
Positive: 1 Negative: 0
Condition exists (0:r0=7 /\ 0:r1=4)
Observation andnot Always 1 0
Time andnot 0.00
Hash=78f011a0b5a0c65fa1cf106fcd62c845
[1] https://github.com/herd/herdtools7/pull/855
Signed-off-by: Puranjay Mohan <puranjay@kernel.org>
Acked-by: Andrea Parri <parri.andrea@gmail.com>
Signed-off-by: Paul E. McKenney <paulmck@kernel.org>
Cc: Alan Stern <stern@rowland.harvard.edu>
Cc: Will Deacon <will@kernel.org>
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: Akira Yokosawa <akiyks@gmail.com>
Cc: Daniel Lustig <dlustig@nvidia.com>
Cc: Joel Fernandes <joel@joelfernandes.org>
Cc: <linux-arch@vger.kernel.org>
---
tools/memory-model/linux-kernel.def | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def
index d1f11930ec512..a12b96c547b7a 100644
--- a/tools/memory-model/linux-kernel.def
+++ b/tools/memory-model/linux-kernel.def
@@ -70,6 +70,7 @@ atomic_or(V,X) { __atomic_op(X,|,V); }
atomic_xor(V,X) { __atomic_op(X,^,V); }
atomic_inc(X) { __atomic_op(X,+,1); }
atomic_dec(X) { __atomic_op(X,-,1); }
+atomic_andnot(V,X) { __atomic_op(X,&~,V); }
atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V)
atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V)
@@ -138,3 +139,8 @@ atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0
atomic_add_negative_relaxed(V,X) __atomic_op_return{once}(X,+,V) < 0
atomic_add_negative_acquire(V,X) __atomic_op_return{acquire}(X,+,V) < 0
atomic_add_negative_release(V,X) __atomic_op_return{release}(X,+,V) < 0
+
+atomic_fetch_andnot(V,X) __atomic_fetch_op{mb}(X,&~,V)
+atomic_fetch_andnot_acquire(V,X) __atomic_fetch_op{acquire}(X,&~,V)
+atomic_fetch_andnot_release(V,X) __atomic_fetch_op{release}(X,&~,V)
+atomic_fetch_andnot_relaxed(V,X) __atomic_fetch_op{once}(X,&~,V)
--
2.40.1
^ permalink raw reply related [flat|nested] 11+ messages in thread
end of thread, other threads:[~2025-02-20 16:14 UTC | newest]
Thread overview: 11+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2024-08-02 0:22 [PATCH memory-model 0/7] LKMM updates for v6.12 Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 1/7] tools/memory-model: Add atomic_and()/or()/xor() and add_negative Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 2/7] tools/memory-model: Add atomic_andnot() with its variants Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 3/7] tools/memory-model: Document herd7 (abstract) representation Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 4/7] tools/memory-model: Add locking.txt and glossary.txt to README Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 5/7] tools/memory-model: simple.txt: Fix stale reference to recipes-pairs.txt Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 6/7] docs/memory-barriers.txt: Remove left-over references to "CACHE COHERENCY" Paul E. McKenney
2024-08-02 0:22 ` [PATCH memory-model 7/7] MAINTAINERS: Add the dedicated maillist info for LKMM Paul E. McKenney
2024-08-02 9:46 ` Andrea Parri
2024-08-02 17:47 ` Paul E. McKenney
-- strict thread matches above, loose matches on Subject: below --
2025-02-20 16:13 [PATCH memory-model 0/7] LKMM updates for v6.15 Paul E. McKenney
2025-02-20 16:13 ` [PATCH memory-model 2/7] tools/memory-model: Add atomic_andnot() with its variants Paul E. McKenney
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox