Remove atomic fence support.

Author: Patrick-6

genmc-sys/src/lib.rs

@@ -203,7 +203,6 @@ mod ffi {
             memory_ordering: MemOrdering,
             store_event_type: StoreEventType,
         ) -> StoreResult;
-        fn handleFence(self: Pin<&mut MiriGenMCShim>, thread_id: i32, memory_ordering: MemOrdering);
 
         fn handleMalloc(
             self: Pin<&mut MiriGenMCShim>,

genmc-sys/src_cpp/MiriInterface.cpp

@@ -380,16 +380,6 @@ void MiriGenMCShim::handleThreadKill(ThreadId thread_id) {
 	return GenMCDriver::handleStore(std::move(wLab), oldValSetter);
 }
 
-void MiriGenMCShim::handleFence(ThreadId thread_id, MemOrdering ord)
-{
-	MIRI_LOG() << "Received fence operation from Miri with ordering " << ord << "\n";
-
-	auto pos = incPos(thread_id);
-
-	auto fLab = std::make_unique<FenceLabel>(pos, ord);
-	GenMCDriver::handleFence(std::move(fLab));
-}
-
 /**** Memory (de)allocation ****/
 
 auto MiriGenMCShim::handleMalloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uintptr_t

genmc-sys/src_cpp/MiriInterface.hpp

@@ -70,8 +70,6 @@ struct MiriGenMCShim : private GenMCDriver
 										  GenmcScalar value, GenmcScalar old_val,
 										  MemOrdering ord, StoreEventType store_event_type);
 
-	void handleFence(ThreadId thread_id, MemOrdering ord);
-
 	/**** Memory (de)allocation ****/
 
 	uintptr_t handleMalloc(ThreadId thread_id, uint64_t size, uint64_t alignment);

src/concurrency/genmc/mapping.rs

@@ -1,6 +1,6 @@
 use genmc_sys::{MemOrdering, RMWBinOp};
 
-use crate::{AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd};
+use crate::{AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd};
 
 impl AtomicReadOrd {
     pub(super) fn convert(self) -> MemOrdering {
@@ -22,17 +22,6 @@ impl AtomicWriteOrd {
     }
 }
 
-impl AtomicFenceOrd {
-    pub(super) fn convert(self) -> MemOrdering {
-        match self {
-            AtomicFenceOrd::Acquire => MemOrdering::Acquire,
-            AtomicFenceOrd::Release => MemOrdering::Release,
-            AtomicFenceOrd::AcqRel => MemOrdering::AcquireRelease,
-            AtomicFenceOrd::SeqCst => MemOrdering::SequentiallyConsistent,
-        }
-    }
-}
-
 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.

src/concurrency/genmc/mod.rs

@@ -199,24 +199,10 @@ impl GenmcCtx {
 
     pub(crate) fn atomic_fence<'tcx>(
         &self,
-        machine: &MiriMachine<'tcx>,
-        ordering: AtomicFenceOrd,
+        _machine: &MiriMachine<'tcx>,
+        _ordering: AtomicFenceOrd,
     ) -> InterpResult<'tcx> {
-        assert!(!self.allow_data_races.get()); // TODO GENMC: handle this properly
-        info!("GenMC: atomic_fence with ordering: {ordering:?}");
-
-        let ordering = ordering.convert();
-
-        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 mut mc = self.handle.borrow_mut();
-        let pinned_mc = mc.as_mut();
-        pinned_mc.handleFence(genmc_tid.0, ordering);
-
-        // TODO GENMC: can this operation ever fail?
-        interp_ok(())
+        throw_unsup_format!("FIXME(genmc): Add support for atomic fences.")
     }
 
     /// Inform GenMC about an atomic read-modify-write operation.