|
| 1 | +/** This file contains functionality related to handling mutexes. */ |
| 2 | + |
| 3 | +#include "MiriInterface.hpp" |
| 4 | + |
| 5 | +// GenMC headers: |
| 6 | +#include "Static/ModuleID.hpp" |
| 7 | + |
| 8 | +// CXX.rs generated headers: |
| 9 | +#include "genmc-sys/src/lib.rs.h" |
| 10 | + |
| 11 | +#define MUTEX_UNLOCKED SVal(0) |
| 12 | +#define MUTEX_LOCKED SVal(1) |
| 13 | + |
| 14 | +auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size) |
| 15 | + -> MutexLockResult { |
| 16 | + // This annotation informs GenMC about the condition required to make this lock call succeed. |
| 17 | + // It stands for `value_read_by_load != MUTEX_LOCKED`. |
| 18 | + const auto size_bits = size * 8; |
| 19 | + const auto annot = std::move(Annotation( |
| 20 | + AssumeType::Spinloop, |
| 21 | + Annotation::ExprVP( |
| 22 | + NeExpr<ModuleID::ID>::create( |
| 23 | + // `RegisterExpr` marks the value of the current expression, i.e., the loaded value. |
| 24 | + // The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute |
| 25 | + // other variables from previous expressions that may be used here. |
| 26 | + RegisterExpr<ModuleID::ID>::create(size_bits, /* id */ 0), |
| 27 | + ConcreteExpr<ModuleID::ID>::create(size_bits, MUTEX_LOCKED) |
| 28 | + ) |
| 29 | + .release() |
| 30 | + ) |
| 31 | + )); |
| 32 | + |
| 33 | + // As usual, we need to tell GenMC which value was stored at this location before this atomic |
| 34 | + // access, if there previously was a non-atomic initializing access. We set the initial state of |
| 35 | + // a mutex to be "unlocked". |
| 36 | + const auto old_val = MUTEX_UNLOCKED; |
| 37 | + const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::LockCasRead>( |
| 38 | + thread_id, |
| 39 | + old_val, |
| 40 | + address, |
| 41 | + size, |
| 42 | + annot, |
| 43 | + EventDeps() |
| 44 | + ); |
| 45 | + if (const auto* err = std::get_if<VerificationError>(&load_ret)) |
| 46 | + return MutexLockResultExt::from_error(format_error(*err)); |
| 47 | + // If we get a `Reset`, GenMC decided that this lock operation should not yet run, since it |
| 48 | + // would not acquire the mutex. Like the handling of the case further down where we read a `1` |
| 49 | + // ("Mutex already locked"), Miri should call the handle function again once the current thread |
| 50 | + // is scheduled by GenMC the next time. |
| 51 | + if (std::holds_alternative<Reset>(load_ret)) |
| 52 | + return MutexLockResultExt::reset(); |
| 53 | + |
| 54 | + const auto* ret_val = std::get_if<SVal>(&load_ret); |
| 55 | + ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result."); |
| 56 | + ERROR_ON( |
| 57 | + *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, |
| 58 | + "Mutex read value was neither 0 nor 1" |
| 59 | + ); |
| 60 | + const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; |
| 61 | + if (is_lock_acquired) { |
| 62 | + const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>( |
| 63 | + inc_pos(thread_id), |
| 64 | + old_val, |
| 65 | + address, |
| 66 | + size, |
| 67 | + EventDeps() |
| 68 | + ); |
| 69 | + if (const auto* err = std::get_if<VerificationError>(&store_ret)) |
| 70 | + return MutexLockResultExt::from_error(format_error(*err)); |
| 71 | + // We don't update Miri's memory for this operation so we don't need to know if the store |
| 72 | + // was the co-maximal store, but we still check that we at least get a boolean as the result |
| 73 | + // of the store. |
| 74 | + const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret); |
| 75 | + ERROR_ON( |
| 76 | + nullptr == is_coherence_order_maximal_write, |
| 77 | + "Unimplemented: store part of mutex try_lock returned unexpected result." |
| 78 | + ); |
| 79 | + } else { |
| 80 | + // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire |
| 81 | + // it. GenMC determines this based on the annotation we pass with the load further up in |
| 82 | + // this function, namely when that load will read a value other than `MUTEX_LOCKED`. |
| 83 | + this->handle_assume_block(thread_id, AssumeType::Spinloop); |
| 84 | + } |
| 85 | + return MutexLockResultExt::ok(is_lock_acquired); |
| 86 | +} |
| 87 | + |
| 88 | +auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size) |
| 89 | + -> MutexLockResult { |
| 90 | + auto& currPos = threads_action_[thread_id].event; |
| 91 | + // As usual, we need to tell GenMC which value was stored at this location before this atomic |
| 92 | + // access, if there previously was a non-atomic initializing access. We set the initial state of |
| 93 | + // a mutex to be "unlocked". |
| 94 | + const auto old_val = MUTEX_UNLOCKED; |
| 95 | + const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>( |
| 96 | + ++currPos, |
| 97 | + old_val, |
| 98 | + SAddr(address), |
| 99 | + ASize(size) |
| 100 | + ); |
| 101 | + if (const auto* err = std::get_if<VerificationError>(&load_ret)) |
| 102 | + return MutexLockResultExt::from_error(format_error(*err)); |
| 103 | + const auto* ret_val = std::get_if<SVal>(&load_ret); |
| 104 | + if (nullptr == ret_val) { |
| 105 | + ERROR("Unimplemented: mutex trylock load returned unexpected result."); |
| 106 | + } |
| 107 | + |
| 108 | + ERROR_ON( |
| 109 | + *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED, |
| 110 | + "Mutex read value was neither 0 nor 1" |
| 111 | + ); |
| 112 | + const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED; |
| 113 | + if (!is_lock_acquired) { |
| 114 | + return MutexLockResultExt::ok(false); /* Lock already held. */ |
| 115 | + } |
| 116 | + |
| 117 | + const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>( |
| 118 | + ++currPos, |
| 119 | + old_val, |
| 120 | + SAddr(address), |
| 121 | + ASize(size) |
| 122 | + ); |
| 123 | + if (const auto* err = std::get_if<VerificationError>(&store_ret)) |
| 124 | + return MutexLockResultExt::from_error(format_error(*err)); |
| 125 | + // We don't update Miri's memory for this operation so we don't need to know if the store was |
| 126 | + // co-maximal, but we still check that we get a boolean result. |
| 127 | + const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret); |
| 128 | + ERROR_ON( |
| 129 | + nullptr == is_coherence_order_maximal_write, |
| 130 | + "Unimplemented: store part of mutex try_lock returned unexpected result." |
| 131 | + ); |
| 132 | + return MutexLockResultExt::ok(true); |
| 133 | +} |
| 134 | + |
| 135 | +auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size) |
| 136 | + -> StoreResult { |
| 137 | + const auto pos = inc_pos(thread_id); |
| 138 | + const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>( |
| 139 | + pos, |
| 140 | + // As usual, we need to tell GenMC which value was stored at this location before this |
| 141 | + // atomic access, if there previously was a non-atomic initializing access. We set the |
| 142 | + // initial state of a mutex to be "unlocked". |
| 143 | + /* old_val */ MUTEX_UNLOCKED, |
| 144 | + MemOrdering::Release, |
| 145 | + SAddr(address), |
| 146 | + ASize(size), |
| 147 | + AType::Signed, |
| 148 | + /* store_value */ MUTEX_UNLOCKED, |
| 149 | + EventDeps() |
| 150 | + ); |
| 151 | + if (const auto* err = std::get_if<VerificationError>(&ret)) |
| 152 | + return StoreResultExt::from_error(format_error(*err)); |
| 153 | + const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret); |
| 154 | + ERROR_ON( |
| 155 | + nullptr == is_coherence_order_maximal_write, |
| 156 | + "Unimplemented: store part of mutex unlock returned unexpected result." |
| 157 | + ); |
| 158 | + return StoreResultExt::ok(*is_coherence_order_maximal_write); |
| 159 | +} |
0 commit comments