@@ -29,7 +29,9 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
2929 )
3030 ));
3131
32- // Mutex starts out unlocked, so we always say the previous value is "unlocked".
32+ // As usual, we need to tell GenMC which value was stored at this location before this atomic
33+ // access, if there previously was a non-atomic initializing access. We set the initial state of
34+ // a mutex to be "unlocked".
3335 const auto old_val = MUTEX_UNLOCKED;
3436 const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::LockCasRead>(
3537 thread_id,
@@ -84,7 +86,9 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
8486auto MiriGenmcShim::handle_mutex_try_lock (ThreadId thread_id, uint64_t address, uint64_t size)
8587 -> MutexLockResult {
8688 auto & currPos = threads_action_[thread_id].event ;
87- // Mutex starts out unlocked, so we always say the previous value is "unlocked".
89+ // As usual, we need to tell GenMC which value was stored at this location before this atomic
90+ // access, if there previously was a non-atomic initializing access. We set the initial state of
91+ // a mutex to be "unlocked".
8892 const auto old_val = MUTEX_UNLOCKED;
8993 const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
9094 ++currPos,
@@ -131,7 +135,9 @@ auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, ui
131135 const auto pos = inc_pos (thread_id);
132136 const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
133137 pos,
134- // Mutex starts out unlocked, so we always say the previous value is "unlocked".
138+ // As usual, we need to tell GenMC which value was stored at this location before this
139+ // atomic access, if there previously was a non-atomic initializing access. We set the
140+ // initial state of a mutex to be "unlocked".
135141 /* old_val */ MUTEX_UNLOCKED,
136142 MemOrdering::Release,
137143 SAddr (address),
0 commit comments