Remove Mutex handling, do cleanup.

Author: Patrick-6

genmc-sys/src/lib.rs

@@ -17,9 +17,6 @@ impl GenmcScalar {
     pub const UNINIT: Self = Self { value: 0, extra: 0, is_init: false };
     pub const DUMMY: Self = Self::from_u64(0xDEADBEEF);
 
-    pub const MUTEX_LOCKED_STATE: Self = Self::from_u64(1);
-    pub const MUTEX_UNLOCKED_STATE: Self = Self::from_u64(0);
-
     pub const fn from_u64(value: u64) -> Self {
         Self { value, extra: 0, is_init: true }
     }
@@ -91,7 +88,6 @@ mod ffi {
         Normal,
         ReadModifyWrite,
         CompareExchange,
-        MutexUnlockWrite,
     }
 
     #[derive(Debug, Clone, Copy)]
@@ -112,13 +108,6 @@ mod ffi {
         error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
     }
 
-    #[must_use]
-    #[derive(Debug)]
-    struct MutexLockResult {
-        is_lock_acquired: bool,
-        error: UniquePtr<CxxString>, // TODO GENMC: pass more error info here
-    }
-
     #[must_use]
     #[derive(Debug)]
     struct CompareExchangeResult {
@@ -195,7 +184,6 @@ mod ffi {
         type StoreResult;
         type ReadModifyWriteResult;
         type CompareExchangeResult;
-        type MutexLockResult;
         type VerificationError;
 
         type GenmcScalar;
@@ -267,29 +255,6 @@ mod ffi {
         fn handleThreadJoin(self: Pin<&mut MiriGenMCShim>, thread_id: i32, child_id: i32);
         fn handleThreadFinish(self: Pin<&mut MiriGenMCShim>, thread_id: i32, ret_val: u64);
 
-        /**** Blocking instructions ****/
-        fn handleUserBlock(self: Pin<&mut MiriGenMCShim>, thread_id: i32);
-
-        /**** Mutex handling ****/
-        fn handleMutexLock(
-            self: Pin<&mut MiriGenMCShim>,
-            thread_id: i32,
-            address: u64,
-            size: u64,
-        ) -> MutexLockResult;
-        fn handleMutexTryLock(
-            self: Pin<&mut MiriGenMCShim>,
-            thread_id: i32,
-            address: u64,
-            size: u64,
-        ) -> MutexLockResult;
-        fn handleMutexUnlock(
-            self: Pin<&mut MiriGenMCShim>,
-            thread_id: i32,
-            address: u64,
-            size: u64,
-        ) -> StoreResult;
-
         /**** Scheduling ****/
         fn scheduleNext(
             self: Pin<&mut MiriGenMCShim>,

genmc-sys/src_cpp/MiriInterface.cpp

@@ -224,15 +224,6 @@ void MiriGenMCShim::handleThreadFinish(ThreadId thread_id, uint64_t ret_val)
 	GenMCDriver::handleThreadFinish(std::move(eLab));
 }
 
-/**** Blocking instructions ****/
-
-void MiriGenMCShim::handleUserBlock(ThreadId thread_id)
-{
-	auto pos = incPos(thread_id);
-	auto bLab = UserBlockLabel::create(pos);
-	GenMCDriver::handleBlock(std::move(bLab));
-}
-
 /**** Memory access handling ****/
 
 [[nodiscard]] auto MiriGenMCShim::handleLoad(ThreadId thread_id, uint64_t address, uint64_t size,
@@ -365,9 +356,6 @@ void MiriGenMCShim::handleUserBlock(ThreadId thread_id)
 	case StoreEventType::CompareExchange:
 		wLab = std::make_unique<CasWriteLabel>(pos, ord, loc, aSize, type, val);
 		break;
-	case StoreEventType::MutexUnlockWrite:
-		wLab = UnlockWriteLabel::create(pos, ord, loc, aSize, AType::Signed, val);
-		break;
 	default:
 		ERROR("Unsupported Store Event Type");
 	}
@@ -423,94 +411,3 @@ void MiriGenMCShim::handleFree(ThreadId thread_id, uint64_t address, uint64_t si
 	auto dLab = std::make_unique<FreeLabel>(pos, addr, size);
 	GenMCDriver::handleFree(std::move(dLab));
 }
-
-/**** Mutex handling ****/
-
-auto MiriGenMCShim::handleMutexLock(ThreadId thread_id, uint64_t address, uint64_t size)
-	-> MutexLockResult
-{
-	// TODO GENMC: this needs to be identical even in multithreading
-	ModuleID::ID annot_id;
-	if (annotation_id.contains(address)) {
-		annot_id = annotation_id.at(address);
-	} else {
-		annot_id = annotation_id_counter++;
-		annotation_id.insert(std::make_pair(address, annot_id));
-	}
-	const auto aSize = ASize(size);
-	auto annot = std::move(Annotation(
-		AssumeType::Spinloop,
-		Annotation::ExprVP(NeExpr<AnnotID>::create(
-					   RegisterExpr<AnnotID>::create(aSize.getBits(), annot_id),
-					   ConcreteExpr<AnnotID>::create(aSize.getBits(), SVal(1)))
-					   .release())));
-
-	auto &currPos = globalInstructions[thread_id].event;
-	// auto rLab = LockCasReadLabel::create(++currPos, address, size);
-	auto rLab = LockCasReadLabel::create(++currPos, address, size, annot);
-
-	// Mutex starts out unlocked, so we always say the previous value is "unlocked".
-	auto oldValSetter = [this](SAddr loc) { this->handleOldVal(loc, SVal(0)); };
-	LoadResult loadResult = GenMCDriver::handleLoad(std::move(rLab), oldValSetter);
-	if (loadResult.is_error()) {
-		--currPos;
-		return MutexLockResult::fromError(*loadResult.error);
-	} else if (loadResult.is_read_opt) {
-		--currPos;
-		// TODO GENMC: is_read_opt == Mutex is acquired
-		// None	--> Someone else has lock, this thread will be rescheduled later (currently
-		// block) 0	--> Got the lock 1 	--> Someone else has lock, this thread will
-		// not be rescheduled later (block on Miri side)
-		return MutexLockResult(false);
-	}
-	// TODO GENMC(QUESTION): is the `isBlocked` even needed?
-	// if (!loadResult.has_value() || getCurThr().isBlocked())
-	//     return;
-
-	const bool is_lock_acquired = loadResult.value() == SVal(0);
-	if (is_lock_acquired) {
-		auto wLab = LockCasWriteLabel::create(++currPos, address, size);
-		StoreResult storeResult = GenMCDriver::handleStore(std::move(wLab), oldValSetter);
-		if (storeResult.is_error())
-			return MutexLockResult::fromError(*storeResult.error);
-
-	} else {
-		auto bLab = LockNotAcqBlockLabel::create(++currPos);
-		GenMCDriver::handleBlock(std::move(bLab));
-	}
-
-	return MutexLockResult(is_lock_acquired);
-}
-
-auto MiriGenMCShim::handleMutexTryLock(ThreadId thread_id, uint64_t address, uint64_t size)
-	-> MutexLockResult
-{
-	auto &currPos = globalInstructions[thread_id].event;
-	auto rLab = TrylockCasReadLabel::create(++currPos, address, size);
-	// Mutex starts out unlocked, so we always say the previous value is "unlocked".
-	auto oldValSetter = [this](SAddr loc) { this->handleOldVal(loc, SVal(0)); };
-	LoadResult loadResult = GenMCDriver::handleLoad(std::move(rLab), oldValSetter);
-	if (!loadResult.has_value()) {
-		--currPos;
-		// TODO GENMC: maybe use std move and make it take a unique_ptr<string> ?
-		return MutexLockResult::fromError(*loadResult.error);
-	}
-
-	const bool is_lock_acquired = loadResult.value() == SVal(0);
-	if (!is_lock_acquired)
-		return MutexLockResult(false); /* Lock already held. */
-
-	auto wLab = TrylockCasWriteLabel::create(++currPos, address, size);
-	StoreResult storeResult = GenMCDriver::handleStore(std::move(wLab), oldValSetter);
-	if (storeResult.is_error())
-		return MutexLockResult::fromError(*storeResult.error);
-
-	return MutexLockResult(true);
-}
-
-auto MiriGenMCShim::handleMutexUnlock(ThreadId thread_id, uint64_t address, uint64_t size)
-	-> StoreResult
-{
-	return handleStore(thread_id, address, size, SVal(0), SVal(0xDEADBEEF),
-			   MemOrdering::Release, StoreEventType::MutexUnlockWrite);
-}

genmc-sys/src_cpp/MiriInterface.hpp

@@ -28,22 +28,6 @@ enum class StoreEventType : uint8_t {
 	Normal,
 	ReadModifyWrite,
 	CompareExchange,
-	MutexUnlockWrite,
-};
-
-struct MutexLockResult {
-	bool is_lock_acquired;
-	std::unique_ptr<ModelCheckerError> error; // TODO GENMC: pass more error info here
-
-	MutexLockResult(bool is_lock_acquired) : is_lock_acquired(is_lock_acquired), error(nullptr)
-	{}
-
-	static auto fromError(std::string msg) -> MutexLockResult
-	{
-		auto res = MutexLockResult(false);
-		res.error = std::make_unique<ModelCheckerError>(msg);
-		return res;
-	}
 };
 
 // TODO GENMC: fix naming conventions
@@ -97,21 +81,8 @@ struct MiriGenMCShim : private GenMCDriver {
 	void handleThreadJoin(ThreadId thread_id, ThreadId child_id);
 	void handleThreadFinish(ThreadId thread_id, uint64_t ret_val);
 
-	/**** Blocking instructions ****/
-
-	void handleUserBlock(ThreadId thread_id);
-
-	/**** Mutex handling ****/
-	auto handleMutexLock(ThreadId thread_id, uint64_t address, uint64_t size)
-		-> MutexLockResult;
-	auto handleMutexTryLock(ThreadId thread_id, uint64_t address, uint64_t size)
-		-> MutexLockResult;
-	auto handleMutexUnlock(ThreadId thread_id, uint64_t address, uint64_t size) -> StoreResult;
-
 	/**** Scheduling queries ****/
 
-	// TODO GENMC: implement
-
 	auto scheduleNext(const int curr_thread_id, const ActionKind curr_thread_next_instr_kind)
 		-> int64_t;
 

src/concurrency/genmc/dummy.rs

@@ -254,26 +254,6 @@ impl GenmcCtx {
     }
 }
 
-/// Other functionality not directly related to event handling
-impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
-pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
-    fn check_genmc_intercept_function(
-        &mut self,
-        _instance: rustc_middle::ty::Instance<'tcx>,
-        _args: &[rustc_const_eval::interpret::FnArg<'tcx, crate::Provenance>],
-        _dest: &crate::PlaceTy<'tcx>,
-        _ret: Option<mir::BasicBlock>,
-    ) -> InterpResult<'tcx, bool> {
-        unreachable!()
-    }
-
-    /**** Scheduling functionality ****/
-
-    fn genmc_schedule_thread(&mut self) -> InterpResult<'tcx, ThreadId> {
-        unreachable!()
-    }
-}
-
 impl VisitProvenance for GenmcCtx {
     fn visit_provenance(&self, _visit: &mut VisitWith<'_>) {
         unreachable!()