Skip to content

Commit 0dcc21b

Browse files
RalfJungRalfJung
authored
Merge pull request #4569 from RalfJung/atomic-rmw
atomics: unify handling min/max and the other RMWs
2 parents 3a16bbc + 1186db8 commit 0dcc21b

File tree

5 files changed

+83
-127
lines changed

5 files changed

+83
-127
lines changed

‎src/tools/miri/src/concurrency/data_race.rs‎

Lines changed: 23 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@ use super::vector_clock::{VClock, VTimestamp, VectorIdx};
5656
use super::weak_memory::EvalContextExt as _;
5757
use crate::concurrency::GlobalDataRaceHandler;
5858
use crate::diagnostics::RacingOp;
59+
use crate::intrinsics::AtomicRmwOp;
5960
use crate::*;
6061

6162
pub type AllocState = VClockAlloc;
@@ -778,9 +779,8 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
778779
&mut self,
779780
place: &MPlaceTy<'tcx>,
780781
rhs: &ImmTy<'tcx>,
781-
op: mir::BinOp,
782-
not: bool,
783-
atomic: AtomicRwOrd,
782+
atomic_op: AtomicRmwOp,
783+
ord: AtomicRwOrd,
784784
) -> InterpResult<'tcx, ImmTy<'tcx>> {
785785
let this = self.eval_context_mut();
786786
this.atomic_access_check(place, AtomicAccessType::Rmw)?;
@@ -793,8 +793,9 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
793793
this,
794794
place.ptr().addr(),
795795
place.layout.size,
796-
atomic,
797-
(op, not),
796+
place.layout.backend_repr.is_signed(),
797+
ord,
798+
atomic_op,
798799
rhs.to_scalar(),
799800
old.to_scalar(),
800801
)?;
@@ -804,13 +805,26 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
804805
return interp_ok(ImmTy::from_scalar(old_val, old.layout));
805806
}
806807

807-
let val = this.binary_op(op, &old, rhs)?;
808-
let val = if not { this.unary_op(mir::UnOp::Not, &val)? } else { val };
808+
let val = match atomic_op {
809+
AtomicRmwOp::MirOp { op, neg } => {
810+
let val = this.binary_op(op, &old, rhs)?;
811+
if neg { this.unary_op(mir::UnOp::Not, &val)? } else { val }
812+
}
813+
AtomicRmwOp::Max => {
814+
let lt = this.binary_op(mir::BinOp::Lt, &old, rhs)?.to_scalar().to_bool()?;
815+
if lt { rhs } else { &old }.clone()
816+
}
817+
AtomicRmwOp::Min => {
818+
let lt = this.binary_op(mir::BinOp::Lt, &old, rhs)?.to_scalar().to_bool()?;
819+
if lt { &old } else { rhs }.clone()
820+
}
821+
};
822+
809823
this.allow_data_races_mut(|this| this.write_immediate(*val, place))?;
810824

811-
this.validate_atomic_rmw(place, atomic)?;
825+
this.validate_atomic_rmw(place, ord)?;
812826

813-
this.buffered_atomic_rmw(val.to_scalar(), place, atomic, old.to_scalar())?;
827+
this.buffered_atomic_rmw(val.to_scalar(), place, ord, old.to_scalar())?;
814828
interp_ok(old)
815829
}
816830

@@ -852,59 +866,6 @@ pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
852866
interp_ok(old)
853867
}
854868

855-
/// Perform an conditional atomic exchange with a memory place and a new
856-
/// scalar value, the old value is returned.
857-
fn atomic_min_max_scalar(
858-
&mut self,
859-
place: &MPlaceTy<'tcx>,
860-
rhs: ImmTy<'tcx>,
861-
min: bool,
862-
atomic: AtomicRwOrd,
863-
) -> InterpResult<'tcx, ImmTy<'tcx>> {
864-
let this = self.eval_context_mut();
865-
this.atomic_access_check(place, AtomicAccessType::Rmw)?;
866-
867-
let old = this.allow_data_races_mut(|this| this.read_immediate(place))?;
868-
869-
// Inform GenMC about the atomic min/max operation.
870-
if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
871-
let (old_val, new_val) = genmc_ctx.atomic_min_max_op(
872-
this,
873-
place.ptr().addr(),
874-
place.layout.size,
875-
atomic,
876-
min,
877-
old.layout.backend_repr.is_signed(),
878-
rhs.to_scalar(),
879-
old.to_scalar(),
880-
)?;
881-
// The store might be the latest store in coherence order (determined by GenMC).
882-
// If it is, we need to update the value in Miri's memory:
883-
if let Some(new_val) = new_val {
884-
this.allow_data_races_mut(|this| this.write_scalar(new_val, place))?;
885-
}
886-
return interp_ok(ImmTy::from_scalar(old_val, old.layout));
887-
}
888-
889-
let lt = this.binary_op(mir::BinOp::Lt, &old, &rhs)?.to_scalar().to_bool()?;
890-
891-
#[rustfmt::skip] // rustfmt makes this unreadable
892-
let new_val = if min {
893-
if lt { &old } else { &rhs }
894-
} else {
895-
if lt { &rhs } else { &old }
896-
};
897-
898-
this.allow_data_races_mut(|this| this.write_immediate(**new_val, place))?;
899-
900-
this.validate_atomic_rmw(place, atomic)?;
901-
902-
this.buffered_atomic_rmw(new_val.to_scalar(), place, atomic, old.to_scalar())?;
903-
904-
// Return the old value.
905-
interp_ok(old)
906-
}
907-
908869
/// Perform an atomic compare and exchange at a given memory location.
909870
/// On success an atomic RMW operation is performed and on failure
910871
/// only an atomic read occurs. If `can_fail_spuriously` is true,

‎src/tools/miri/src/concurrency/genmc/dummy.rs‎

Lines changed: 3 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
use rustc_abi::{Align, Size};
22
use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult};
3-
use rustc_middle::mir;
43

54
pub use self::run::run_genmc_mode;
5+
use crate::intrinsics::AtomicRmwOp;
66
use crate::{
77
AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriMachine, Scalar,
88
ThreadId, ThreadManager, VisitProvenance, VisitWith,
@@ -94,22 +94,9 @@ impl GenmcCtx {
9494
_ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
9595
_address: Size,
9696
_size: Size,
97-
_ordering: AtomicRwOrd,
98-
(_rmw_op, _not): (mir::BinOp, bool),
99-
_rhs_scalar: Scalar,
100-
_old_value: Scalar,
101-
) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
102-
unreachable!()
103-
}
104-
105-
pub(crate) fn atomic_min_max_op<'tcx>(
106-
&self,
107-
_ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
108-
_address: Size,
109-
_size: Size,
110-
_ordering: AtomicRwOrd,
111-
_min: bool,
11297
_is_signed: bool,
98+
_ordering: AtomicRwOrd,
99+
_atomic_op: AtomicRmwOp,
113100
_rhs_scalar: Scalar,
114101
_old_value: Scalar,
115102
) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {

‎src/tools/miri/src/concurrency/genmc/mod.rs‎

Lines changed: 4 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,15 @@ use genmc_sys::{
77
};
88
use rustc_abi::{Align, Size};
99
use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult, interp_ok};
10-
use rustc_middle::{mir, throw_machine_stop, throw_ub_format, throw_unsup_format};
10+
use rustc_middle::{throw_machine_stop, throw_ub_format, throw_unsup_format};
1111
// FIXME(genmc,tracing): Implement some work-around for enabling debug/trace level logging (currently disabled statically in rustc).
1212
use tracing::{debug, info};
1313

1414
use self::global_allocations::{EvalContextExt as _, GlobalAllocationHandler};
1515
use self::helper::{MAX_ACCESS_SIZE, genmc_scalar_to_scalar, scalar_to_genmc_scalar};
1616
use self::thread_id_map::ThreadIdMap;
1717
use crate::concurrency::genmc::helper::split_access;
18+
use crate::intrinsics::AtomicRmwOp;
1819
use crate::{
1920
AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriConfig,
2021
MiriMachine, MiriMemoryKind, Scalar, TerminationInfo, ThreadId, ThreadManager, VisitProvenance,
@@ -298,8 +299,9 @@ impl GenmcCtx {
298299
_ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
299300
_address: Size,
300301
_size: Size,
302+
_is_signed: bool,
301303
_ordering: AtomicRwOrd,
302-
(_rmw_op, _not): (mir::BinOp, bool),
304+
_atomic_op: AtomicRmwOp,
303305
_rhs_scalar: Scalar,
304306
_old_value: Scalar,
305307
) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
@@ -310,29 +312,6 @@ impl GenmcCtx {
310312
throw_unsup_format!("FIXME(genmc): Add support for atomic RMW.")
311313
}
312314

313-
/// Inform GenMC about an atomic `min` or `max` operation.
314-
///
315-
/// Returns `(old_val, Option<new_val>)`. `new_val` might not be the latest write in coherence order, which is indicated by `None`.
316-
///
317-
/// `old_value` is the value that a non-atomic load would read here, or `None` if the memory is uninitalized.
318-
pub(crate) fn atomic_min_max_op<'tcx>(
319-
&self,
320-
_ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
321-
_address: Size,
322-
_size: Size,
323-
_ordering: AtomicRwOrd,
324-
_min: bool,
325-
_is_signed: bool,
326-
_rhs_scalar: Scalar,
327-
_old_value: Scalar,
328-
) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
329-
assert!(
330-
!self.get_alloc_data_races(),
331-
"atomic min/max operation with data race checking disabled."
332-
);
333-
throw_unsup_format!("FIXME(genmc): Add support for atomic min/max.")
334-
}
335-
336315
/// Returns `(old_val, Option<new_val>)`. `new_val` might not be the latest write in coherence order, which is indicated by `None`.
337316
///
338317
/// `old_value` is the value that a non-atomic load would read here, or `None` if the memory is uninitalized.

‎src/tools/miri/src/intrinsics/atomic.rs‎

Lines changed: 50 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,13 @@ use rustc_middle::{mir, ty};
55
use super::check_intrinsic_arg_count;
66
use crate::*;
77

8-
pub enum AtomicOp {
9-
/// The `bool` indicates whether the result of the operation should be negated (`UnOp::Not`,
10-
/// must be a boolean-typed operation).
11-
MirOp(mir::BinOp, bool),
8+
pub enum AtomicRmwOp {
9+
MirOp {
10+
op: mir::BinOp,
11+
/// Indicates whether the result of the operation should be negated (`UnOp::Not`, must be a
12+
/// boolean-typed operation).
13+
neg: bool,
14+
},
1215
Max,
1316
Min,
1417
}
@@ -106,55 +109,85 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
106109

107110
"or" => {
108111
let ord = get_ord_at(2);
109-
this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::BitOr, false), rw_ord(ord))?;
112+
this.atomic_rmw_op(
113+
args,
114+
dest,
115+
AtomicRmwOp::MirOp { op: BinOp::BitOr, neg: false },
116+
rw_ord(ord),
117+
)?;
110118
}
111119
"xor" => {
112120
let ord = get_ord_at(2);
113-
this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::BitXor, false), rw_ord(ord))?;
121+
this.atomic_rmw_op(
122+
args,
123+
dest,
124+
AtomicRmwOp::MirOp { op: BinOp::BitXor, neg: false },
125+
rw_ord(ord),
126+
)?;
114127
}
115128
"and" => {
116129
let ord = get_ord_at(2);
117-
this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::BitAnd, false), rw_ord(ord))?;
130+
this.atomic_rmw_op(
131+
args,
132+
dest,
133+
AtomicRmwOp::MirOp { op: BinOp::BitAnd, neg: false },
134+
rw_ord(ord),
135+
)?;
118136
}
119137
"nand" => {
120138
let ord = get_ord_at(2);
121-
this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::BitAnd, true), rw_ord(ord))?;
139+
this.atomic_rmw_op(
140+
args,
141+
dest,
142+
AtomicRmwOp::MirOp { op: BinOp::BitAnd, neg: true },
143+
rw_ord(ord),
144+
)?;
122145
}
123146
"xadd" => {
124147
let ord = get_ord_at(2);
125-
this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::Add, false), rw_ord(ord))?;
148+
this.atomic_rmw_op(
149+
args,
150+
dest,
151+
AtomicRmwOp::MirOp { op: BinOp::Add, neg: false },
152+
rw_ord(ord),
153+
)?;
126154
}
127155
"xsub" => {
128156
let ord = get_ord_at(2);
129-
this.atomic_rmw_op(args, dest, AtomicOp::MirOp(BinOp::Sub, false), rw_ord(ord))?;
157+
this.atomic_rmw_op(
158+
args,
159+
dest,
160+
AtomicRmwOp::MirOp { op: BinOp::Sub, neg: false },
161+
rw_ord(ord),
162+
)?;
130163
}
131164
"min" => {
132165
let ord = get_ord_at(1);
133166
// Later we will use the type to indicate signed vs unsigned,
134167
// so make sure it matches the intrinsic name.
135168
assert!(matches!(args[1].layout.ty.kind(), ty::Int(_)));
136-
this.atomic_rmw_op(args, dest, AtomicOp::Min, rw_ord(ord))?;
169+
this.atomic_rmw_op(args, dest, AtomicRmwOp::Min, rw_ord(ord))?;
137170
}
138171
"umin" => {
139172
let ord = get_ord_at(1);
140173
// Later we will use the type to indicate signed vs unsigned,
141174
// so make sure it matches the intrinsic name.
142175
assert!(matches!(args[1].layout.ty.kind(), ty::Uint(_)));
143-
this.atomic_rmw_op(args, dest, AtomicOp::Min, rw_ord(ord))?;
176+
this.atomic_rmw_op(args, dest, AtomicRmwOp::Min, rw_ord(ord))?;
144177
}
145178
"max" => {
146179
let ord = get_ord_at(1);
147180
// Later we will use the type to indicate signed vs unsigned,
148181
// so make sure it matches the intrinsic name.
149182
assert!(matches!(args[1].layout.ty.kind(), ty::Int(_)));
150-
this.atomic_rmw_op(args, dest, AtomicOp::Max, rw_ord(ord))?;
183+
this.atomic_rmw_op(args, dest, AtomicRmwOp::Max, rw_ord(ord))?;
151184
}
152185
"umax" => {
153186
let ord = get_ord_at(1);
154187
// Later we will use the type to indicate signed vs unsigned,
155188
// so make sure it matches the intrinsic name.
156189
assert!(matches!(args[1].layout.ty.kind(), ty::Uint(_)));
157-
this.atomic_rmw_op(args, dest, AtomicOp::Max, rw_ord(ord))?;
190+
this.atomic_rmw_op(args, dest, AtomicRmwOp::Max, rw_ord(ord))?;
158191
}
159192

160193
_ => return interp_ok(EmulateItemResult::NotSupported),
@@ -222,8 +255,8 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
222255
&mut self,
223256
args: &[OpTy<'tcx>],
224257
dest: &MPlaceTy<'tcx>,
225-
atomic_op: AtomicOp,
226-
atomic: AtomicRwOrd,
258+
atomic_op: AtomicRmwOp,
259+
ord: AtomicRwOrd,
227260
) -> InterpResult<'tcx> {
228261
let this = self.eval_context_mut();
229262

@@ -240,14 +273,7 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
240273
);
241274
}
242275

243-
let old = match atomic_op {
244-
AtomicOp::Min =>
245-
this.atomic_min_max_scalar(&place, rhs, /* min */ true, atomic)?,
246-
AtomicOp::Max =>
247-
this.atomic_min_max_scalar(&place, rhs, /* min */ false, atomic)?,
248-
AtomicOp::MirOp(op, not) =>
249-
this.atomic_rmw_op_immediate(&place, &rhs, op, not, atomic)?,
250-
};
276+
let old = this.atomic_rmw_op_immediate(&place, &rhs, atomic_op, ord)?;
251277
this.write_immediate(*old, dest)?; // old value is returned
252278
interp_ok(())
253279
}

‎src/tools/miri/src/intrinsics/mod.rs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,9 @@
33
mod atomic;
44
mod simd;
55

6+
pub use self::atomic::AtomicRmwOp;
7+
8+
#[rustfmt::skip] // prevent `use` reordering
69
use std::ops::Neg;
710

811
use rand::Rng;

0 commit comments

Comments
 (0)