From b5deaa074381ed949b2fad9dd4eb49927d7b4149 Mon Sep 17 00:00:00 2001 From: Daniel Schwartz-Narbonne Date: Fri, 25 Jun 2021 15:52:16 -0400 Subject: [PATCH 1/2] Support atomic exchange primitives --- .../rustc_codegen_llvm/src/gotoc/intrinsic.rs | 5 +++ src/test/cbmc/Atomics/Stable/Exchange/main.rs | 38 +++++++++++++++++++ .../cbmc/Atomics/Unstable/AtomicXchg/main.rs | 37 ++++++++++++++++++ 3 files changed, 80 insertions(+) create mode 100644 src/test/cbmc/Atomics/Stable/Exchange/main.rs create mode 100644 src/test/cbmc/Atomics/Unstable/AtomicXchg/main.rs diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs index 88ee89a44a4e..1524cb736482 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs @@ -280,6 +280,11 @@ impl<'tcx> GotocCtx<'tcx> { "atomic_xadd_acqrel" => codegen_atomic_binop!(plus), "atomic_xadd_rel" => codegen_atomic_binop!(plus), "atomic_xadd_relaxed" => codegen_atomic_binop!(plus), + "atomic_xchg" + | "atomic_xchg_acq" + | "atomic_xchg_acqrel" + | "atomic_xchg_rel" + | "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc), "atomic_xor" => codegen_atomic_binop!(bitxor), "atomic_xor_acq" => codegen_atomic_binop!(bitxor), "atomic_xor_acqrel" => codegen_atomic_binop!(bitxor), diff --git a/src/test/cbmc/Atomics/Stable/Exchange/main.rs b/src/test/cbmc/Atomics/Stable/Exchange/main.rs new file mode 100644 index 000000000000..70e26fb1c7af --- /dev/null +++ b/src/test/cbmc/Atomics/Stable/Exchange/main.rs @@ -0,0 +1,38 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +use std::sync::atomic::{AtomicBool, Ordering}; + +fn main() { + // pub fn compare_exchange( + // &self, + // current: bool, + // new: bool, + // success: Ordering, + // failure: Ordering + // ) -> Result + // Stores a value into the bool if the current value is the same + // as the current value. + // The return value is a result indicating whether the new value + // was written and containing the previous value. On success this + // value is guaranteed to be equal to current. + let a1 = AtomicBool::new(true); + let a2 = AtomicBool::new(true); + let a3 = AtomicBool::new(true); + let a4 = AtomicBool::new(true); + let a5 = AtomicBool::new(true); + + + // swap is the stable version of atomic_xchg + // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#435 + assert!(a1.swap(false, Ordering::Acquire) == true); + assert!(a2.swap(false, Ordering::AcqRel) == true); + assert!(a3.swap(false, Ordering::Relaxed) == true); + assert!(a4.swap(false, Ordering::Release) == true); + assert!(a5.swap(false, Ordering::SeqCst) == true); + + assert!(a1.load(Ordering::Relaxed) == false); + assert!(a2.load(Ordering::Relaxed) == false); + assert!(a3.load(Ordering::Relaxed) == false); + assert!(a4.load(Ordering::Relaxed) == false); + assert!(a5.load(Ordering::Relaxed) == false); +} diff --git a/src/test/cbmc/Atomics/Unstable/AtomicXchg/main.rs b/src/test/cbmc/Atomics/Unstable/AtomicXchg/main.rs new file mode 100644 index 000000000000..92fc0fc752af --- /dev/null +++ b/src/test/cbmc/Atomics/Unstable/AtomicXchg/main.rs @@ -0,0 +1,37 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(core_intrinsics)] +use std::intrinsics::{ + atomic_xchg, atomic_xchg_acq, atomic_xchg_acqrel, atomic_xchg_rel, atomic_xchg_relaxed, +}; + +fn main() { + let mut a1 = 0 as u8; + let mut a2 = 0 as u8; + let mut a3 = 0 as u8; + let mut a4 = 0 as u8; + let mut a5 = 0 as u8; + + let ptr_a1: *mut u8 = &mut a1; + let ptr_a2: *mut u8 = &mut a2; + let ptr_a3: *mut u8 = &mut a3; + let ptr_a4: *mut u8 = &mut a4; + let ptr_a5: *mut u8 = &mut a5; + + 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 + assert!(atomic_xchg(ptr_a1, 1) == 0); + assert!(atomic_xchg(ptr_a1, 0) == 1); + assert!(atomic_xchg_acq(ptr_a2, 1) == 0); + assert!(atomic_xchg_acq(ptr_a2, 0) == 1); + assert!(atomic_xchg_acqrel(ptr_a3, 1) == 0); + assert!(atomic_xchg_acqrel(ptr_a3, 0) == 1); + assert!(atomic_xchg_rel(ptr_a4, 1) == 0); + assert!(atomic_xchg_rel(ptr_a4, 0) == 1); + assert!(atomic_xchg_relaxed(ptr_a5, 1) == 0); + assert!(atomic_xchg_relaxed(ptr_a5, 0) == 1); + } +} From 257c86a1caa5bcda357475d4dce73f8db01a63a0 Mon Sep 17 00:00:00 2001 From: Daniel Schwartz-Narbonne Date: Mon, 28 Jun 2021 14:12:24 -0400 Subject: [PATCH 2/2] PR comments --- compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs | 10 +++++----- src/test/cbmc/Atomics/Stable/Exchange/main.rs | 13 ------------- 2 files changed, 5 insertions(+), 18 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs index 1524cb736482..e78522335683 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs @@ -280,11 +280,11 @@ impl<'tcx> GotocCtx<'tcx> { "atomic_xadd_acqrel" => codegen_atomic_binop!(plus), "atomic_xadd_rel" => codegen_atomic_binop!(plus), "atomic_xadd_relaxed" => codegen_atomic_binop!(plus), - "atomic_xchg" - | "atomic_xchg_acq" - | "atomic_xchg_acqrel" - | "atomic_xchg_rel" - | "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_xchg" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_xchg_acq" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_xchg_acqrel" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_xchg_rel" => self.codegen_atomic_store(intrinsic, fargs, p, loc), + "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, p, loc), "atomic_xor" => codegen_atomic_binop!(bitxor), "atomic_xor_acq" => codegen_atomic_binop!(bitxor), "atomic_xor_acqrel" => codegen_atomic_binop!(bitxor), diff --git a/src/test/cbmc/Atomics/Stable/Exchange/main.rs b/src/test/cbmc/Atomics/Stable/Exchange/main.rs index 70e26fb1c7af..92755b04ea0d 100644 --- a/src/test/cbmc/Atomics/Stable/Exchange/main.rs +++ b/src/test/cbmc/Atomics/Stable/Exchange/main.rs @@ -3,25 +3,12 @@ use std::sync::atomic::{AtomicBool, Ordering}; fn main() { - // pub fn compare_exchange( - // &self, - // current: bool, - // new: bool, - // success: Ordering, - // failure: Ordering - // ) -> Result - // Stores a value into the bool if the current value is the same - // as the current value. - // The return value is a result indicating whether the new value - // was written and containing the previous value. On success this - // value is guaranteed to be equal to current. let a1 = AtomicBool::new(true); let a2 = AtomicBool::new(true); let a3 = AtomicBool::new(true); let a4 = AtomicBool::new(true); let a5 = AtomicBool::new(true); - // swap is the stable version of atomic_xchg // https://doc.rust-lang.org/src/core/sync/atomic.rs.html#435 assert!(a1.swap(false, Ordering::Acquire) == true);