Merge pull request #4569 from RalfJung/atomic-rmw

RalfJung · web-flow · commit 421cf190537c · 2025-09-05T10:46:21.000Z
atomics: unify handling min/max and the other RMWs
diff --git a/src/concurrency/data_race.rs b/src/concurrency/data_race.rs
@@ -56,6 +56,7 @@ use super::vector_clock::{VClock, VTimestamp, VectorIdx};
 use super::weak_memory::EvalContextExt as _;
 use crate::concurrency::GlobalDataRaceHandler;
 use crate::diagnostics::RacingOp;
+use crate::intrinsics::AtomicRmwOp;
 use crate::*;
 
 pub type AllocState = VClockAlloc;
@@ -778,9 +779,8 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
         &mut self,
         place: &MPlaceTy<'tcx>,
         rhs: &ImmTy<'tcx>,
-        op: mir::BinOp,
-        not: bool,
-        atomic: AtomicRwOrd,
+        atomic_op: AtomicRmwOp,
+        ord: AtomicRwOrd,
     ) -> InterpResult<'tcx, ImmTy<'tcx>> {
         let this = self.eval_context_mut();
         this.atomic_access_check(place, AtomicAccessType::Rmw)?;
@@ -793,8 +793,9 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
                 this,
                 place.ptr().addr(),
                 place.layout.size,
-                atomic,
-                (op, not),
+                place.layout.backend_repr.is_signed(),
+                ord,
+                atomic_op,
                 rhs.to_scalar(),
                 old.to_scalar(),
             )?;
@@ -804,13 +805,26 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
             return interp_ok(ImmTy::from_scalar(old_val, old.layout));
         }
 
-        let val = this.binary_op(op, &old, rhs)?;
-        let val = if not { this.unary_op(mir::UnOp::Not, &val)? } else { val };
+        let val = match atomic_op {
+            AtomicRmwOp::MirOp { op, neg } => {
+                let val = this.binary_op(op, &old, rhs)?;
+                if neg { this.unary_op(mir::UnOp::Not, &val)? } else { val }
+            }
+            AtomicRmwOp::Max => {
+                let lt = this.binary_op(mir::BinOp::Lt, &old, rhs)?.to_scalar().to_bool()?;
+                if lt { rhs } else { &old }.clone()
+            }
+            AtomicRmwOp::Min => {
+                let lt = this.binary_op(mir::BinOp::Lt, &old, rhs)?.to_scalar().to_bool()?;
+                if lt { &old } else { rhs }.clone()
+            }
+        };
+
         this.allow_data_races_mut(|this| this.write_immediate(*val, place))?;
 
-        this.validate_atomic_rmw(place, atomic)?;
+        this.validate_atomic_rmw(place, ord)?;
 
-        this.buffered_atomic_rmw(val.to_scalar(), place, atomic, old.to_scalar())?;
+        this.buffered_atomic_rmw(val.to_scalar(), place, ord, old.to_scalar())?;
         interp_ok(old)
     }
 
@@ -852,59 +866,6 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
         interp_ok(old)
     }
 
-    /// Perform an conditional atomic exchange with a memory place and a new
-    /// scalar value, the old value is returned.
-    fn atomic_min_max_scalar(
-        &mut self,
-        place: &MPlaceTy<'tcx>,
-        rhs: ImmTy<'tcx>,
-        min: bool,
-        atomic: AtomicRwOrd,
-    ) -> InterpResult<'tcx, ImmTy<'tcx>> {
-        let this = self.eval_context_mut();
-        this.atomic_access_check(place, AtomicAccessType::Rmw)?;
-
-        let old = this.allow_data_races_mut(|this| this.read_immediate(place))?;
-
-        // Inform GenMC about the atomic min/max operation.
-        if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
-            let (old_val, new_val) = genmc_ctx.atomic_min_max_op(
-                this,
-                place.ptr().addr(),
-                place.layout.size,
-                atomic,
-                min,
-                old.layout.backend_repr.is_signed(),
-                rhs.to_scalar(),
-                old.to_scalar(),
-            )?;
-            // The store might be the latest store in coherence order (determined by GenMC).
-            // If it is, we need to update the value in Miri's memory:
-            if let Some(new_val) = new_val {
-                this.allow_data_races_mut(|this| this.write_scalar(new_val, place))?;
-            }
-            return interp_ok(ImmTy::from_scalar(old_val, old.layout));
-        }
-
-        let lt = this.binary_op(mir::BinOp::Lt, &old, &rhs)?.to_scalar().to_bool()?;
-
-        #[rustfmt::skip] // rustfmt makes this unreadable
-        let new_val = if min {
-            if lt { &old } else { &rhs }
-        } else {
-            if lt { &rhs } else { &old }
-        };
-
-        this.allow_data_races_mut(|this| this.write_immediate(**new_val, place))?;
-
-        this.validate_atomic_rmw(place, atomic)?;
-
-        this.buffered_atomic_rmw(new_val.to_scalar(), place, atomic, old.to_scalar())?;
-
-        // Return the old value.
-        interp_ok(old)
-    }
-
     /// Perform an atomic compare and exchange at a given memory location.
     /// On success an atomic RMW operation is performed and on failure
     /// only an atomic read occurs. If `can_fail_spuriously` is true,
diff --git a/src/concurrency/genmc/dummy.rs b/src/concurrency/genmc/dummy.rs
@@ -1,8 +1,8 @@
 use rustc_abi::{Align, Size};
 use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult};
-use rustc_middle::mir;
 
 pub use self::run::run_genmc_mode;
+use crate::intrinsics::AtomicRmwOp;
 use crate::{
     AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriMachine, Scalar,
     ThreadId, ThreadManager, VisitProvenance, VisitWith,
@@ -94,22 +94,9 @@ impl GenmcCtx {
         _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
         _address: Size,
         _size: Size,
-        _ordering: AtomicRwOrd,
-        (_rmw_op, _not): (mir::BinOp, bool),
-        _rhs_scalar: Scalar,
-        _old_value: Scalar,
-    ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
-        unreachable!()
-    }
-
-    pub(crate) fn atomic_min_max_op<'tcx>(
-        &self,
-        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-        _address: Size,
-        _size: Size,
-        _ordering: AtomicRwOrd,
-        _min: bool,
         _is_signed: bool,
+        _ordering: AtomicRwOrd,
+        _atomic_op: AtomicRmwOp,
         _rhs_scalar: Scalar,
         _old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
diff --git a/src/concurrency/genmc/mod.rs b/src/concurrency/genmc/mod.rs
@@ -7,14 +7,15 @@ use genmc_sys::{
 };
 use rustc_abi::{Align, Size};
 use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult, interp_ok};
-use rustc_middle::{mir, throw_machine_stop, throw_ub_format, throw_unsup_format};
+use rustc_middle::{throw_machine_stop, throw_ub_format, throw_unsup_format};
 // FIXME(genmc,tracing): Implement some work-around for enabling debug/trace level logging (currently disabled statically in rustc).
 use tracing::{debug, info};
 
 use self::global_allocations::{EvalContextExt as _, GlobalAllocationHandler};
 use self::helper::{MAX_ACCESS_SIZE, genmc_scalar_to_scalar, scalar_to_genmc_scalar};
 use self::thread_id_map::ThreadIdMap;
 use crate::concurrency::genmc::helper::split_access;
+use crate::intrinsics::AtomicRmwOp;
 use crate::{
     AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriConfig,
     MiriMachine, MiriMemoryKind, Scalar, TerminationInfo, ThreadId, ThreadManager, VisitProvenance,
@@ -298,8 +299,9 @@ impl GenmcCtx {
         _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
         _address: Size,
         _size: Size,
+        _is_signed: bool,
         _ordering: AtomicRwOrd,
-        (_rmw_op, _not): (mir::BinOp, bool),
+        _atomic_op: AtomicRmwOp,
         _rhs_scalar: Scalar,
         _old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
@@ -310,29 +312,6 @@ impl GenmcCtx {
         throw_unsup_format!("FIXME(genmc): Add support for atomic RMW.")
     }
 
-    /// Inform GenMC about an atomic `min` or `max` operation.
-    ///
-    /// Returns `(old_val, Option<new_val>)`. `new_val` might not be the latest write in coherence order, which is indicated by `None`.
-    ///
-    /// `old_value` is the value that a non-atomic load would read here, or `None` if the memory is uninitalized.
-    pub(crate) fn atomic_min_max_op<'tcx>(
-        &self,
-        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-        _address: Size,
-        _size: Size,
-        _ordering: AtomicRwOrd,
-        _min: bool,
-        _is_signed: bool,
-        _rhs_scalar: Scalar,
-        _old_value: Scalar,
-    ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
-        assert!(
-            !self.get_alloc_data_races(),
-            "atomic min/max operation with data race checking disabled."
-        );
-        throw_unsup_format!("FIXME(genmc): Add support for atomic min/max.")
-    }
-
     /// Returns `(old_val, Option<new_val>)`. `new_val` might not be the latest write in coherence order, which is indicated by `None`.
     ///
     /// `old_value` is the value that a non-atomic load would read here, or `None` if the memory is uninitalized.
diff --git a/src/intrinsics/atomic.rs b/src/intrinsics/atomic.rs
@@ -5,10 +5,13 @@ use rustc_middle::{mir, ty};
 use super::check_intrinsic_arg_count;
 use crate::*;
 
-pub enum AtomicOp {
-    /// The `bool` indicates whether the result of the operation should be negated (`UnOp::Not`,
-    /// must be a boolean-typed operation).
-    MirOp(mir::BinOp, bool),
+pub enum AtomicRmwOp {
+    MirOp {
+        op: mir::BinOp,
+        /// Indicates whether the result of the operation should be negated (`UnOp::Not`, must be a
+        /// boolean-typed operation).
+        neg: bool,
+    },
     Max,
     Min,
 }
@@ -106,55 +109,85 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
 
             "or" => {
                 let ord = get_ord_at(2);
-                this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::BitOr, false), rw_ord(ord))?;
+                this.atomic_rmw_op(
+                    args,
+                    dest,
+                    AtomicRmwOp::MirOp { op: BinOp::BitOr, neg: false },
+                    rw_ord(ord),
+                )?;
             }
             "xor" => {
                 let ord = get_ord_at(2);
-                this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::BitXor, false), rw_ord(ord))?;
+                this.atomic_rmw_op(
+                    args,
+                    dest,
+                    AtomicRmwOp::MirOp { op: BinOp::BitXor, neg: false },
+                    rw_ord(ord),
+                )?;
             }
             "and" => {
                 let ord = get_ord_at(2);
-                this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::BitAnd, false), rw_ord(ord))?;
+                this.atomic_rmw_op(
+                    args,
+                    dest,
+                    AtomicRmwOp::MirOp { op: BinOp::BitAnd, neg: false },
+                    rw_ord(ord),
+                )?;
             }
             "nand" => {
                 let ord = get_ord_at(2);
-                this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::BitAnd, true), rw_ord(ord))?;
+                this.atomic_rmw_op(
+                    args,
+                    dest,
+                    AtomicRmwOp::MirOp { op: BinOp::BitAnd, neg: true },
+                    rw_ord(ord),
+                )?;
             }
             "xadd" => {
                 let ord = get_ord_at(2);
-                this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::Add, false), rw_ord(ord))?;
+                this.atomic_rmw_op(
+                    args,
+                    dest,
+                    AtomicRmwOp::MirOp { op: BinOp::Add, neg: false },
+                    rw_ord(ord),
+                )?;
             }
             "xsub" => {
                 let ord = get_ord_at(2);
-                this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::Sub, false), rw_ord(ord))?;
+                this.atomic_rmw_op(
+                    args,
+                    dest,
+                    AtomicRmwOp::MirOp { op: BinOp::Sub, neg: false },
+                    rw_ord(ord),
+                )?;
             }
             "min" => {
                 let ord = get_ord_at(1);
                 // Later we will use the type to indicate signed vs unsigned,
                 // so make sure it matches the intrinsic name.
                 assert!(matches!(args[1].layout.ty.kind(), ty::Int(_)));
-                this.atomic_rmw_op(args, dest, AtomicOp::Min, rw_ord(ord))?;
+                this.atomic_rmw_op(args, dest, AtomicRmwOp::Min, rw_ord(ord))?;
             }
             "umin" => {
                 let ord = get_ord_at(1);
                 // Later we will use the type to indicate signed vs unsigned,
                 // so make sure it matches the intrinsic name.
                 assert!(matches!(args[1].layout.ty.kind(), ty::Uint(_)));
-                this.atomic_rmw_op(args, dest, AtomicOp::Min, rw_ord(ord))?;
+                this.atomic_rmw_op(args, dest, AtomicRmwOp::Min, rw_ord(ord))?;
             }
             "max" => {
                 let ord = get_ord_at(1);
                 // Later we will use the type to indicate signed vs unsigned,
                 // so make sure it matches the intrinsic name.
                 assert!(matches!(args[1].layout.ty.kind(), ty::Int(_)));
-                this.atomic_rmw_op(args, dest, AtomicOp::Max, rw_ord(ord))?;
+                this.atomic_rmw_op(args, dest, AtomicRmwOp::Max, rw_ord(ord))?;
             }
             "umax" => {
                 let ord = get_ord_at(1);
                 // Later we will use the type to indicate signed vs unsigned,
                 // so make sure it matches the intrinsic name.
                 assert!(matches!(args[1].layout.ty.kind(), ty::Uint(_)));
-                this.atomic_rmw_op(args, dest, AtomicOp::Max, rw_ord(ord))?;
+                this.atomic_rmw_op(args, dest, AtomicRmwOp::Max, rw_ord(ord))?;
             }
 
             _ => return interp_ok(EmulateItemResult::NotSupported),
@@ -222,8 +255,8 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
         &mut self,
         args: &[OpTy<'tcx>],
         dest: &MPlaceTy<'tcx>,
-        atomic_op: AtomicOp,
-        atomic: AtomicRwOrd,
+        atomic_op: AtomicRmwOp,
+        ord: AtomicRwOrd,
     ) -> InterpResult<'tcx> {
         let this = self.eval_context_mut();
 
@@ -240,14 +273,7 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
             );
         }
 
-        let old = match atomic_op {
-            AtomicOp::Min =>
-                this.atomic_min_max_scalar(&place, rhs, /* min */ true, atomic)?,
-            AtomicOp::Max =>
-                this.atomic_min_max_scalar(&place, rhs, /* min */ false, atomic)?,
-            AtomicOp::MirOp(op, not) =>
-                this.atomic_rmw_op_immediate(&place, &rhs, op, not, atomic)?,
-        };
+        let old = this.atomic_rmw_op_immediate(&place, &rhs, atomic_op, ord)?;
         this.write_immediate(*old, dest)?; // old value is returned
         interp_ok(())
     }
diff --git a/src/intrinsics/mod.rs b/src/intrinsics/mod.rs
@@ -3,6 +3,9 @@
 mod atomic;
 mod simd;
 
+pub use self::atomic::AtomicRmwOp;
+
+#[rustfmt::skip] // prevent `use` reordering
 use std::ops::Neg;
 
 use rand::Rng;
