@@ -358,30 +358,31 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
358358 *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
359359 " Mutex read value was neither 0 nor 1"
360360 );
361- const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
362- if (is_lock_acquired) {
363- const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
364- nullptr ,
365- inc_pos (thread_id),
366- old_val,
367- address,
368- size,
369- EventDeps ()
370- );
371- if (const auto * err = std::get_if<VerificationError>(&store_ret))
372- return MutexLockResultExt::from_error (format_error (*err));
373- // We don't update Miri's memory for this operation so we don't need to know if the store
374- // was the co-maximal store, but we still check that we at least get a boolean as the result
375- // of the store.
376- const auto * is_co_max = std::get_if<bool >(&store_ret);
377- ERROR_ON (!is_co_max, " Unimplemented: mutex_try_lock store returned unexpected result." );
378- } else {
361+ auto is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
362+ if (!is_lock_acquired) {
379363 // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
380364 // it. GenMC determines this based on the annotation we pass with the load further up in
381365 // this function, namely when that load will read a value other than `MUTEX_LOCKED`.
382366 this ->handle_assume_block (thread_id, AssumeType::Spinloop);
367+ return MutexLockResultExt::ok (false );
383368 }
384- return MutexLockResultExt::ok (is_lock_acquired);
369+
370+ const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
371+ nullptr ,
372+ inc_pos (thread_id),
373+ old_val,
374+ address,
375+ size,
376+ EventDeps ()
377+ );
378+ if (const auto * err = std::get_if<VerificationError>(&store_ret))
379+ return MutexLockResultExt::from_error (format_error (*err));
380+ // We don't update Miri's memory for this operation so we don't need to know if the store
381+ // was the co-maximal store, but we still check that we at least get a boolean as the result
382+ // of the store.
383+ const auto * is_co_max = std::get_if<bool >(&store_ret);
384+ ERROR_ON (!is_co_max, " Unimplemented: mutex_try_lock store returned unexpected result." );
385+ return MutexLockResultExt::ok (true );
385386}
386387
387388auto MiriGenmcShim::handle_mutex_try_lock (ThreadId thread_id, uint64_t address, uint64_t size)
0 commit comments