Remove RMW support

Author: Patrick-6

genmc-sys/src/lib.rs

@@ -81,7 +81,6 @@ mod ffi {
     #[derive(Debug)]
     enum StoreEventType {
         Normal,
-        ReadModifyWrite,
         CompareExchange,
     }
 
@@ -93,15 +92,6 @@ mod ffi {
 
     /**** \/ Result & Error types \/ ****/
 
-    #[must_use]
-    #[derive(Debug)]
-    struct ReadModifyWriteResult {
-        old_value: GenmcScalar,
-        new_value: GenmcScalar,
-        isCoMaxWrite: bool,
-        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
-    }
-
     #[must_use]
     #[derive(Debug)]
     struct CompareExchangeResult {
@@ -176,7 +166,6 @@ mod ffi {
         // Result / Error types:
         type LoadResult;
         type StoreResult;
-        type ReadModifyWriteResult;
         type CompareExchangeResult;
         type VerificationError;
 
@@ -199,17 +188,6 @@ mod ffi {
             memory_ordering: MemOrdering,
             old_value: GenmcScalar,
         ) -> LoadResult;
-        fn handleReadModifyWrite(
-            self: Pin<&mut MiriGenMCShim>,
-            thread_id: i32,
-            address: u64,
-            size: u64,
-            load_ordering: MemOrdering,
-            store_ordering: MemOrdering,
-            rmw_op: RMWBinOp,
-            rhs_value: GenmcScalar,
-            old_value: GenmcScalar,
-        ) -> ReadModifyWriteResult;
         fn handleCompareExchange(
             self: Pin<&mut MiriGenMCShim>,
             thread_id: i32,

genmc-sys/src_cpp/MiriInterface.cpp

@@ -231,41 +231,6 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 	return result;
 }
 
-[[nodiscard]] auto MiriGenMCShim::handleReadModifyWrite(ThreadId thread_id, uint64_t address,
-														uint64_t size, MemOrdering loadOrd,
-														MemOrdering store_ordering, RMWBinOp rmw_op,
-														GenmcScalar rhs_value, GenmcScalar old_val)
-	-> ReadModifyWriteResult
-{
-	auto pos = incPos(thread_id);
-
-	auto loc = SAddr(address);
-	auto aSize = ASize(size);
-	auto type = AType::Unsigned;
-
-	auto rhsVal = rhs_value.toSVal();
-	auto newLab =
-		std::make_unique<FaiReadLabel>(pos, loadOrd, loc, aSize, type, rmw_op, rhsVal);
-
-	auto oldValSetter = [this, old_val](SAddr loc)
-	{ this->handleOldVal(loc, old_val); };
-	auto result = GenMCDriver::handleLoad(std::move(newLab), oldValSetter);
-	if (const auto *error = result.error.get())
-	{
-		return ReadModifyWriteResult::fromError(*error);
-	}
-
-	auto oldVal = result.scalar.toSVal(); // TODO GENMC: u128 handling
-	auto newVal = executeRMWBinOp(oldVal, rhsVal, size, rmw_op);
-
-	auto store_result = handleStore(thread_id, address, size, GenmcScalar(newVal), old_val,
-									store_ordering, StoreEventType::ReadModifyWrite);
-
-	if (store_result.is_error())
-		return ReadModifyWriteResult::fromError(*store_result.error.get());
-	return ReadModifyWriteResult(oldVal, newVal, store_result.isCoMaxWrite);
-}
-
 [[nodiscard]] auto MiriGenMCShim::handleCompareExchange(
 	ThreadId thread_id, uint64_t address, uint64_t size, GenmcScalar expected_value,
 	GenmcScalar new_value, GenmcScalar old_val, MemOrdering success_load_ordering,
@@ -326,9 +291,6 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 	case StoreEventType::Normal:
 		wLab = std::make_unique<WriteLabel>(pos, ord, loc, aSize, type, val);
 		break;
-	case StoreEventType::ReadModifyWrite:
-		wLab = std::make_unique<FaiWriteLabel>(pos, ord, loc, aSize, type, val);
-		break;
 	case StoreEventType::CompareExchange:
 		wLab = std::make_unique<CasWriteLabel>(pos, ord, loc, aSize, type, val);
 		break;

genmc-sys/src_cpp/MiriInterface.hpp

@@ -27,7 +27,6 @@ using ThreadId = int;
 enum class StoreEventType : uint8_t
 {
 	Normal,
-	ReadModifyWrite,
 	CompareExchange,
 };
 
@@ -56,10 +55,6 @@ struct MiriGenMCShim : private GenMCDriver
 	///////////////////
 	[[nodiscard]] LoadResult handleLoad(ThreadId thread_id, uint64_t address, uint64_t size,
 										MemOrdering ord, GenmcScalar old_val);
-	[[nodiscard]] ReadModifyWriteResult
-	handleReadModifyWrite(ThreadId thread_id, uint64_t address, uint64_t size,
-						  MemOrdering loadOrd, MemOrdering store_ordering, RMWBinOp rmw_op,
-						  GenmcScalar rhs_value, GenmcScalar old_val);
 	[[nodiscard]] CompareExchangeResult
 	handleCompareExchange(ThreadId thread_id, uint64_t address, uint64_t size,
 						  GenmcScalar expected_value, GenmcScalar new_value,

src/concurrency/genmc/helper.rs

@@ -46,17 +46,6 @@ pub fn split_access(address: Size, size: Size) -> impl Iterator<Item = (u64, u64
     start_chunks.chain(aligned_chunks).chain(end_chunks)
 }
 
-/// Like `scalar_to_genmc_scalar`, but returns an error if the scalar is not an integer
-pub fn rhs_scalar_to_genmc_scalar<'tcx>(
-    ecx: &MiriInterpCx<'tcx>,
-    scalar: Scalar,
-) -> InterpResult<'tcx, GenmcScalar> {
-    if matches!(scalar, Scalar::Ptr(..)) {
-        throw_unsup_format!("Right hand side of atomic operation cannot be a pointer");
-    }
-    scalar_to_genmc_scalar(ecx, scalar)
-}
-
 pub fn option_scalar_to_genmc_scalar<'tcx>(
     ecx: &MiriInterpCx<'tcx>,
     maybe_scalar: Option<Scalar>,

src/concurrency/genmc/mapping.rs

@@ -1,4 +1,4 @@
-use genmc_sys::{MemOrdering, RMWBinOp};
+use genmc_sys::MemOrdering;
 
 use crate::{AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd};
 
@@ -36,26 +36,3 @@ impl AtomicRwOrd {
         }
     }
 }
-
-pub(super) fn min_max_to_genmc_rmw_op(min: bool, is_signed: bool) -> RMWBinOp {
-    match (min, is_signed) {
-        (true, true) => RMWBinOp::Min, // TODO GENMC: is there a use for FMin? (Min, UMin, FMin)
-        (false, true) => RMWBinOp::Max,
-        (true, false) => RMWBinOp::UMin,
-        (false, false) => RMWBinOp::UMax,
-    }
-}
-
-pub(super) fn to_genmc_rmw_op(bin_op: rustc_middle::mir::BinOp, negate: bool) -> RMWBinOp {
-    match bin_op {
-        rustc_middle::mir::BinOp::Add => RMWBinOp::Add,
-        rustc_middle::mir::BinOp::Sub => RMWBinOp::Sub,
-        rustc_middle::mir::BinOp::BitOr if !negate => RMWBinOp::Or,
-        rustc_middle::mir::BinOp::BitXor if !negate => RMWBinOp::Xor,
-        rustc_middle::mir::BinOp::BitAnd if negate => RMWBinOp::Nand,
-        rustc_middle::mir::BinOp::BitAnd => RMWBinOp::And,
-        _ => {
-            panic!("unsupported atomic operation: bin_op: {bin_op:?}, negate: {negate}");
-        }
-    }
-}

src/concurrency/genmc/mod.rs

@@ -3,7 +3,7 @@ use std::sync::Arc;
 
 use genmc_sys::{
     ActionKind, GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, GenmcThreadId, MemOrdering,
-    MiriGenMCShim, RMWBinOp, StoreEventType, UniquePtr, createGenmcHandle,
+    MiriGenMCShim, StoreEventType, UniquePtr, createGenmcHandle,
 };
 use rustc_abi::{Align, Size};
 use rustc_const_eval::interpret::{AllocId, InterpCx, InterpResult, interp_ok};
@@ -12,10 +12,9 @@ use tracing::info;
 
 use self::global_allocations::{EvalContextExtPriv as _, GlobalAllocationHandler};
 use self::helper::{
-    genmc_scalar_to_scalar, option_scalar_to_genmc_scalar, rhs_scalar_to_genmc_scalar,
+    genmc_scalar_to_scalar, option_scalar_to_genmc_scalar,
     scalar_to_genmc_scalar,
 };
-use self::mapping::{min_max_to_genmc_rmw_op, to_genmc_rmw_op};
 use self::thread_info_manager::ThreadInfoManager;
 use crate::concurrency::genmc::helper::split_access;
 use crate::{
@@ -205,101 +204,51 @@ impl GenmcCtx {
     /// Returns `(old_val, Option<new_val>)`. `new_val` might not be the latest write in coherence order, which is indicated by `None`.
     pub(crate) fn atomic_rmw_op<'tcx>(
         &self,
-        ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-        address: Size,
-        size: Size,
-        ordering: AtomicRwOrd,
-        (rmw_op, not): (mir::BinOp, bool),
-        rhs_scalar: Scalar,
+        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+        _address: Size,
+        _size: Size,
+        _ordering: AtomicRwOrd,
+        (_rmw_op, _not): (mir::BinOp, bool),
+        _rhs_scalar: Scalar,
         // The value that we would get, if we were to do a non-atomic load here.
-        old_value: Scalar,
+        _old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
-        let (load_ordering, store_ordering) = ordering.to_genmc_memory_orderings();
-        let genmc_rmw_op = to_genmc_rmw_op(rmw_op, not);
-        tracing::info!(
-            "GenMC: atomic_rmw_op (op: {rmw_op:?}, not: {not}, genmc_rmw_op: {genmc_rmw_op:?}): rhs value: {rhs_scalar:?}, orderings ({load_ordering:?}, {store_ordering:?})"
-        );
-        let genmc_rhs_scalar = rhs_scalar_to_genmc_scalar(ecx, rhs_scalar)?;
-        let genmc_old_value = scalar_to_genmc_scalar(ecx, old_value)?;
-        self.atomic_rmw_op_impl(
-            ecx,
-            address,
-            size,
-            load_ordering,
-            store_ordering,
-            genmc_rmw_op,
-            genmc_rhs_scalar,
-            genmc_old_value,
-        )
+        assert!(!self.allow_data_races.get());
+        throw_unsup_format!("FIXME(genmc): Add support for atomic min/max.")
     }
 
     /// 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`.
     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,
+        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+        _address: Size,
+        _size: Size,
+        _ordering: AtomicRwOrd,
+        _min: bool,
+        _is_signed: bool,
+        _rhs_scalar: Scalar,
         // The value that we would get, if we were to do a non-atomic load here.
-        old_value: Scalar,
+        _old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
-        let (load_ordering, store_ordering) = ordering.to_genmc_memory_orderings();
-        let genmc_rmw_op = min_max_to_genmc_rmw_op(min, is_signed);
-        tracing::info!(
-            "GenMC: atomic_min_max_op (min: {min}, signed: {is_signed}, genmc_rmw_op: {genmc_rmw_op:?}): rhs value: {rhs_scalar:?}, orderings ({load_ordering:?}, {store_ordering:?})"
-        );
-        let genmc_rhs_scalar = rhs_scalar_to_genmc_scalar(ecx, rhs_scalar)?;
-        let genmc_old_value = scalar_to_genmc_scalar(ecx, old_value)?;
-        self.atomic_rmw_op_impl(
-            ecx,
-            address,
-            size,
-            load_ordering,
-            store_ordering,
-            genmc_rmw_op,
-            genmc_rhs_scalar,
-            genmc_old_value,
-        )
+        assert!(!self.allow_data_races.get());
+        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`.
     pub(crate) fn atomic_exchange<'tcx>(
         &self,
-        ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-        address: Size,
-        size: Size,
-        rhs_scalar: Scalar,
-        ordering: AtomicRwOrd,
+        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+        _address: Size,
+        _size: Size,
+        _rhs_scalar: Scalar,
+        _ordering: AtomicRwOrd,
         // The value that we would get, if we were to do a non-atomic load here.
-        old_value: Scalar,
+        _old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
-        // TODO GENMC: could maybe merge this with atomic_rmw?
-
-        let (load_ordering, store_ordering) = ordering.to_genmc_memory_orderings();
-        let genmc_rmw_op = RMWBinOp::Xchg;
-        tracing::info!(
-            "GenMC: atomic_exchange (op: {genmc_rmw_op:?}): new value: {rhs_scalar:?}, orderings ({load_ordering:?}, {store_ordering:?})"
-        );
-        let genmc_rhs_scalar = scalar_to_genmc_scalar(ecx, rhs_scalar)?;
-        let genmc_old_value = scalar_to_genmc_scalar(ecx, old_value)?;
-        self.atomic_rmw_op_impl(
-            ecx,
-            address,
-            size,
-            load_ordering,
-            store_ordering,
-            genmc_rmw_op,
-            genmc_rhs_scalar,
-            genmc_old_value,
-        )
+        assert!(!self.allow_data_races.get());
+        throw_unsup_format!("FIXME(genmc): Add support for atomic swap.")
     }
 
     pub(crate) fn atomic_compare_exchange<'tcx>(
@@ -734,64 +683,6 @@ impl GenmcCtx {
         interp_ok(store_result.isCoMaxWrite)
     }
 
-    fn atomic_rmw_op_impl<'tcx>(
-        &self,
-        ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-        address: Size,
-        size: Size,
-        load_ordering: MemOrdering,
-        store_ordering: MemOrdering,
-        genmc_rmw_op: RMWBinOp,
-        genmc_rhs_scalar: GenmcScalar,
-        genmc_old_value: GenmcScalar,
-    ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
-        assert!(
-            size.bytes() <= 8,
-            "TODO GENMC: no support for accesses larger than 8 bytes (got {} bytes)",
-            size.bytes()
-        );
-        let machine = &ecx.machine;
-        assert_ne!(0, size.bytes());
-        let thread_infos = self.thread_infos.borrow();
-        let curr_thread_id = machine.threads.active_thread();
-        let genmc_tid = thread_infos.get_info(curr_thread_id).genmc_tid;
-
-        let genmc_address = address.bytes();
-        let genmc_size = size.bytes();
-
-        info!(
-            "GenMC: atomic_rmw_op, thread: {curr_thread_id:?} ({genmc_tid:?}) (op: {genmc_rmw_op:?}, rhs value: {genmc_rhs_scalar:?}), address: {address:?}, size: {size:?}, orderings: ({load_ordering:?}, {store_ordering:?})",
-        );
-
-        let mut mc = self.handle.borrow_mut();
-        let pinned_mc = mc.as_mut();
-        let rmw_result = pinned_mc.handleReadModifyWrite(
-            genmc_tid.0,
-            genmc_address,
-            genmc_size,
-            load_ordering,
-            store_ordering,
-            genmc_rmw_op,
-            genmc_rhs_scalar,
-            genmc_old_value,
-        );
-
-        if let Some(error) = rmw_result.error.as_ref() {
-            let msg = error.to_string_lossy().to_string();
-            info!("GenMC: RMW operation returned an error: \"{msg}\"");
-            throw_ub_format!("{}", msg); // TODO GENMC: proper error handling: find correct error here
-        }
-
-        let old_value_scalar = genmc_scalar_to_scalar(ecx, rmw_result.old_value, size)?;
-
-        let new_value_scalar = if rmw_result.isCoMaxWrite {
-            Some(genmc_scalar_to_scalar(ecx, rmw_result.new_value, size)?)
-        } else {
-            None
-        };
-        interp_ok((old_value_scalar, new_value_scalar))
-    }
-
     /**** Scheduling functionality ****/
 
     pub fn schedule_thread<'tcx>(