Skip to content

Commit 293f5bc

Browse files
committed
Documentation/litmus-tests: Demonstrate unordered failing cmpxchg
This commit adds four litmus tests showing that a failing cmpxchg() operation is unordered unless followed by an smp_mb__after_atomic() operation. Suggested-by: Frederic Weisbecker <[email protected]> Signed-off-by: Paul E. McKenney <[email protected]> Cc: Alan Stern <[email protected]> Cc: Will Deacon <[email protected]> Cc: Peter Zijlstra <[email protected]> Cc: Boqun Feng <[email protected]> Cc: Nicholas Piggin <[email protected]> Cc: David Howells <[email protected]> Cc: Jade Alglave <[email protected]> Cc: Luc Maranget <[email protected]> Cc: "Paul E. McKenney" <[email protected]> Cc: Akira Yokosawa <[email protected]> Cc: Daniel Lustig <[email protected]> Cc: Joel Fernandes <[email protected]> Cc: Mark Rutland <[email protected]> Cc: Jonathan Corbet <[email protected]> Cc: <[email protected]> Cc: <[email protected]> Acked-by: Andrea Parri <[email protected]>
1 parent d2c470c commit 293f5bc

File tree

5 files changed

+143
-0
lines changed

5 files changed

+143
-0
lines changed

Documentation/litmus-tests/README

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,22 @@ 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+
2440

2541
locking (/locking directory)
2642
----------------------------
Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
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+
27+
WRITE_ONCE(*y, 1);
28+
r1 = cmpxchg(z, 1, 0);
29+
smp_mb__after_atomic();
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-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 r0;
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 r0;
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: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,33 @@
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+
27+
WRITE_ONCE(*y, 1);
28+
r1 = cmpxchg(z, 1, 0);
29+
r0 = READ_ONCE(*x);
30+
}
31+
32+
locations[0:r1;1:r1]
33+
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 r0;
16+
int r1;
17+
18+
WRITE_ONCE(*x, 1);
19+
r1 = cmpxchg(y, 0, 1);
20+
}
21+
22+
P1(int *x, int *y)
23+
{
24+
int r0;
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)