Skip to content

Commit 72b4080

Browse files
torvaldstorvalds
committed
Merge tag 'lkmm.2025.03.21a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu
Pull kernel memory model updates from Paul McKenney: "Add more atomic operations, rework tags, and update documentation: - Add additional atomic operations (Puranjay Mohan) - Make better use of herd7 tags (Jonas Oberhauser) - Update documentation (Akira Yokosawa) These changes require v7.58 of the herd7 and klitmus tools, up from v7.52" * tag 'lkmm.2025.03.21a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu: tools/memory-model: glossary.txt: Fix indents tools/memory-model/README: Fix typo tools/memory-model: Distinguish between syntactic and semantic tags tools/memory-model: Switch to softcoded herd7 tags tools/memory-model: Define effect of Mb tags on RMWs in tools/... tools/memory-model: Define applicable tags on operation in tools/... tools/memory-model: Legitimize current use of tags in LKMM macros tools/memory-model: Add atomic_andnot() with its variants tools/memory-model: Add atomic_and()/or()/xor() and add_negative
2 parents 418beca + a2bfbf8 commit 72b4080

File tree

7 files changed

+178
-120
lines changed

7 files changed

+178
-120
lines changed

‎tools/memory-model/Documentation/glossary.txt

Lines changed: 16 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -15,14 +15,14 @@ Address Dependency: When the address of a later memory access is computed
1515
3 do_something(p->a);
1616
4 rcu_read_unlock();
1717

18-
In this case, because the address of "p->a" on line 3 is computed
19-
from the value returned by the rcu_dereference() on line 2, the
20-
address dependency extends from that rcu_dereference() to that
21-
"p->a". In rare cases, optimizing compilers can destroy address
22-
dependencies. Please see Documentation/RCU/rcu_dereference.rst
23-
for more information.
18+
In this case, because the address of "p->a" on line 3 is computed
19+
from the value returned by the rcu_dereference() on line 2, the
20+
address dependency extends from that rcu_dereference() to that
21+
"p->a". In rare cases, optimizing compilers can destroy address
22+
dependencies. Please see Documentation/RCU/rcu_dereference.rst
23+
for more information.
2424

25-
See also "Control Dependency" and "Data Dependency".
25+
See also "Control Dependency" and "Data Dependency".
2626

2727
Acquire: With respect to a lock, acquiring that lock, for example,
2828
using spin_lock(). With respect to a non-lock shared variable,
@@ -59,23 +59,23 @@ Control Dependency: When a later store's execution depends on a test
5959
1 if (READ_ONCE(x))
6060
2 WRITE_ONCE(y, 1);
6161

62-
Here, the control dependency extends from the READ_ONCE() on
63-
line 1 to the WRITE_ONCE() on line 2. Control dependencies are
64-
fragile, and can be easily destroyed by optimizing compilers.
65-
Please see control-dependencies.txt for more information.
62+
Here, the control dependency extends from the READ_ONCE() on
63+
line 1 to the WRITE_ONCE() on line 2. Control dependencies are
64+
fragile, and can be easily destroyed by optimizing compilers.
65+
Please see control-dependencies.txt for more information.
6666

67-
See also "Address Dependency" and "Data Dependency".
67+
See also "Address Dependency" and "Data Dependency".
6868

6969
Cycle: Memory-barrier pairing is restricted to a pair of CPUs, as the
7070
name suggests. And in a great many cases, a pair of CPUs is all
7171
that is required. In other cases, the notion of pairing must be
7272
extended to additional CPUs, and the result is called a "cycle".
7373
In a cycle, each CPU's ordering interacts with that of the next:
7474

75-
CPU 0 CPU 1 CPU 2
76-
WRITE_ONCE(x, 1); WRITE_ONCE(y, 1); WRITE_ONCE(z, 1);
77-
smp_mb(); smp_mb(); smp_mb();
78-
r0 = READ_ONCE(y); r1 = READ_ONCE(z); r2 = READ_ONCE(x);
75+
CPU 0 CPU 1 CPU 2
76+
WRITE_ONCE(x, 1); WRITE_ONCE(y, 1); WRITE_ONCE(z, 1);
77+
smp_mb(); smp_mb(); smp_mb();
78+
r0 = READ_ONCE(y); r1 = READ_ONCE(z); r2 = READ_ONCE(x);
7979

8080
CPU 0's smp_mb() interacts with that of CPU 1, which interacts
8181
with that of CPU 2, which in turn interacts with that of CPU 0

‎tools/memory-model/Documentation/herd-representation.txt

Lines changed: 26 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,11 @@
1818
#
1919
# By convention, a blank line in a cell means "same as the preceding line".
2020
#
21+
# Note that the syntactic representation does not always match the sets and
22+
# relations in linux-kernel.cat, due to redefinitions in linux-kernel.bell and
23+
# lock.cat. For example, the po link between LKR and LKW is upgraded to an rmw
24+
# link, and W[ACQUIRE] are not included in the Acquire set.
25+
#
2126
# Disclaimer. The table includes representations of "add" and "and" operations;
2227
# corresponding/identical representations of "sub", "inc", "dec" and "or", "xor",
2328
# "andnot" operations are omitted.
@@ -27,16 +32,16 @@
2732
------------------------------------------------------------------------------
2833
| Non-RMW ops | |
2934
------------------------------------------------------------------------------
30-
| READ_ONCE | R[once] |
35+
| READ_ONCE | R[ONCE] |
3136
| atomic_read | |
32-
| WRITE_ONCE | W[once] |
37+
| WRITE_ONCE | W[ONCE] |
3338
| atomic_set | |
34-
| smp_load_acquire | R[acquire] |
39+
| smp_load_acquire | R[ACQUIRE] |
3540
| atomic_read_acquire | |
36-
| smp_store_release | W[release] |
41+
| smp_store_release | W[RELEASE] |
3742
| atomic_set_release | |
38-
| smp_store_mb | W[once] ->po F[mb] |
39-
| smp_mb | F[mb] |
43+
| smp_store_mb | W[ONCE] ->po F[MB] |
44+
| smp_mb | F[MB] |
4045
| smp_rmb | F[rmb] |
4146
| smp_wmb | F[wmb] |
4247
| smp_mb__before_atomic | F[before-atomic] |
@@ -49,8 +54,8 @@
4954
| rcu_read_lock | F[rcu-lock] |
5055
| rcu_read_unlock | F[rcu-unlock] |
5156
| synchronize_rcu | F[sync-rcu] |
52-
| rcu_dereference | R[once] |
53-
| rcu_assign_pointer | W[release] |
57+
| rcu_dereference | R[ONCE] |
58+
| rcu_assign_pointer | W[RELEASE] |
5459
| srcu_read_lock | R[srcu-lock] |
5560
| srcu_down_read | |
5661
| srcu_read_unlock | W[srcu-unlock] |
@@ -60,32 +65,31 @@
6065
------------------------------------------------------------------------------
6166
| RMW ops w/o return value | |
6267
------------------------------------------------------------------------------
63-
| atomic_add | R*[noreturn] ->rmw W*[once] |
68+
| atomic_add | R*[NORETURN] ->rmw W*[NORETURN] |
6469
| atomic_and | |
6570
| spin_lock | LKR ->po LKW |
6671
------------------------------------------------------------------------------
6772
| RMW ops w/ return value | |
6873
------------------------------------------------------------------------------
69-
| atomic_add_return | F[mb] ->po R*[once] |
70-
| | ->rmw W*[once] ->po F[mb] |
74+
| atomic_add_return | R*[MB] ->rmw W*[MB] |
7175
| atomic_fetch_add | |
7276
| atomic_fetch_and | |
7377
| atomic_xchg | |
7478
| xchg | |
7579
| atomic_add_negative | |
76-
| atomic_add_return_relaxed | R*[once] ->rmw W*[once] |
80+
| atomic_add_return_relaxed | R*[ONCE] ->rmw W*[ONCE] |
7781
| atomic_fetch_add_relaxed | |
7882
| atomic_fetch_and_relaxed | |
7983
| atomic_xchg_relaxed | |
8084
| xchg_relaxed | |
8185
| atomic_add_negative_relaxed | |
82-
| atomic_add_return_acquire | R*[acquire] ->rmw W*[once] |
86+
| atomic_add_return_acquire | R*[ACQUIRE] ->rmw W*[ACQUIRE] |
8387
| atomic_fetch_add_acquire | |
8488
| atomic_fetch_and_acquire | |
8589
| atomic_xchg_acquire | |
8690
| xchg_acquire | |
8791
| atomic_add_negative_acquire | |
88-
| atomic_add_return_release | R*[once] ->rmw W*[release] |
92+
| atomic_add_return_release | R*[RELEASE] ->rmw W*[RELEASE] |
8993
| atomic_fetch_add_release | |
9094
| atomic_fetch_and_release | |
9195
| atomic_xchg_release | |
@@ -94,17 +98,16 @@
9498
------------------------------------------------------------------------------
9599
| Conditional RMW ops | |
96100
------------------------------------------------------------------------------
97-
| atomic_cmpxchg | On success: F[mb] ->po R*[once] |
98-
| | ->rmw W*[once] ->po F[mb] |
99-
| | On failure: R*[once] |
101+
| atomic_cmpxchg | On success: R*[MB] ->rmw W*[MB] |
102+
| | On failure: R*[MB] |
100103
| cmpxchg | |
101104
| atomic_add_unless | |
102-
| atomic_cmpxchg_relaxed | On success: R*[once] ->rmw W*[once] |
103-
| | On failure: R*[once] |
104-
| atomic_cmpxchg_acquire | On success: R*[acquire] ->rmw W*[once] |
105-
| | On failure: R*[once] |
106-
| atomic_cmpxchg_release | On success: R*[once] ->rmw W*[release] |
107-
| | On failure: R*[once] |
105+
| atomic_cmpxchg_relaxed | On success: R*[ONCE] ->rmw W*[ONCE] |
106+
| | On failure: R*[ONCE] |
107+
| atomic_cmpxchg_acquire | On success: R*[ACQUIRE] ->rmw W*[ACQUIRE] |
108+
| | On failure: R*[ACQUIRE] |
109+
| atomic_cmpxchg_release | On success: R*[RELEASE] ->rmw W*[RELEASE] |
110+
| | On failure: R*[RELEASE] |
108111
| spin_trylock | On success: LKR ->po LKW |
109112
| | On failure: LF |
110113
------------------------------------------------------------------------------

‎tools/memory-model/README

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ that litmus test to be exercised within the Linux kernel.
2020
REQUIREMENTS
2121
============
2222

23-
Version 7.52 or higher of the "herd7" and "klitmus7" tools must be
23+
Version 7.58 or higher of the "herd7" and "klitmus7" tools must be
2424
downloaded separately:
2525

2626
https://github.com/herd/herdtools7
@@ -79,7 +79,7 @@ Several thousand more example litmus tests are available here:
7979
https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/herd
8080
https://git.kernel.org/pub/scm/linux/kernel/git/paulmck/perfbook.git/tree/CodeSamples/formal/litmus
8181

82-
Documentation describing litmus tests and now to use them may be found
82+
Documentation describing litmus tests and how to use them may be found
8383
here:
8484

8585
tools/memory-model/Documentation/litmus-tests.txt

‎tools/memory-model/linux-kernel.bell

Lines changed: 24 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -13,17 +13,18 @@
1313

1414
"Linux-kernel memory consistency model"
1515

16-
enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) ||
17-
'release (*smp_store_release*) ||
18-
'acquire (*smp_load_acquire*) ||
19-
'noreturn (* R of non-return RMW *)
20-
instructions R[{'once,'acquire,'noreturn}]
21-
instructions W[{'once,'release}]
22-
instructions RMW[{'once,'acquire,'release}]
16+
enum Accesses = 'ONCE (*READ_ONCE,WRITE_ONCE*) ||
17+
'RELEASE (*smp_store_release*) ||
18+
'ACQUIRE (*smp_load_acquire*) ||
19+
'NORETURN (* R of non-return RMW *) ||
20+
'MB (*xchg(),cmpxchg(),...*)
21+
instructions R[Accesses]
22+
instructions W[Accesses]
23+
instructions RMW[Accesses]
2324

2425
enum Barriers = 'wmb (*smp_wmb*) ||
2526
'rmb (*smp_rmb*) ||
26-
'mb (*smp_mb*) ||
27+
'MB (*smp_mb*) ||
2728
'barrier (*barrier*) ||
2829
'rcu-lock (*rcu_read_lock*) ||
2930
'rcu-unlock (*rcu_read_unlock*) ||
@@ -35,6 +36,17 @@ enum Barriers = 'wmb (*smp_wmb*) ||
3536
'after-srcu-read-unlock (*smp_mb__after_srcu_read_unlock*)
3637
instructions F[Barriers]
3738

39+
40+
(*
41+
* Filter out syntactic annotations that do not provide the corresponding
42+
* semantic ordering, such as Acquire on a store or Mb on a failed RMW.
43+
*)
44+
let FailedRMW = RMW \ (domain(rmw) | range(rmw))
45+
let Acquire = ACQUIRE \ W \ FailedRMW
46+
let Release = RELEASE \ R \ FailedRMW
47+
let Mb = MB \ FailedRMW
48+
let Noreturn = NORETURN \ W
49+
3850
(* SRCU *)
3951
enum SRCU = 'srcu-lock || 'srcu-unlock || 'sync-srcu
4052
instructions SRCU[SRCU]
@@ -73,7 +85,7 @@ flag ~empty rcu-rscs & (po ; [Sync-srcu] ; po) as invalid-sleep
7385
flag ~empty different-values(srcu-rscs) as srcu-bad-value-match
7486

7587
(* Compute marked and plain memory accesses *)
76-
let Marked = (~M) | IW | Once | Release | Acquire | domain(rmw) | range(rmw) |
88+
let Marked = (~M) | IW | ONCE | RELEASE | ACQUIRE | MB | RMW |
7789
LKR | LKW | UL | LF | RL | RU | Srcu-lock | Srcu-unlock
7890
let Plain = M \ Marked
7991

@@ -82,3 +94,6 @@ let carry-dep = (data ; [~ Srcu-unlock] ; rfi)*
8294
let addr = carry-dep ; addr
8395
let ctrl = carry-dep ; ctrl
8496
let data = carry-dep ; data
97+
98+
flag ~empty (if "lkmmv2" then 0 else _)
99+
as this-model-requires-variant-higher-than-lkmmv1

‎tools/memory-model/linux-kernel.cat

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,16 @@ let R4rmb = R \ Noreturn (* Reads for which rmb works *)
3434
let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb]
3535
let wmb = [W] ; fencerel(Wmb) ; [W]
3636
let mb = ([M] ; fencerel(Mb) ; [M]) |
37+
(*
38+
* full-barrier RMWs (successful cmpxchg(), xchg(), etc.) act as
39+
* though there were enclosed by smp_mb().
40+
* The effect of these virtual smp_mb() is formalized by adding
41+
* Mb tags to the read and write of the operation, and providing
42+
* the same ordering as though there were additional po edges
43+
* between the Mb tag and the read resp. write.
44+
*)
45+
([M] ; po ; [Mb & R]) |
46+
([Mb & W] ; po ; [M]) |
3747
([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) |
3848
([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) |
3949
([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) |

‎tools/memory-model/linux-kernel.cfg

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
macros linux-kernel.def
22
bell linux-kernel.bell
33
model linux-kernel.cat
4+
variant lkmmv2
45
graph columns
56
squished true
67
showevents noregs

0 commit comments

Comments
 (0)