Remove compare_exchange support.

Author: Patrick-6

genmc-sys/src/lib.rs

@@ -77,13 +77,6 @@ mod ffi {
         UMin = 10,
     }
 
-    // TODO GENMC: do these have to be shared with the Rust side?
-    #[derive(Debug)]
-    enum StoreEventType {
-        Normal,
-        CompareExchange,
-    }
-
     #[derive(Debug, Clone, Copy)]
     struct GenmcScalar {
         value: u64,
@@ -92,15 +85,6 @@ mod ffi {
 
     /**** \/ Result & Error types \/ ****/
 
-    #[must_use]
-    #[derive(Debug)]
-    struct CompareExchangeResult {
-        old_value: GenmcScalar, // TODO GENMC: handle bigger values
-        is_success: bool,
-        isCoMaxWrite: bool,
-        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
-    }
-
     #[must_use]
     #[derive(Debug)]
     struct LoadResult {
@@ -158,15 +142,13 @@ mod ffi {
 
         type MemOrdering;
         type RMWBinOp;
-        type StoreEventType;
 
         // Types for Scheduling queries:
         type ActionKind;
 
         // Result / Error types:
         type LoadResult;
         type StoreResult;
-        type CompareExchangeResult;
         type VerificationError;
 
         type GenmcScalar;
@@ -188,19 +170,6 @@ mod ffi {
             memory_ordering: MemOrdering,
             old_value: GenmcScalar,
         ) -> LoadResult;
-        fn handleCompareExchange(
-            self: Pin<&mut MiriGenMCShim>,
-            thread_id: i32,
-            address: u64,
-            size: u64,
-            expected_value: GenmcScalar,
-            new_value: GenmcScalar,
-            old_value: GenmcScalar,
-            success_load_ordering: MemOrdering,
-            success_store_ordering: MemOrdering,
-            fail_load_ordering: MemOrdering,
-            can_fail_spuriously: bool,
-        ) -> CompareExchangeResult;
         fn handleStore(
             self: Pin<&mut MiriGenMCShim>,
             thread_id: i32,
@@ -209,7 +178,6 @@ mod ffi {
             value: GenmcScalar,
             old_value: GenmcScalar,
             memory_ordering: MemOrdering,
-            store_event_type: StoreEventType,
         ) -> StoreResult;
 
         fn handleMalloc(

genmc-sys/src_cpp/MiriInterface.cpp

@@ -218,7 +218,7 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 											 MemOrdering ord, GenmcScalar old_val) -> LoadResult
 {
 	auto pos = incPos(thread_id);
-	
+
 	auto loc = SAddr(address);
 	auto aSize = ASize(size);
 	auto type = AType::Unsigned; // TODO GENMC: get correct type from Miri
@@ -231,49 +231,9 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 	return result;
 }
 
-[[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,
-	MemOrdering success_store_ordering, MemOrdering fail_load_ordering,
-	bool can_fail_spuriously) -> CompareExchangeResult
-{
-	auto pos = incPos(thread_id);
-
-	auto loc = SAddr(address);
-	auto aSize = ASize(size);
-	auto type = AType::Unsigned;
-
-	auto expectedVal = expected_value.toSVal();
-	auto newVal = new_value.toSVal();
-
-	// FIXME(GenMC): properly handle failure memory ordering.
-
-	auto newLab = std::make_unique<CasReadLabel>(pos, success_load_ordering, loc, aSize, type,
-												 expectedVal, newVal);
-
-	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 CompareExchangeResult::fromError(*error);
-	}
-
-	auto oldVal = result.scalar.toSVal();
-	if (oldVal != expectedVal)
-		return CompareExchangeResult::failure(oldVal);
-
-	auto store_result = handleStore(thread_id, address, size, GenmcScalar(newVal), old_val,
-									success_store_ordering, StoreEventType::CompareExchange);
-
-	if (store_result.is_error())
-		return CompareExchangeResult::fromError(*store_result.error);
-	return CompareExchangeResult::success(oldVal, store_result.isCoMaxWrite);
-}
-
 [[nodiscard]] auto MiriGenMCShim::handleStore(ThreadId thread_id, uint64_t address, uint64_t size,
 											  GenmcScalar value, GenmcScalar old_val,
-											  MemOrdering ord, StoreEventType store_event_type)
+											  MemOrdering ord)
 	-> StoreResult
 {
 	auto pos = incPos(thread_id);
@@ -282,21 +242,9 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 	auto aSize = ASize(size);
 	auto type = AType::Unsigned; // TODO GENMC: get from Miri
 
-	// TODO GENMC: u128 support
 	auto val = value.toSVal();
 
-	std::unique_ptr<WriteLabel> wLab;
-	switch (store_event_type)
-	{
-	case StoreEventType::Normal:
-		wLab = std::make_unique<WriteLabel>(pos, ord, loc, aSize, type, val);
-		break;
-	case StoreEventType::CompareExchange:
-		wLab = std::make_unique<CasWriteLabel>(pos, ord, loc, aSize, type, val);
-		break;
-	default:
-		ERROR("Unsupported Store Event Type");
-	}
+	std::unique_ptr<WriteLabel> wLab = std::make_unique<WriteLabel>(pos, ord, loc, aSize, type, val);
 
 	auto oldValSetter = [this, old_val](SAddr loc)
 	{

genmc-sys/src_cpp/MiriInterface.hpp

@@ -55,15 +55,9 @@ struct MiriGenMCShim : private GenMCDriver
 	///////////////////
 	[[nodiscard]] LoadResult handleLoad(ThreadId thread_id, uint64_t address, uint64_t size,
 										MemOrdering ord, GenmcScalar old_val);
-	[[nodiscard]] CompareExchangeResult
-	handleCompareExchange(ThreadId thread_id, uint64_t address, uint64_t size,
-						  GenmcScalar expected_value, GenmcScalar new_value,
-						  GenmcScalar old_val, MemOrdering success_load_ordering,
-						  MemOrdering success_store_ordering, MemOrdering fail_load_ordering,
-						  bool can_fail_spuriously);
 	[[nodiscard]] StoreResult handleStore(ThreadId thread_id, uint64_t address, uint64_t size,
 										  GenmcScalar value, GenmcScalar old_val,
-										  MemOrdering ord, StoreEventType store_event_type);
+										  MemOrdering ord);
 
 	/**** Memory (de)allocation ****/
 

src/concurrency/genmc/mapping.rs

@@ -1,6 +1,6 @@
 use genmc_sys::MemOrdering;
 
-use crate::{AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd};
+use crate::{AtomicReadOrd, AtomicWriteOrd};
 
 impl AtomicReadOrd {
     pub(super) fn convert(self) -> MemOrdering {
@@ -21,18 +21,3 @@ impl AtomicWriteOrd {
         }
     }
 }
-
-impl AtomicRwOrd {
-    /// Split up the atomic success ordering of a read-modify-write operation into GenMC's representation.
-    /// Note that both returned orderings are currently identical, because this is what GenMC expects.
-    pub(super) fn to_genmc_memory_orderings(self) -> (MemOrdering, MemOrdering) {
-        match self {
-            AtomicRwOrd::Relaxed => (MemOrdering::Relaxed, MemOrdering::Relaxed),
-            AtomicRwOrd::Acquire => (MemOrdering::Acquire, MemOrdering::Acquire),
-            AtomicRwOrd::Release => (MemOrdering::Release, MemOrdering::Release),
-            AtomicRwOrd::AcqRel => (MemOrdering::AcquireRelease, MemOrdering::AcquireRelease),
-            AtomicRwOrd::SeqCst =>
-                (MemOrdering::SequentiallyConsistent, MemOrdering::SequentiallyConsistent),
-        }
-    }
-}

src/concurrency/genmc/mod.rs

@@ -3,18 +3,15 @@ use std::sync::Arc;
 
 use genmc_sys::{
     ActionKind, GENMC_GLOBAL_ADDRESSES_MASK, GenmcScalar, GenmcThreadId, MemOrdering,
-    MiriGenMCShim, StoreEventType, UniquePtr, createGenmcHandle,
+    MiriGenMCShim, UniquePtr, createGenmcHandle,
 };
 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 tracing::info;
 
 use self::global_allocations::{EvalContextExtPriv as _, GlobalAllocationHandler};
-use self::helper::{
-    genmc_scalar_to_scalar, option_scalar_to_genmc_scalar,
-    scalar_to_genmc_scalar,
-};
+use self::helper::{genmc_scalar_to_scalar, option_scalar_to_genmc_scalar, scalar_to_genmc_scalar};
 use self::thread_info_manager::ThreadInfoManager;
 use crate::concurrency::genmc::helper::split_access;
 use crate::{
@@ -214,7 +211,7 @@ impl GenmcCtx {
         _old_value: Scalar,
     ) -> InterpResult<'tcx, (Scalar, Option<Scalar>)> {
         assert!(!self.allow_data_races.get());
-        throw_unsup_format!("FIXME(genmc): Add support for atomic min/max.")
+        throw_unsup_format!("FIXME(genmc): Add support for atomic RMW.")
     }
 
     /// Inform GenMC about an atomic `min` or `max` operation.
@@ -253,69 +250,19 @@ impl GenmcCtx {
 
     pub(crate) fn atomic_compare_exchange<'tcx>(
         &self,
-        ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
-        address: Size,
-        size: Size,
-        expected_old_value: Scalar,
-        new_value: Scalar,
-        success: AtomicRwOrd,
-        fail: AtomicReadOrd,
-        can_fail_spuriously: bool,
+        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+        _address: Size,
+        _size: Size,
+        _expected_old_value: Scalar,
+        _new_value: Scalar,
+        _success: AtomicRwOrd,
+        _fail: AtomicReadOrd,
+        _can_fail_spuriously: bool,
         // 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, bool, bool)> {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
-
-        let machine = &ecx.machine;
-        let (success_load_ordering, success_store_ordering) = success.to_genmc_memory_orderings();
-        let fail_load_ordering = fail.convert();
-
-        info!(
-            "GenMC: atomic_compare_exchange, address: {address:?}, size: {size:?} (expect: {expected_old_value:?}, new: {new_value:?}, old_value: {old_value:?}, {success:?}, {fail:?}), can fail spuriously: {can_fail_spuriously}"
-        );
-        info!(
-            "GenMC: atomic_compare_exchange orderings: success: ({success_load_ordering:?}, {success_store_ordering:?}), failure load ordering: {fail_load_ordering:?}"
-        );
-
-        let thread_infos = self.thread_infos.borrow();
-        let curr_thread = machine.threads.active_thread();
-        let genmc_tid = thread_infos.get_info(curr_thread).genmc_tid;
-
-        let genmc_address = address.bytes();
-        let genmc_size = size.bytes();
-
-        let genmc_expected_value = scalar_to_genmc_scalar(ecx, expected_old_value)?;
-        let genmc_new_value = scalar_to_genmc_scalar(ecx, new_value)?;
-        let genmc_old_value = scalar_to_genmc_scalar(ecx, old_value)?;
-
-        let mut mc = self.handle.borrow_mut();
-        let pinned_mc = mc.as_mut().unwrap();
-        let cas_result = pinned_mc.handleCompareExchange(
-            genmc_tid.0,
-            genmc_address,
-            genmc_size,
-            genmc_expected_value,
-            genmc_new_value,
-            genmc_old_value,
-            success_load_ordering,
-            success_store_ordering,
-            fail_load_ordering,
-            can_fail_spuriously,
-        );
-
-        if let Some(error) = cas_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 return_scalar = genmc_scalar_to_scalar(ecx, cas_result.old_value, size)?;
-        info!(
-            "GenMC: atomic_compare_exchange: result: {cas_result:?}, returning scalar: {return_scalar:?}"
-        );
-        // The write can only be a co-maximal write if the CAS succeeded.
-        assert!(cas_result.is_success || !cas_result.isCoMaxWrite);
-        interp_ok((return_scalar, cas_result.isCoMaxWrite, cas_result.is_success))
+        assert!(!self.allow_data_races.get());
+        throw_unsup_format!("FIXME(genmc): Add support for atomic compare_exchange.")
     }
 
     /// Inform GenMC about a non-atomic memory load
@@ -671,7 +618,6 @@ impl GenmcCtx {
             genmc_value,
             genmc_old_value,
             memory_ordering,
-            StoreEventType::Normal,
         );
 
         if let Some(error) = store_result.error.as_ref() {