Skip to content

Commit ee20260

Browse files
committed
Merge tag 'lkmm.2024.05.10a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu
Pull LKMM documentation updates from Paul McKenney: "This upgrades LKMM documentation, perhaps most notably adding a number of litmus tests illustrating cmpxchg() ordering properties. TL;DR: Failing cmpxchg() operations provide no ordering" * tag 'lkmm.2024.05.10a' of git://git.kernel.org/pub/scm/linux/kernel/git/paulmck/linux-rcu: Documentation/litmus-tests: Make cmpxchg() tests safe for klitmus Documentation/atomic_t: Emphasize that failed atomic operations give no ordering Documentation/litmus-tests: Demonstrate unordered failing cmpxchg Documentation/litmus-tests: Add locking tests to README
2 parents 2e57d1d + 2ba5b41 commit ee20260

File tree

6 files changed

+176
-2
lines changed

6 files changed

+176
-2
lines changed

Documentation/atomic_t.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -171,14 +171,14 @@ The rule of thumb:
171171
- RMW operations that are conditional are unordered on FAILURE,
172172
otherwise the above rules apply.
173173

174-
Except of course when an operation has an explicit ordering like:
174+
Except of course when a successful operation has an explicit ordering like:
175175

176176
{}_relaxed: unordered
177177
{}_acquire: the R of the RMW (or atomic_read) is an ACQUIRE
178178
{}_release: the W of the RMW (or atomic_set) is a RELEASE
179179

180180
Where 'unordered' is against other memory locations. Address dependencies are
181-
not defeated.
181+
not defeated. Conditional operations are still unordered on FAILURE.
182182

183183
Fully ordered primitives are ordered against everything prior and everything
184184
subsequent. Therefore a fully ordered primitive is like having an smp_mb()

Documentation/litmus-tests/README

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,51 @@ Atomic-RMW-ops-are-atomic-WRT-atomic_set.litmus
2121
Test that atomic_set() cannot break the atomicity of atomic RMWs.
2222
NOTE: Require herd7 7.56 or later which supports "(void)expr".
2323

24+
cmpxchg-fail-ordered-1.litmus
25+
Demonstrate that a failing cmpxchg() operation acts as a full barrier
26+
when followed by smp_mb__after_atomic().
27+
28+
cmpxchg-fail-ordered-2.litmus
29+
Demonstrate that a failing cmpxchg() operation acts as an acquire
30+
operation when followed by smp_mb__after_atomic().
31+
32+
cmpxchg-fail-unordered-1.litmus
33+
Demonstrate that a failing cmpxchg() operation does not act as a
34+
full barrier.
35+
36+
cmpxchg-fail-unordered-2.litmus
37+
Demonstrate that a failing cmpxchg() operation does not act as an
38+
acquire operation.
39+
40+
41+
locking (/locking directory)
42+
----------------------------
43+
44+
DCL-broken.litmus
45+
Demonstrates that double-checked locking needs more than just
46+
the obvious lock acquisitions and releases.
47+
48+
DCL-fixed.litmus
49+
Demonstrates corrected double-checked locking that uses
50+
smp_store_release() and smp_load_acquire() in addition to the
51+
obvious lock acquisitions and releases.
52+
53+
RM-broken.litmus
54+
Demonstrates problems with "roach motel" locking, where code is
55+
freely moved into lock-based critical sections. This example also
56+
shows how to use the "filter" clause to discard executions that
57+
would be excluded by other code not modeled in the litmus test.
58+
Note also that this "roach motel" optimization is emulated by
59+
physically moving P1()'s two reads from x under the lock.
60+
61+
What is a roach motel? This is from an old advertisement for
62+
a cockroach trap, much later featured in one of the "Men in
63+
Black" movies. "The roaches check in. They don't check out."
64+
65+
RM-fixed.litmus
66+
The counterpart to RM-broken.litmus, showing P0()'s two loads from
67+
x safely outside of the critical section.
68+
2469

2570
RCU (/rcu directory)
2671
--------------------
Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
C cmpxchg-fail-ordered-1
2+
3+
(*
4+
* Result: Never
5+
*
6+
* Demonstrate that a failing cmpxchg() operation will act as a full
7+
* barrier when followed by smp_mb__after_atomic().
8+
*)
9+
10+
{}
11+
12+
P0(int *x, int *y, int *z)
13+
{
14+
int r0;
15+
int r1;
16+
17+
WRITE_ONCE(*x, 1);
18+
r1 = cmpxchg(z, 1, 0);
19+
smp_mb__after_atomic();
20+
r0 = READ_ONCE(*y);
21+
}
22+
23+
P1(int *x, int *y, int *z)
24+
{
25+
int r0;
26+
int r1;
27+
28+
WRITE_ONCE(*y, 1);
29+
r1 = cmpxchg(z, 1, 0);
30+
smp_mb__after_atomic();
31+
r0 = READ_ONCE(*x);
32+
}
33+
34+
locations[0:r1;1:r1]
35+
exists (0:r0=0 /\ 1:r0=0)
Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
C cmpxchg-fail-ordered-2
2+
3+
(*
4+
* Result: Never
5+
*
6+
* Demonstrate use of smp_mb__after_atomic() to make a failing cmpxchg
7+
* operation have acquire ordering.
8+
*)
9+
10+
{}
11+
12+
P0(int *x, int *y)
13+
{
14+
int r1;
15+
16+
WRITE_ONCE(*x, 1);
17+
r1 = cmpxchg(y, 0, 1);
18+
}
19+
20+
P1(int *x, int *y)
21+
{
22+
int r1;
23+
int r2;
24+
25+
r1 = cmpxchg(y, 0, 1);
26+
smp_mb__after_atomic();
27+
r2 = READ_ONCE(*x);
28+
}
29+
30+
exists (0:r1=0 /\ 1:r1=1 /\ 1:r2=0)
Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
C cmpxchg-fail-unordered-1
2+
3+
(*
4+
* Result: Sometimes
5+
*
6+
* Demonstrate that a failing cmpxchg() operation does not act as a
7+
* full barrier. (In contrast, a successful cmpxchg() does act as a
8+
* full barrier.)
9+
*)
10+
11+
{}
12+
13+
P0(int *x, int *y, int *z)
14+
{
15+
int r0;
16+
int r1;
17+
18+
WRITE_ONCE(*x, 1);
19+
r1 = cmpxchg(z, 1, 0);
20+
r0 = READ_ONCE(*y);
21+
}
22+
23+
P1(int *x, int *y, int *z)
24+
{
25+
int r0;
26+
int r1;
27+
28+
WRITE_ONCE(*y, 1);
29+
r1 = cmpxchg(z, 1, 0);
30+
r0 = READ_ONCE(*x);
31+
}
32+
33+
locations[0:r1;1:r1]
34+
exists (0:r0=0 /\ 1:r0=0)
Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
C cmpxchg-fail-unordered-2
2+
3+
(*
4+
* Result: Sometimes
5+
*
6+
* Demonstrate that a failing cmpxchg() operation does not act as either
7+
* an acquire release operation. (In contrast, a successful cmpxchg()
8+
* does act as both an acquire and a release operation.)
9+
*)
10+
11+
{}
12+
13+
P0(int *x, int *y)
14+
{
15+
int r1;
16+
17+
WRITE_ONCE(*x, 1);
18+
r1 = cmpxchg(y, 0, 1);
19+
}
20+
21+
P1(int *x, int *y)
22+
{
23+
int r1;
24+
int r2;
25+
26+
r1 = cmpxchg(y, 0, 1);
27+
r2 = READ_ONCE(*x);
28+
}
29+
30+
exists (0:r1=0 /\ 1:r1=1 /\ 1:r2=0)

0 commit comments

Comments
 (0)