Skip to content

Commit

Permalink
Update tests & docs for new atomic intrinsics without ordering restri…
Browse files Browse the repository at this point in the history 
…ctions (#1487)

* Update intrinsics table

* Test new orderings
  • Loading branch information
@adpaco-aws
adpaco-aws authored Aug 11, 2022
1 parent de71c09 commit 4f59fda
Show file tree
Hide file tree
Showing 3 changed files with 194 additions and 105 deletions.
134 changes: 73 additions & 61 deletions docs/src/rust-feature-support/intrinsics.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,94 +21,106 @@ assert_inhabited | Yes | |
assert_uninit_valid | Yes | |
assert_zero_valid | Yes | |
assume | Yes | |
atomic_and | Partial | See [Atomics](#atomics) |
atomic_and_acq | Partial | See [Atomics](#atomics) |
atomic_and_seqcst | Partial | See [Atomics](#atomics) |
atomic_and_acquire | Partial | See [Atomics](#atomics) |
atomic_and_acqrel | Partial | See [Atomics](#atomics) |
atomic_and_rel | Partial | See [Atomics](#atomics) |
atomic_and_release | Partial | See [Atomics](#atomics) |
atomic_and_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchg | Partial | See [Atomics](#atomics) |
atomic_cxchg_acq | Partial | See [Atomics](#atomics) |
atomic_cxchg_acq_failrelaxed | Partial | See [Atomics](#atomics) |
atomic_cxchg_acqrel | Partial | See [Atomics](#atomics) |
atomic_cxchg_acqrel_failrelaxed | Partial | See [Atomics](#atomics) |
atomic_cxchg_failacq | Partial | See [Atomics](#atomics) |
atomic_cxchg_failrelaxed | Partial | See [Atomics](#atomics) |
atomic_cxchg_rel | Partial | See [Atomics](#atomics) |
atomic_cxchg_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchgweak | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acq | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acq_failrelaxed | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acqrel | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acqrel_failrelaxed | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_failacq | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_failrelaxed | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_rel | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_relaxed | Partial | See [Atomics](#atomics) |
atomic_fence | Partial | See [Atomics](#atomics) |
atomic_fence_acq | Partial | See [Atomics](#atomics) |
atomic_cxchg_acqrel_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchg_acqrel_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchg_acqrel_seqcst | Partial | See [Atomics](#atomics) |
atomic_cxchg_acquire_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchg_acquire_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchg_acquire_seqcst | Partial | See [Atomics](#atomics) |
atomic_cxchg_relaxed_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchg_relaxed_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchg_relaxed_seqcst | Partial | See [Atomics](#atomics) |
atomic_cxchg_release_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchg_release_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchg_release_seqcst | Partial | See [Atomics](#atomics) |
atomic_cxchg_seqcst_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchg_seqcst_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchg_seqcst_seqcst | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acqrel_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acqrel_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acqrel_seqcst | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acquire_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acquire_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_acquire_seqcst | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_relaxed_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_relaxed_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_relaxed_seqcst | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_release_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_release_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_release_seqcst | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_seqcst_acquire | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_seqcst_relaxed | Partial | See [Atomics](#atomics) |
atomic_cxchgweak_seqcst_seqcst | Partial | See [Atomics](#atomics) |
atomic_fence_seqcst | Partial | See [Atomics](#atomics) |
atomic_fence_acquire | Partial | See [Atomics](#atomics) |
atomic_fence_acqrel | Partial | See [Atomics](#atomics) |
atomic_fence_rel | Partial | See [Atomics](#atomics) |
atomic_load | Partial | See [Atomics](#atomics) |
atomic_load_acq | Partial | See [Atomics](#atomics) |
atomic_fence_release | Partial | See [Atomics](#atomics) |
atomic_load_seqcst | Partial | See [Atomics](#atomics) |
atomic_load_acquire | Partial | See [Atomics](#atomics) |
atomic_load_relaxed | Partial | See [Atomics](#atomics) |
atomic_load_unordered | Partial | See [Atomics](#atomics) |
atomic_max | Partial | See [Atomics](#atomics) |
atomic_max_acq | Partial | See [Atomics](#atomics) |
atomic_max_seqcst | Partial | See [Atomics](#atomics) |
atomic_max_acquire | Partial | See [Atomics](#atomics) |
atomic_max_acqrel | Partial | See [Atomics](#atomics) |
atomic_max_rel | Partial | See [Atomics](#atomics) |
atomic_max_release | Partial | See [Atomics](#atomics) |
atomic_max_relaxed | Partial | See [Atomics](#atomics) |
atomic_min | Partial | See [Atomics](#atomics) |
atomic_min_acq | Partial | See [Atomics](#atomics) |
atomic_min_seqcst | Partial | See [Atomics](#atomics) |
atomic_min_acquire | Partial | See [Atomics](#atomics) |
atomic_min_acqrel | Partial | See [Atomics](#atomics) |
atomic_min_rel | Partial | See [Atomics](#atomics) |
atomic_min_release | Partial | See [Atomics](#atomics) |
atomic_min_relaxed | Partial | See [Atomics](#atomics) |
atomic_nand | Partial | See [Atomics](#atomics) |
atomic_nand_acq | Partial | See [Atomics](#atomics) |
atomic_nand_seqcst | Partial | See [Atomics](#atomics) |
atomic_nand_acquire | Partial | See [Atomics](#atomics) |
atomic_nand_acqrel | Partial | See [Atomics](#atomics) |
atomic_nand_rel | Partial | See [Atomics](#atomics) |
atomic_nand_release | Partial | See [Atomics](#atomics) |
atomic_nand_relaxed | Partial | See [Atomics](#atomics) |
atomic_or | Partial | See [Atomics](#atomics) |
atomic_or_acq | Partial | See [Atomics](#atomics) |
atomic_or_seqcst | Partial | See [Atomics](#atomics) |
atomic_or_acquire | Partial | See [Atomics](#atomics) |
atomic_or_acqrel | Partial | See [Atomics](#atomics) |
atomic_or_rel | Partial | See [Atomics](#atomics) |
atomic_or_release | Partial | See [Atomics](#atomics) |
atomic_or_relaxed | Partial | See [Atomics](#atomics) |
atomic_singlethreadfence | Partial | See [Atomics](#atomics) |
atomic_singlethreadfence_acq | Partial | See [Atomics](#atomics) |
atomic_singlethreadfence_seqcst | Partial | See [Atomics](#atomics) |
atomic_singlethreadfence_acquire | Partial | See [Atomics](#atomics) |
atomic_singlethreadfence_acqrel | Partial | See [Atomics](#atomics) |
atomic_singlethreadfence_rel | Partial | See [Atomics](#atomics) |
atomic_store | Partial | See [Atomics](#atomics) |
atomic_store_rel | Partial | See [Atomics](#atomics) |
atomic_singlethreadfence_release | Partial | See [Atomics](#atomics) |
atomic_store_seqcst | Partial | See [Atomics](#atomics) |
atomic_store_release | Partial | See [Atomics](#atomics) |
atomic_store_relaxed | Partial | See [Atomics](#atomics) |
atomic_store_unordered | Partial | See [Atomics](#atomics) |
atomic_umax | Partial | See [Atomics](#atomics) |
atomic_umax_acq | Partial | See [Atomics](#atomics) |
atomic_umax_seqcst | Partial | See [Atomics](#atomics) |
atomic_umax_acquire | Partial | See [Atomics](#atomics) |
atomic_umax_acqrel | Partial | See [Atomics](#atomics) |
atomic_umax_rel | Partial | See [Atomics](#atomics) |
atomic_umax_release | Partial | See [Atomics](#atomics) |
atomic_umax_relaxed | Partial | See [Atomics](#atomics) |
atomic_umin | Partial | See [Atomics](#atomics) |
atomic_umin_acq | Partial | See [Atomics](#atomics) |
atomic_umin_seqcst | Partial | See [Atomics](#atomics) |
atomic_umin_acquire | Partial | See [Atomics](#atomics) |
atomic_umin_acqrel | Partial | See [Atomics](#atomics) |
atomic_umin_rel | Partial | See [Atomics](#atomics) |
atomic_umin_release | Partial | See [Atomics](#atomics) |
atomic_umin_relaxed | Partial | See [Atomics](#atomics) |
atomic_xadd | Partial | See [Atomics](#atomics) |
atomic_xadd_acq | Partial | See [Atomics](#atomics) |
atomic_xadd_seqcst | Partial | See [Atomics](#atomics) |
atomic_xadd_acquire | Partial | See [Atomics](#atomics) |
atomic_xadd_acqrel | Partial | See [Atomics](#atomics) |
atomic_xadd_rel | Partial | See [Atomics](#atomics) |
atomic_xadd_release | Partial | See [Atomics](#atomics) |
atomic_xadd_relaxed | Partial | See [Atomics](#atomics) |
atomic_xchg | Partial | See [Atomics](#atomics) |
atomic_xchg_acq | Partial | See [Atomics](#atomics) |
atomic_xchg_seqcst | Partial | See [Atomics](#atomics) |
atomic_xchg_acquire | Partial | See [Atomics](#atomics) |
atomic_xchg_acqrel | Partial | See [Atomics](#atomics) |
atomic_xchg_rel | Partial | See [Atomics](#atomics) |
atomic_xchg_release | Partial | See [Atomics](#atomics) |
atomic_xchg_relaxed | Partial | See [Atomics](#atomics) |
atomic_xor | Partial | See [Atomics](#atomics) |
atomic_xor_acq | Partial | See [Atomics](#atomics) |
atomic_xor_seqcst | Partial | See [Atomics](#atomics) |
atomic_xor_acquire | Partial | See [Atomics](#atomics) |
atomic_xor_acqrel | Partial | See [Atomics](#atomics) |
atomic_xor_rel | Partial | See [Atomics](#atomics) |
atomic_xor_release | Partial | See [Atomics](#atomics) |
atomic_xor_relaxed | Partial | See [Atomics](#atomics) |
atomic_xsub | Partial | See [Atomics](#atomics) |
atomic_xsub_acq | Partial | See [Atomics](#atomics) |
atomic_xsub_seqcst | Partial | See [Atomics](#atomics) |
atomic_xsub_acquire | Partial | See [Atomics](#atomics) |
atomic_xsub_acqrel | Partial | See [Atomics](#atomics) |
atomic_xsub_rel | Partial | See [Atomics](#atomics) |
atomic_xsub_release | Partial | See [Atomics](#atomics) |
atomic_xsub_relaxed | Partial | See [Atomics](#atomics) |
blackbox | Yes | |
bitreverse | Yes | |
Expand Down
82 changes: 60 additions & 22 deletions tests/kani/Intrinsics/Atomic/Unstable/AtomicCxchg/main.rs
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,15 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT

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

#![feature(core_intrinsics)]
use std::intrinsics::{
atomic_cxchg_acqrel_acquire, atomic_cxchg_acqrel_relaxed, atomic_cxchg_acquire_acquire,
atomic_cxchg_acquire_relaxed, atomic_cxchg_relaxed_relaxed, atomic_cxchg_release_relaxed,
atomic_cxchg_acqrel_acquire, atomic_cxchg_acqrel_relaxed, atomic_cxchg_acqrel_seqcst,
atomic_cxchg_acquire_acquire, atomic_cxchg_acquire_relaxed, atomic_cxchg_acquire_seqcst,
atomic_cxchg_relaxed_acquire, atomic_cxchg_relaxed_relaxed, atomic_cxchg_relaxed_seqcst,
atomic_cxchg_release_acquire, atomic_cxchg_release_relaxed, atomic_cxchg_release_seqcst,
atomic_cxchg_seqcst_acquire, atomic_cxchg_seqcst_relaxed, atomic_cxchg_seqcst_seqcst,
};

Expand All @@ -22,6 +24,12 @@ fn main() {
let mut a7 = 0 as u8;
let mut a8 = 0 as u8;
let mut a9 = 0 as u8;
let mut a10 = 0 as u8;
let mut a11 = 0 as u8;
let mut a12 = 0 as u8;
let mut a13 = 0 as u8;
let mut a14 = 0 as u8;
let mut a15 = 0 as u8;

let ptr_a1: *mut u8 = &mut a1;
let ptr_a2: *mut u8 = &mut a2;
Expand All @@ -32,21 +40,33 @@ fn main() {
let ptr_a7: *mut u8 = &mut a7;
let ptr_a8: *mut u8 = &mut a8;
let ptr_a9: *mut u8 = &mut a9;
let ptr_a10: *mut u8 = &mut a10;
let ptr_a11: *mut u8 = &mut a11;
let ptr_a12: *mut u8 = &mut a12;
let ptr_a13: *mut u8 = &mut a13;
let ptr_a14: *mut u8 = &mut a14;
let ptr_a15: *mut u8 = &mut a15;

unsafe {
// Stores a value if the current value is the same as the old value
// Returns (val, ok) where
// * val: the old value
// * ok: bool indicating whether the operation was successful or not
let x1 = atomic_cxchg_seqcst_seqcst(ptr_a1, 0, 1);
let x2 = atomic_cxchg_acquire_acquire(ptr_a2, 0, 1);
let x3 = atomic_cxchg_acquire_relaxed(ptr_a3, 0, 1);
let x4 = atomic_cxchg_acqrel_acquire(ptr_a4, 0, 1);
let x5 = atomic_cxchg_acqrel_relaxed(ptr_a5, 0, 1);
let x6 = atomic_cxchg_seqcst_acquire(ptr_a6, 0, 1);
let x7 = atomic_cxchg_seqcst_relaxed(ptr_a7, 0, 1);
let x8 = atomic_cxchg_release_relaxed(ptr_a8, 0, 1);
let x9 = atomic_cxchg_relaxed_relaxed(ptr_a9, 0, 1);
let x1 = atomic_cxchg_acqrel_acquire(ptr_a1, 0, 1);
let x2 = atomic_cxchg_acqrel_relaxed(ptr_a2, 0, 1);
let x3 = atomic_cxchg_acqrel_seqcst(ptr_a3, 0, 1);
let x4 = atomic_cxchg_acquire_acquire(ptr_a4, 0, 1);
let x5 = atomic_cxchg_acquire_relaxed(ptr_a5, 0, 1);
let x6 = atomic_cxchg_acquire_seqcst(ptr_a6, 0, 1);
let x7 = atomic_cxchg_relaxed_acquire(ptr_a7, 0, 1);
let x8 = atomic_cxchg_relaxed_relaxed(ptr_a8, 0, 1);
let x9 = atomic_cxchg_relaxed_seqcst(ptr_a9, 0, 1);
let x10 = atomic_cxchg_release_acquire(ptr_a10, 0, 1);
let x11 = atomic_cxchg_release_relaxed(ptr_a11, 0, 1);
let x12 = atomic_cxchg_release_seqcst(ptr_a12, 0, 1);
let x13 = atomic_cxchg_seqcst_acquire(ptr_a13, 0, 1);
let x14 = atomic_cxchg_seqcst_relaxed(ptr_a14, 0, 1);
let x15 = atomic_cxchg_seqcst_seqcst(ptr_a15, 0, 1);

assert!(x1 == (0, true));
assert!(x2 == (0, true));
Expand All @@ -57,16 +77,28 @@ fn main() {
assert!(x7 == (0, true));
assert!(x8 == (0, true));
assert!(x9 == (0, true));
assert!(x10 == (0, true));
assert!(x11 == (0, true));
assert!(x12 == (0, true));
assert!(x13 == (0, true));
assert!(x14 == (0, true));
assert!(x15 == (0, true));

let y1 = atomic_cxchg_seqcst_seqcst(ptr_a1, 1, 1);
let y2 = atomic_cxchg_acquire_acquire(ptr_a2, 1, 1);
let y3 = atomic_cxchg_acqrel_relaxed(ptr_a3, 1, 1);
let y4 = atomic_cxchg_acqrel_acquire(ptr_a4, 1, 1);
let y5 = atomic_cxchg_acqrel_relaxed(ptr_a5, 1, 1);
let y6 = atomic_cxchg_seqcst_acquire(ptr_a6, 1, 1);
let y7 = atomic_cxchg_seqcst_relaxed(ptr_a7, 1, 1);
let y8 = atomic_cxchg_release_relaxed(ptr_a8, 1, 1);
let y9 = atomic_cxchg_relaxed_relaxed(ptr_a9, 1, 1);
let y1 = atomic_cxchg_acqrel_acquire(ptr_a1, 1, 1);
let y2 = atomic_cxchg_acqrel_relaxed(ptr_a2, 1, 1);
let y3 = atomic_cxchg_acqrel_seqcst(ptr_a3, 1, 1);
let y4 = atomic_cxchg_acquire_acquire(ptr_a4, 1, 1);
let y5 = atomic_cxchg_acquire_relaxed(ptr_a5, 1, 1);
let y6 = atomic_cxchg_acquire_seqcst(ptr_a6, 1, 1);
let y7 = atomic_cxchg_relaxed_acquire(ptr_a7, 1, 1);
let y8 = atomic_cxchg_relaxed_relaxed(ptr_a8, 1, 1);
let y9 = atomic_cxchg_relaxed_seqcst(ptr_a9, 1, 1);
let y10 = atomic_cxchg_release_acquire(ptr_a10, 1, 1);
let y11 = atomic_cxchg_release_relaxed(ptr_a11, 1, 1);
let y12 = atomic_cxchg_release_seqcst(ptr_a12, 1, 1);
let y13 = atomic_cxchg_seqcst_acquire(ptr_a13, 1, 1);
let y14 = atomic_cxchg_seqcst_relaxed(ptr_a14, 1, 1);
let y15 = atomic_cxchg_seqcst_seqcst(ptr_a15, 1, 1);

assert!(y1 == (1, true));
assert!(y2 == (1, true));
Expand All @@ -77,5 +109,11 @@ fn main() {
assert!(y7 == (1, true));
assert!(y8 == (1, true));
assert!(y9 == (1, true));
assert!(y10 == (1, true));
assert!(y11 == (1, true));
assert!(y12 == (1, true));
assert!(y13 == (1, true));
assert!(y14 == (1, true));
assert!(y15 == (1, true));
}
}
Loading

0 comments on commit 4f59fda

Please sign in to comment.