Skip to content

Commit 4f59fda

Browse files
adpaco-awsadpaco-aws
authored
Update tests & docs for new atomic intrinsics without ordering restrictions (#1487)
* Update intrinsics table * Test new orderings
1 parent de71c09 commit 4f59fda

File tree

3 files changed

+194
-105
lines changed

3 files changed

+194
-105
lines changed

‎docs/src/rust-feature-support/intrinsics.md‎

Lines changed: 73 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -21,94 +21,106 @@ assert_inhabited | Yes | |
2121
assert_uninit_valid | Yes | |
2222
assert_zero_valid | Yes | |
2323
assume | Yes | |
24-
atomic_and | Partial | See [Atomics](#atomics) |
25-
atomic_and_acq | Partial | See [Atomics](#atomics) |
24+
atomic_and_seqcst | Partial | See [Atomics](#atomics) |
25+
atomic_and_acquire | Partial | See [Atomics](#atomics) |
2626
atomic_and_acqrel | Partial | See [Atomics](#atomics) |
27-
atomic_and_rel | Partial | See [Atomics](#atomics) |
27+
atomic_and_release | Partial | See [Atomics](#atomics) |
2828
atomic_and_relaxed | Partial | See [Atomics](#atomics) |
29-
atomic_cxchg | Partial | See [Atomics](#atomics) |
30-
atomic_cxchg_acq | Partial | See [Atomics](#atomics) |
31-
atomic_cxchg_acq_failrelaxed | Partial | See [Atomics](#atomics) |
32-
atomic_cxchg_acqrel | Partial | See [Atomics](#atomics) |
33-
atomic_cxchg_acqrel_failrelaxed | Partial | See [Atomics](#atomics) |
34-
atomic_cxchg_failacq | Partial | See [Atomics](#atomics) |
35-
atomic_cxchg_failrelaxed | Partial | See [Atomics](#atomics) |
36-
atomic_cxchg_rel | Partial | See [Atomics](#atomics) |
37-
atomic_cxchg_relaxed | Partial | See [Atomics](#atomics) |
38-
atomic_cxchgweak | Partial | See [Atomics](#atomics) |
39-
atomic_cxchgweak_acq | Partial | See [Atomics](#atomics) |
40-
atomic_cxchgweak_acq_failrelaxed | Partial | See [Atomics](#atomics) |
41-
atomic_cxchgweak_acqrel | Partial | See [Atomics](#atomics) |
42-
atomic_cxchgweak_acqrel_failrelaxed | Partial | See [Atomics](#atomics) |
43-
atomic_cxchgweak_failacq | Partial | See [Atomics](#atomics) |
44-
atomic_cxchgweak_failrelaxed | Partial | See [Atomics](#atomics) |
45-
atomic_cxchgweak_rel | Partial | See [Atomics](#atomics) |
46-
atomic_cxchgweak_relaxed | Partial | See [Atomics](#atomics) |
47-
atomic_fence | Partial | See [Atomics](#atomics) |
48-
atomic_fence_acq | Partial | See [Atomics](#atomics) |
29+
atomic_cxchg_acqrel_acquire | Partial | See [Atomics](#atomics) |
30+
atomic_cxchg_acqrel_relaxed | Partial | See [Atomics](#atomics) |
31+
atomic_cxchg_acqrel_seqcst | Partial | See [Atomics](#atomics) |
32+
atomic_cxchg_acquire_acquire | Partial | See [Atomics](#atomics) |
33+
atomic_cxchg_acquire_relaxed | Partial | See [Atomics](#atomics) |
34+
atomic_cxchg_acquire_seqcst | Partial | See [Atomics](#atomics) |
35+
atomic_cxchg_relaxed_acquire | Partial | See [Atomics](#atomics) |
36+
atomic_cxchg_relaxed_relaxed | Partial | See [Atomics](#atomics) |
37+
atomic_cxchg_relaxed_seqcst | Partial | See [Atomics](#atomics) |
38+
atomic_cxchg_release_acquire | Partial | See [Atomics](#atomics) |
39+
atomic_cxchg_release_relaxed | Partial | See [Atomics](#atomics) |
40+
atomic_cxchg_release_seqcst | Partial | See [Atomics](#atomics) |
41+
atomic_cxchg_seqcst_acquire | Partial | See [Atomics](#atomics) |
42+
atomic_cxchg_seqcst_relaxed | Partial | See [Atomics](#atomics) |
43+
atomic_cxchg_seqcst_seqcst | Partial | See [Atomics](#atomics) |
44+
atomic_cxchgweak_acqrel_acquire | Partial | See [Atomics](#atomics) |
45+
atomic_cxchgweak_acqrel_relaxed | Partial | See [Atomics](#atomics) |
46+
atomic_cxchgweak_acqrel_seqcst | Partial | See [Atomics](#atomics) |
47+
atomic_cxchgweak_acquire_acquire | Partial | See [Atomics](#atomics) |
48+
atomic_cxchgweak_acquire_relaxed | Partial | See [Atomics](#atomics) |
49+
atomic_cxchgweak_acquire_seqcst | Partial | See [Atomics](#atomics) |
50+
atomic_cxchgweak_relaxed_acquire | Partial | See [Atomics](#atomics) |
51+
atomic_cxchgweak_relaxed_relaxed | Partial | See [Atomics](#atomics) |
52+
atomic_cxchgweak_relaxed_seqcst | Partial | See [Atomics](#atomics) |
53+
atomic_cxchgweak_release_acquire | Partial | See [Atomics](#atomics) |
54+
atomic_cxchgweak_release_relaxed | Partial | See [Atomics](#atomics) |
55+
atomic_cxchgweak_release_seqcst | Partial | See [Atomics](#atomics) |
56+
atomic_cxchgweak_seqcst_acquire | Partial | See [Atomics](#atomics) |
57+
atomic_cxchgweak_seqcst_relaxed | Partial | See [Atomics](#atomics) |
58+
atomic_cxchgweak_seqcst_seqcst | Partial | See [Atomics](#atomics) |
59+
atomic_fence_seqcst | Partial | See [Atomics](#atomics) |
60+
atomic_fence_acquire | Partial | See [Atomics](#atomics) |
4961
atomic_fence_acqrel | Partial | See [Atomics](#atomics) |
50-
atomic_fence_rel | Partial | See [Atomics](#atomics) |
51-
atomic_load | Partial | See [Atomics](#atomics) |
52-
atomic_load_acq | Partial | See [Atomics](#atomics) |
62+
atomic_fence_release | Partial | See [Atomics](#atomics) |
63+
atomic_load_seqcst | Partial | See [Atomics](#atomics) |
64+
atomic_load_acquire | Partial | See [Atomics](#atomics) |
5365
atomic_load_relaxed | Partial | See [Atomics](#atomics) |
5466
atomic_load_unordered | Partial | See [Atomics](#atomics) |
55-
atomic_max | Partial | See [Atomics](#atomics) |
56-
atomic_max_acq | Partial | See [Atomics](#atomics) |
67+
atomic_max_seqcst | Partial | See [Atomics](#atomics) |
68+
atomic_max_acquire | Partial | See [Atomics](#atomics) |
5769
atomic_max_acqrel | Partial | See [Atomics](#atomics) |
58-
atomic_max_rel | Partial | See [Atomics](#atomics) |
70+
atomic_max_release | Partial | See [Atomics](#atomics) |
5971
atomic_max_relaxed | Partial | See [Atomics](#atomics) |
60-
atomic_min | Partial | See [Atomics](#atomics) |
61-
atomic_min_acq | Partial | See [Atomics](#atomics) |
72+
atomic_min_seqcst | Partial | See [Atomics](#atomics) |
73+
atomic_min_acquire | Partial | See [Atomics](#atomics) |
6274
atomic_min_acqrel | Partial | See [Atomics](#atomics) |
63-
atomic_min_rel | Partial | See [Atomics](#atomics) |
75+
atomic_min_release | Partial | See [Atomics](#atomics) |
6476
atomic_min_relaxed | Partial | See [Atomics](#atomics) |
65-
atomic_nand | Partial | See [Atomics](#atomics) |
66-
atomic_nand_acq | Partial | See [Atomics](#atomics) |
77+
atomic_nand_seqcst | Partial | See [Atomics](#atomics) |
78+
atomic_nand_acquire | Partial | See [Atomics](#atomics) |
6779
atomic_nand_acqrel | Partial | See [Atomics](#atomics) |
68-
atomic_nand_rel | Partial | See [Atomics](#atomics) |
80+
atomic_nand_release | Partial | See [Atomics](#atomics) |
6981
atomic_nand_relaxed | Partial | See [Atomics](#atomics) |
70-
atomic_or | Partial | See [Atomics](#atomics) |
71-
atomic_or_acq | Partial | See [Atomics](#atomics) |
82+
atomic_or_seqcst | Partial | See [Atomics](#atomics) |
83+
atomic_or_acquire | Partial | See [Atomics](#atomics) |
7284
atomic_or_acqrel | Partial | See [Atomics](#atomics) |
73-
atomic_or_rel | Partial | See [Atomics](#atomics) |
85+
atomic_or_release | Partial | See [Atomics](#atomics) |
7486
atomic_or_relaxed | Partial | See [Atomics](#atomics) |
75-
atomic_singlethreadfence | Partial | See [Atomics](#atomics) |
76-
atomic_singlethreadfence_acq | Partial | See [Atomics](#atomics) |
87+
atomic_singlethreadfence_seqcst | Partial | See [Atomics](#atomics) |
88+
atomic_singlethreadfence_acquire | Partial | See [Atomics](#atomics) |
7789
atomic_singlethreadfence_acqrel | Partial | See [Atomics](#atomics) |
78-
atomic_singlethreadfence_rel | Partial | See [Atomics](#atomics) |
79-
atomic_store | Partial | See [Atomics](#atomics) |
80-
atomic_store_rel | Partial | See [Atomics](#atomics) |
90+
atomic_singlethreadfence_release | Partial | See [Atomics](#atomics) |
91+
atomic_store_seqcst | Partial | See [Atomics](#atomics) |
92+
atomic_store_release | Partial | See [Atomics](#atomics) |
8193
atomic_store_relaxed | Partial | See [Atomics](#atomics) |
8294
atomic_store_unordered | Partial | See [Atomics](#atomics) |
83-
atomic_umax | Partial | See [Atomics](#atomics) |
84-
atomic_umax_acq | Partial | See [Atomics](#atomics) |
95+
atomic_umax_seqcst | Partial | See [Atomics](#atomics) |
96+
atomic_umax_acquire | Partial | See [Atomics](#atomics) |
8597
atomic_umax_acqrel | Partial | See [Atomics](#atomics) |
86-
atomic_umax_rel | Partial | See [Atomics](#atomics) |
98+
atomic_umax_release | Partial | See [Atomics](#atomics) |
8799
atomic_umax_relaxed | Partial | See [Atomics](#atomics) |
88-
atomic_umin | Partial | See [Atomics](#atomics) |
89-
atomic_umin_acq | Partial | See [Atomics](#atomics) |
100+
atomic_umin_seqcst | Partial | See [Atomics](#atomics) |
101+
atomic_umin_acquire | Partial | See [Atomics](#atomics) |
90102
atomic_umin_acqrel | Partial | See [Atomics](#atomics) |
91-
atomic_umin_rel | Partial | See [Atomics](#atomics) |
103+
atomic_umin_release | Partial | See [Atomics](#atomics) |
92104
atomic_umin_relaxed | Partial | See [Atomics](#atomics) |
93-
atomic_xadd | Partial | See [Atomics](#atomics) |
94-
atomic_xadd_acq | Partial | See [Atomics](#atomics) |
105+
atomic_xadd_seqcst | Partial | See [Atomics](#atomics) |
106+
atomic_xadd_acquire | Partial | See [Atomics](#atomics) |
95107
atomic_xadd_acqrel | Partial | See [Atomics](#atomics) |
96-
atomic_xadd_rel | Partial | See [Atomics](#atomics) |
108+
atomic_xadd_release | Partial | See [Atomics](#atomics) |
97109
atomic_xadd_relaxed | Partial | See [Atomics](#atomics) |
98-
atomic_xchg | Partial | See [Atomics](#atomics) |
99-
atomic_xchg_acq | Partial | See [Atomics](#atomics) |
110+
atomic_xchg_seqcst | Partial | See [Atomics](#atomics) |
111+
atomic_xchg_acquire | Partial | See [Atomics](#atomics) |
100112
atomic_xchg_acqrel | Partial | See [Atomics](#atomics) |
101-
atomic_xchg_rel | Partial | See [Atomics](#atomics) |
113+
atomic_xchg_release | Partial | See [Atomics](#atomics) |
102114
atomic_xchg_relaxed | Partial | See [Atomics](#atomics) |
103-
atomic_xor | Partial | See [Atomics](#atomics) |
104-
atomic_xor_acq | Partial | See [Atomics](#atomics) |
115+
atomic_xor_seqcst | Partial | See [Atomics](#atomics) |
116+
atomic_xor_acquire | Partial | See [Atomics](#atomics) |
105117
atomic_xor_acqrel | Partial | See [Atomics](#atomics) |
106-
atomic_xor_rel | Partial | See [Atomics](#atomics) |
118+
atomic_xor_release | Partial | See [Atomics](#atomics) |
107119
atomic_xor_relaxed | Partial | See [Atomics](#atomics) |
108-
atomic_xsub | Partial | See [Atomics](#atomics) |
109-
atomic_xsub_acq | Partial | See [Atomics](#atomics) |
120+
atomic_xsub_seqcst | Partial | See [Atomics](#atomics) |
121+
atomic_xsub_acquire | Partial | See [Atomics](#atomics) |
110122
atomic_xsub_acqrel | Partial | See [Atomics](#atomics) |
111-
atomic_xsub_rel | Partial | See [Atomics](#atomics) |
123+
atomic_xsub_release | Partial | See [Atomics](#atomics) |
112124
atomic_xsub_relaxed | Partial | See [Atomics](#atomics) |
113125
blackbox | Yes | |
114126
bitreverse | Yes | |

‎tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs‎

Lines changed: 60 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,15 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33

4-
// Check that `atomic_cxchg` and other variants (unstable version) return the
5-
// expected result.
4+
// Check that all variants of the `atomic_cxchg_*` intrinsic (unstable version)
5+
// return the expected result.
66

77
#![feature(core_intrinsics)]
88
use std::intrinsics::{
9-
atomic_cxchg_acqrel_acquire, atomic_cxchg_acqrel_relaxed, atomic_cxchg_acquire_acquire,
10-
atomic_cxchg_acquire_relaxed, atomic_cxchg_relaxed_relaxed, atomic_cxchg_release_relaxed,
9+
atomic_cxchg_acqrel_acquire, atomic_cxchg_acqrel_relaxed, atomic_cxchg_acqrel_seqcst,
10+
atomic_cxchg_acquire_acquire, atomic_cxchg_acquire_relaxed, atomic_cxchg_acquire_seqcst,
11+
atomic_cxchg_relaxed_acquire, atomic_cxchg_relaxed_relaxed, atomic_cxchg_relaxed_seqcst,
12+
atomic_cxchg_release_acquire, atomic_cxchg_release_relaxed, atomic_cxchg_release_seqcst,
1113
atomic_cxchg_seqcst_acquire, atomic_cxchg_seqcst_relaxed, atomic_cxchg_seqcst_seqcst,
1214
};
1315

@@ -22,6 +24,12 @@ fn main() {
2224
let mut a7 = 0 as u8;
2325
let mut a8 = 0 as u8;
2426
let mut a9 = 0 as u8;
27+
let mut a10 = 0 as u8;
28+
let mut a11 = 0 as u8;
29+
let mut a12 = 0 as u8;
30+
let mut a13 = 0 as u8;
31+
let mut a14 = 0 as u8;
32+
let mut a15 = 0 as u8;
2533

2634
let ptr_a1: *mut u8 = &mut a1;
2735
let ptr_a2: *mut u8 = &mut a2;
@@ -32,21 +40,33 @@ fn main() {
3240
let ptr_a7: *mut u8 = &mut a7;
3341
let ptr_a8: *mut u8 = &mut a8;
3442
let ptr_a9: *mut u8 = &mut a9;
43+
let ptr_a10: *mut u8 = &mut a10;
44+
let ptr_a11: *mut u8 = &mut a11;
45+
let ptr_a12: *mut u8 = &mut a12;
46+
let ptr_a13: *mut u8 = &mut a13;
47+
let ptr_a14: *mut u8 = &mut a14;
48+
let ptr_a15: *mut u8 = &mut a15;
3549

3650
unsafe {
3751
// Stores a value if the current value is the same as the old value
3852
// Returns (val, ok) where
3953
// * val: the old value
4054
// * ok: bool indicating whether the operation was successful or not
41-
let x1 = atomic_cxchg_seqcst_seqcst(ptr_a1, 0, 1);
42-
let x2 = atomic_cxchg_acquire_acquire(ptr_a2, 0, 1);
43-
let x3 = atomic_cxchg_acquire_relaxed(ptr_a3, 0, 1);
44-
let x4 = atomic_cxchg_acqrel_acquire(ptr_a4, 0, 1);
45-
let x5 = atomic_cxchg_acqrel_relaxed(ptr_a5, 0, 1);
46-
let x6 = atomic_cxchg_seqcst_acquire(ptr_a6, 0, 1);
47-
let x7 = atomic_cxchg_seqcst_relaxed(ptr_a7, 0, 1);
48-
let x8 = atomic_cxchg_release_relaxed(ptr_a8, 0, 1);
49-
let x9 = atomic_cxchg_relaxed_relaxed(ptr_a9, 0, 1);
55+
let x1 = atomic_cxchg_acqrel_acquire(ptr_a1, 0, 1);
56+
let x2 = atomic_cxchg_acqrel_relaxed(ptr_a2, 0, 1);
57+
let x3 = atomic_cxchg_acqrel_seqcst(ptr_a3, 0, 1);
58+
let x4 = atomic_cxchg_acquire_acquire(ptr_a4, 0, 1);
59+
let x5 = atomic_cxchg_acquire_relaxed(ptr_a5, 0, 1);
60+
let x6 = atomic_cxchg_acquire_seqcst(ptr_a6, 0, 1);
61+
let x7 = atomic_cxchg_relaxed_acquire(ptr_a7, 0, 1);
62+
let x8 = atomic_cxchg_relaxed_relaxed(ptr_a8, 0, 1);
63+
let x9 = atomic_cxchg_relaxed_seqcst(ptr_a9, 0, 1);
64+
let x10 = atomic_cxchg_release_acquire(ptr_a10, 0, 1);
65+
let x11 = atomic_cxchg_release_relaxed(ptr_a11, 0, 1);
66+
let x12 = atomic_cxchg_release_seqcst(ptr_a12, 0, 1);
67+
let x13 = atomic_cxchg_seqcst_acquire(ptr_a13, 0, 1);
68+
let x14 = atomic_cxchg_seqcst_relaxed(ptr_a14, 0, 1);
69+
let x15 = atomic_cxchg_seqcst_seqcst(ptr_a15, 0, 1);
5070

5171
assert!(x1 == (0, true));
5272
assert!(x2 == (0, true));
@@ -57,16 +77,28 @@ fn main() {
5777
assert!(x7 == (0, true));
5878
assert!(x8 == (0, true));
5979
assert!(x9 == (0, true));
80+
assert!(x10 == (0, true));
81+
assert!(x11 == (0, true));
82+
assert!(x12 == (0, true));
83+
assert!(x13 == (0, true));
84+
assert!(x14 == (0, true));
85+
assert!(x15 == (0, true));
6086

61-
let y1 = atomic_cxchg_seqcst_seqcst(ptr_a1, 1, 1);
62-
let y2 = atomic_cxchg_acquire_acquire(ptr_a2, 1, 1);
63-
let y3 = atomic_cxchg_acqrel_relaxed(ptr_a3, 1, 1);
64-
let y4 = atomic_cxchg_acqrel_acquire(ptr_a4, 1, 1);
65-
let y5 = atomic_cxchg_acqrel_relaxed(ptr_a5, 1, 1);
66-
let y6 = atomic_cxchg_seqcst_acquire(ptr_a6, 1, 1);
67-
let y7 = atomic_cxchg_seqcst_relaxed(ptr_a7, 1, 1);
68-
let y8 = atomic_cxchg_release_relaxed(ptr_a8, 1, 1);
69-
let y9 = atomic_cxchg_relaxed_relaxed(ptr_a9, 1, 1);
87+
let y1 = atomic_cxchg_acqrel_acquire(ptr_a1, 1, 1);
88+
let y2 = atomic_cxchg_acqrel_relaxed(ptr_a2, 1, 1);
89+
let y3 = atomic_cxchg_acqrel_seqcst(ptr_a3, 1, 1);
90+
let y4 = atomic_cxchg_acquire_acquire(ptr_a4, 1, 1);
91+
let y5 = atomic_cxchg_acquire_relaxed(ptr_a5, 1, 1);
92+
let y6 = atomic_cxchg_acquire_seqcst(ptr_a6, 1, 1);
93+
let y7 = atomic_cxchg_relaxed_acquire(ptr_a7, 1, 1);
94+
let y8 = atomic_cxchg_relaxed_relaxed(ptr_a8, 1, 1);
95+
let y9 = atomic_cxchg_relaxed_seqcst(ptr_a9, 1, 1);
96+
let y10 = atomic_cxchg_release_acquire(ptr_a10, 1, 1);
97+
let y11 = atomic_cxchg_release_relaxed(ptr_a11, 1, 1);
98+
let y12 = atomic_cxchg_release_seqcst(ptr_a12, 1, 1);
99+
let y13 = atomic_cxchg_seqcst_acquire(ptr_a13, 1, 1);
100+
let y14 = atomic_cxchg_seqcst_relaxed(ptr_a14, 1, 1);
101+
let y15 = atomic_cxchg_seqcst_seqcst(ptr_a15, 1, 1);
70102

71103
assert!(y1 == (1, true));
72104
assert!(y2 == (1, true));
@@ -77,5 +109,11 @@ fn main() {
77109
assert!(y7 == (1, true));
78110
assert!(y8 == (1, true));
79111
assert!(y9 == (1, true));
112+
assert!(y10 == (1, true));
113+
assert!(y11 == (1, true));
114+
assert!(y12 == (1, true));
115+
assert!(y13 == (1, true));
116+
assert!(y14 == (1, true));
117+
assert!(y15 == (1, true));
80118
}
81119
}

0 commit comments

Comments
 (0)