genmc/build,api: Move wrappers around GenMC API to single file
GenMC has a single API that was handled in a collection of different files. This commit collects all API wrappers to Exploration.cpp. (The Setup.cpp file remains intact as it contains setting translation and setup functions.)
This commit is contained in:
Michalis Kokologiannakis
parent
d659758c07
commit
c357b65324
5 changed files with 457 additions and 495 deletions
|
|
@ -178,14 +178,8 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
|
|||
// These are all the C++ files we need to compile, which needs to be updated if more C++ files are added to Miri.
|
||||
// We use absolute paths since relative paths can confuse IDEs when attempting to go-to-source on a path in a compiler error.
|
||||
let cpp_files_base_path = Path::new("cpp/src/");
|
||||
let cpp_files = [
|
||||
"MiriInterface/EventHandling.cpp",
|
||||
"MiriInterface/Exploration.cpp",
|
||||
"MiriInterface/Mutex.cpp",
|
||||
"MiriInterface/Setup.cpp",
|
||||
"MiriInterface/ThreadManagement.cpp",
|
||||
]
|
||||
.map(|file| std::path::absolute(cpp_files_base_path.join(file)).unwrap());
|
||||
let cpp_files = ["MiriInterface/Exploration.cpp", "MiriInterface/Setup.cpp"]
|
||||
.map(|file| std::path::absolute(cpp_files_base_path.join(file)).unwrap());
|
||||
|
||||
let mut bridge = cxx_build::bridge("src/lib.rs");
|
||||
// FIXME(genmc,cmake): Remove once the GenMC debug setting is available in the config.h file.
|
||||
|
|
|
|||
|
|
@ -1,265 +0,0 @@
|
|||
/** This file contains functionality related to handling events encountered
|
||||
* during an execution, such as loads, stores or memory (de)allocation. */
|
||||
|
||||
#include "MiriInterface.hpp"
|
||||
|
||||
// CXX.rs generated headers:
|
||||
#include "genmc-sys/src/lib.rs.h"
|
||||
|
||||
// GenMC headers:
|
||||
#include "ADT/value_ptr.hpp"
|
||||
#include "ExecutionGraph/EventLabel.hpp"
|
||||
#include "ExecutionGraph/LoadAnnotation.hpp"
|
||||
#include "Runtime/InterpreterEnumAPI.hpp"
|
||||
#include "Static/ModuleID.hpp"
|
||||
#include "Support/ASize.hpp"
|
||||
#include "Support/Error.hpp"
|
||||
#include "Support/Logger.hpp"
|
||||
#include "Support/MemAccess.hpp"
|
||||
#include "Support/RMWOps.hpp"
|
||||
#include "Support/SAddr.hpp"
|
||||
#include "Support/SVal.hpp"
|
||||
#include "Support/ThreadInfo.hpp"
|
||||
#include "Support/Verbosity.hpp"
|
||||
#include "Verification/GenMCDriver.hpp"
|
||||
#include "Verification/MemoryModel.hpp"
|
||||
|
||||
// C++ headers:
|
||||
#include <cstddef>
|
||||
#include <cstdint>
|
||||
#include <memory>
|
||||
#include <utility>
|
||||
|
||||
/**** Blocking instructions ****/
|
||||
|
||||
void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) {
|
||||
BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
|
||||
GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type);
|
||||
}
|
||||
|
||||
/**** Memory access handling ****/
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_load(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
MemOrdering ord,
|
||||
GenmcScalar old_val
|
||||
) -> LoadResult {
|
||||
// `type` is only used for printing.
|
||||
const auto type = AType::Unsigned;
|
||||
const auto ret = handle_load_reset_if_none<EventLabel::EventLabelKind::Read>(
|
||||
thread_id,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ord,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
type
|
||||
);
|
||||
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret))
|
||||
return LoadResultExt::from_error(format_error(*err));
|
||||
const auto* ret_val = std::get_if<SVal>(&ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
if (ret_val == nullptr)
|
||||
ERROR("Unimplemented: load returned unexpected result.");
|
||||
return LoadResultExt::from_value(*ret_val);
|
||||
}
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_store(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
GenmcScalar value,
|
||||
GenmcScalar old_val,
|
||||
MemOrdering ord
|
||||
) -> StoreResult {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
|
||||
nullptr,
|
||||
pos,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ord,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
/* type */ AType::Unsigned, // `type` is only used for printing.
|
||||
GenmcScalarExt::to_sval(value),
|
||||
EventDeps()
|
||||
);
|
||||
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret))
|
||||
return StoreResultExt::from_error(format_error(*err));
|
||||
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: Store returned unexpected result."
|
||||
);
|
||||
return StoreResultExt::ok(*is_coherence_order_maximal_write);
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
|
||||
}
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
RMWBinOp rmw_op,
|
||||
MemOrdering ordering,
|
||||
GenmcScalar rhs_value,
|
||||
GenmcScalar old_val
|
||||
) -> ReadModifyWriteResult {
|
||||
// NOTE: Both the store and load events should get the same `ordering`, it should not be split
|
||||
// into a load and a store component. This means we can have for example `AcqRel` loads and
|
||||
// stores, but this is intended for RMW operations.
|
||||
|
||||
// Somewhat confusingly, the GenMC term for RMW read/write labels is
|
||||
// `FaiRead` and `FaiWrite`.
|
||||
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::FaiRead>(
|
||||
thread_id,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
rmw_op,
|
||||
GenmcScalarExt::to_sval(rhs_value),
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
return ReadModifyWriteResultExt::from_error(format_error(*err));
|
||||
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
if (nullptr == ret_val) {
|
||||
ERROR("Unimplemented: read-modify-write returned unexpected result.");
|
||||
}
|
||||
const auto read_old_val = *ret_val;
|
||||
const auto new_value =
|
||||
executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op);
|
||||
|
||||
const auto storePos = inc_pos(thread_id);
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
|
||||
nullptr,
|
||||
storePos,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
new_value
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
return ReadModifyWriteResultExt::from_error(format_error(*err));
|
||||
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: RMW store returned unexpected result."
|
||||
);
|
||||
return ReadModifyWriteResultExt::ok(
|
||||
/* old_value: */ read_old_val,
|
||||
new_value,
|
||||
*is_coherence_order_maximal_write
|
||||
);
|
||||
}
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_compare_exchange(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
GenmcScalar expected_value,
|
||||
GenmcScalar new_value,
|
||||
GenmcScalar old_val,
|
||||
MemOrdering success_ordering,
|
||||
MemOrdering fail_load_ordering,
|
||||
bool can_fail_spuriously
|
||||
) -> CompareExchangeResult {
|
||||
// NOTE: Both the store and load events should get the same `ordering`, it should not be split
|
||||
// into a load and a store component. This means we can have for example `AcqRel` loads and
|
||||
// stores, but this is intended for CAS operations.
|
||||
|
||||
// FIXME(GenMC): properly handle failure memory ordering.
|
||||
|
||||
auto expectedVal = GenmcScalarExt::to_sval(expected_value);
|
||||
auto new_val = GenmcScalarExt::to_sval(new_value);
|
||||
|
||||
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::CasRead>(
|
||||
thread_id,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
success_ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
expectedVal,
|
||||
new_val
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
return CompareExchangeResultExt::from_error(format_error(*err));
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result.");
|
||||
const auto read_old_val = *ret_val;
|
||||
if (read_old_val != expectedVal)
|
||||
return CompareExchangeResultExt::failure(read_old_val);
|
||||
|
||||
// FIXME(GenMC): Add support for modelling spurious failures.
|
||||
|
||||
const auto storePos = inc_pos(thread_id);
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
|
||||
nullptr,
|
||||
storePos,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
success_ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
new_val
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
return CompareExchangeResultExt::from_error(format_error(*err));
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: compare-exchange store returned unexpected result."
|
||||
);
|
||||
return CompareExchangeResultExt::success(read_old_val, *is_coherence_order_maximal_write);
|
||||
}
|
||||
|
||||
/**** Memory (de)allocation ****/
|
||||
|
||||
auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)
|
||||
-> uint64_t {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
|
||||
// These are only used for printing and features Miri-GenMC doesn't support (yet).
|
||||
const auto storage_duration = StorageDuration::SD_Heap;
|
||||
// Volatile, as opposed to "persistent" (i.e., non-volatile memory that persists over reboots)
|
||||
const auto storage_type = StorageType::ST_Volatile;
|
||||
const auto address_space = AddressSpace::AS_User;
|
||||
|
||||
const SVal ret_val = GenMCDriver::handleMalloc(
|
||||
nullptr,
|
||||
pos,
|
||||
size,
|
||||
alignment,
|
||||
storage_duration,
|
||||
storage_type,
|
||||
address_space,
|
||||
EventDeps()
|
||||
);
|
||||
return ret_val.get();
|
||||
}
|
||||
|
||||
auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps());
|
||||
// FIXME(genmc): use returned error from `handleFree` once implemented in GenMC.
|
||||
return getResult().status.has_value();
|
||||
}
|
||||
|
|
@ -1,4 +1,5 @@
|
|||
/** This file contains functionality related to exploration, such as scheduling. */
|
||||
/** This file contains functionality related to exploration events
|
||||
* such as loads, stores and memory (de)allocation. */
|
||||
|
||||
#include "MiriInterface.hpp"
|
||||
|
||||
|
|
@ -6,13 +7,32 @@
|
|||
#include "genmc-sys/src/lib.rs.h"
|
||||
|
||||
// GenMC headers:
|
||||
#include "ADT/value_ptr.hpp"
|
||||
#include "ExecutionGraph/EventLabel.hpp"
|
||||
#include "ExecutionGraph/LoadAnnotation.hpp"
|
||||
#include "Runtime/InterpreterEnumAPI.hpp"
|
||||
#include "Static/ModuleID.hpp"
|
||||
#include "Support/ASize.hpp"
|
||||
#include "Support/Error.hpp"
|
||||
#include "Support/Logger.hpp"
|
||||
#include "Support/MemAccess.hpp"
|
||||
#include "Support/RMWOps.hpp"
|
||||
#include "Support/SAddr.hpp"
|
||||
#include "Support/SVal.hpp"
|
||||
#include "Support/ThreadInfo.hpp"
|
||||
#include "Support/Verbosity.hpp"
|
||||
#include "Verification/GenMCDriver.hpp"
|
||||
#include "Verification/MemoryModel.hpp"
|
||||
|
||||
// C++ headers:
|
||||
#include <cmath>
|
||||
#include <cstddef>
|
||||
#include <cstdint>
|
||||
#include <limits>
|
||||
#include <memory>
|
||||
#include <utility>
|
||||
|
||||
/** Scheduling */
|
||||
|
||||
auto MiriGenmcShim::schedule_next(
|
||||
const int curr_thread_id,
|
||||
|
|
@ -41,8 +61,6 @@ auto MiriGenmcShim::schedule_next(
|
|||
);
|
||||
}
|
||||
|
||||
/**** Execution start/end handling ****/
|
||||
|
||||
void MiriGenmcShim::handle_execution_start() {
|
||||
threads_action_.clear();
|
||||
threads_action_.push_back(Action(ActionKind::Load, Event::getInit()));
|
||||
|
|
@ -55,6 +73,240 @@ auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr<std::string> {
|
|||
return {};
|
||||
}
|
||||
|
||||
/**** Blocking instructions ****/
|
||||
|
||||
void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) {
|
||||
BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
|
||||
GenMCDriver::handleAssume(nullptr, inc_pos(thread_id), assume_type);
|
||||
}
|
||||
|
||||
/**** Memory access handling ****/
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_load(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
MemOrdering ord,
|
||||
GenmcScalar old_val
|
||||
) -> LoadResult {
|
||||
// `type` is only used for printing.
|
||||
const auto type = AType::Unsigned;
|
||||
const auto ret = handle_load_reset_if_none<EventLabel::EventLabelKind::Read>(
|
||||
thread_id,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ord,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
type
|
||||
);
|
||||
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret))
|
||||
return LoadResultExt::from_error(format_error(*err));
|
||||
const auto* ret_val = std::get_if<SVal>(&ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
if (ret_val == nullptr)
|
||||
ERROR("Unimplemented: load returned unexpected result.");
|
||||
return LoadResultExt::from_value(*ret_val);
|
||||
}
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_store(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
GenmcScalar value,
|
||||
GenmcScalar old_val,
|
||||
MemOrdering ord
|
||||
) -> StoreResult {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
|
||||
nullptr,
|
||||
pos,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ord,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
/* type */ AType::Unsigned, // `type` is only used for printing.
|
||||
GenmcScalarExt::to_sval(value),
|
||||
EventDeps()
|
||||
);
|
||||
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret))
|
||||
return StoreResultExt::from_error(format_error(*err));
|
||||
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: Store returned unexpected result."
|
||||
);
|
||||
return StoreResultExt::ok(*is_coherence_order_maximal_write);
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
GenMCDriver::handleFence(nullptr, pos, ord, EventDeps());
|
||||
}
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
RMWBinOp rmw_op,
|
||||
MemOrdering ordering,
|
||||
GenmcScalar rhs_value,
|
||||
GenmcScalar old_val
|
||||
) -> ReadModifyWriteResult {
|
||||
// NOTE: Both the store and load events should get the same `ordering`, it should not be split
|
||||
// into a load and a store component. This means we can have for example `AcqRel` loads and
|
||||
// stores, but this is intended for RMW operations.
|
||||
|
||||
// Somewhat confusingly, the GenMC term for RMW read/write labels is
|
||||
// `FaiRead` and `FaiWrite`.
|
||||
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::FaiRead>(
|
||||
thread_id,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
rmw_op,
|
||||
GenmcScalarExt::to_sval(rhs_value),
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
return ReadModifyWriteResultExt::from_error(format_error(*err));
|
||||
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
if (nullptr == ret_val) {
|
||||
ERROR("Unimplemented: read-modify-write returned unexpected result.");
|
||||
}
|
||||
const auto read_old_val = *ret_val;
|
||||
const auto new_value =
|
||||
executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op);
|
||||
|
||||
const auto storePos = inc_pos(thread_id);
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
|
||||
nullptr,
|
||||
storePos,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
new_value
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
return ReadModifyWriteResultExt::from_error(format_error(*err));
|
||||
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: RMW store returned unexpected result."
|
||||
);
|
||||
return ReadModifyWriteResultExt::ok(
|
||||
/* old_value: */ read_old_val,
|
||||
new_value,
|
||||
*is_coherence_order_maximal_write
|
||||
);
|
||||
}
|
||||
|
||||
[[nodiscard]] auto MiriGenmcShim::handle_compare_exchange(
|
||||
ThreadId thread_id,
|
||||
uint64_t address,
|
||||
uint64_t size,
|
||||
GenmcScalar expected_value,
|
||||
GenmcScalar new_value,
|
||||
GenmcScalar old_val,
|
||||
MemOrdering success_ordering,
|
||||
MemOrdering fail_load_ordering,
|
||||
bool can_fail_spuriously
|
||||
) -> CompareExchangeResult {
|
||||
// NOTE: Both the store and load events should get the same `ordering`, it should not be split
|
||||
// into a load and a store component. This means we can have for example `AcqRel` loads and
|
||||
// stores, but this is intended for CAS operations.
|
||||
|
||||
// FIXME(GenMC): properly handle failure memory ordering.
|
||||
|
||||
auto expectedVal = GenmcScalarExt::to_sval(expected_value);
|
||||
auto new_val = GenmcScalarExt::to_sval(new_value);
|
||||
|
||||
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::CasRead>(
|
||||
thread_id,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
success_ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
expectedVal,
|
||||
new_val
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
return CompareExchangeResultExt::from_error(format_error(*err));
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result.");
|
||||
const auto read_old_val = *ret_val;
|
||||
if (read_old_val != expectedVal)
|
||||
return CompareExchangeResultExt::failure(read_old_val);
|
||||
|
||||
// FIXME(GenMC): Add support for modelling spurious failures.
|
||||
|
||||
const auto storePos = inc_pos(thread_id);
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
|
||||
nullptr,
|
||||
storePos,
|
||||
GenmcScalarExt::try_to_sval(old_val),
|
||||
success_ordering,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Unsigned, // The type is only used for printing.
|
||||
new_val
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
return CompareExchangeResultExt::from_error(format_error(*err));
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: compare-exchange store returned unexpected result."
|
||||
);
|
||||
return CompareExchangeResultExt::success(read_old_val, *is_coherence_order_maximal_write);
|
||||
}
|
||||
|
||||
/**** Memory (de)allocation ****/
|
||||
|
||||
auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)
|
||||
-> uint64_t {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
|
||||
// These are only used for printing and features Miri-GenMC doesn't support (yet).
|
||||
const auto storage_duration = StorageDuration::SD_Heap;
|
||||
// Volatile, as opposed to "persistent" (i.e., non-volatile memory that persists over reboots)
|
||||
const auto storage_type = StorageType::ST_Volatile;
|
||||
const auto address_space = AddressSpace::AS_User;
|
||||
|
||||
const SVal ret_val = GenMCDriver::handleMalloc(
|
||||
nullptr,
|
||||
pos,
|
||||
size,
|
||||
alignment,
|
||||
storage_duration,
|
||||
storage_type,
|
||||
address_space,
|
||||
EventDeps()
|
||||
);
|
||||
return ret_val.get();
|
||||
}
|
||||
|
||||
auto MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) -> bool {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
GenMCDriver::handleFree(nullptr, pos, SAddr(address), EventDeps());
|
||||
// FIXME(genmc): use returned error from `handleFree` once implemented in GenMC.
|
||||
return getResult().status.has_value();
|
||||
}
|
||||
|
||||
/**** Estimation mode result ****/
|
||||
|
||||
auto MiriGenmcShim::get_estimation_results() const -> EstimationResult {
|
||||
|
|
@ -66,3 +318,203 @@ auto MiriGenmcShim::get_estimation_results() const -> EstimationResult {
|
|||
.blocked_execs = static_cast<uint64_t>(res.exploredBlocked),
|
||||
};
|
||||
}
|
||||
|
||||
/** Mutexes */
|
||||
|
||||
#define MUTEX_UNLOCKED SVal(0)
|
||||
#define MUTEX_LOCKED SVal(1)
|
||||
|
||||
auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> MutexLockResult {
|
||||
// This annotation informs GenMC about the condition required to make this lock call succeed.
|
||||
// It stands for `value_read_by_load != MUTEX_LOCKED`.
|
||||
const auto size_bits = size * 8;
|
||||
const auto annot = std::move(Annotation(
|
||||
AssumeType::Spinloop,
|
||||
Annotation::ExprVP(
|
||||
NeExpr<ModuleID::ID>::create(
|
||||
// `RegisterExpr` marks the value of the current expression, i.e., the loaded value.
|
||||
// The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute
|
||||
// other variables from previous expressions that may be used here.
|
||||
RegisterExpr<ModuleID::ID>::create(size_bits, /* id */ 0),
|
||||
ConcreteExpr<ModuleID::ID>::create(size_bits, MUTEX_LOCKED)
|
||||
)
|
||||
.release()
|
||||
)
|
||||
));
|
||||
|
||||
// As usual, we need to tell GenMC which value was stored at this location before this atomic
|
||||
// access, if there previously was a non-atomic initializing access. We set the initial state of
|
||||
// a mutex to be "unlocked".
|
||||
const auto old_val = MUTEX_UNLOCKED;
|
||||
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::LockCasRead>(
|
||||
thread_id,
|
||||
old_val,
|
||||
address,
|
||||
size,
|
||||
annot,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
// If we get a `Reset`, GenMC decided that this lock operation should not yet run, since it
|
||||
// would not acquire the mutex. Like the handling of the case further down where we read a `1`
|
||||
// ("Mutex already locked"), Miri should call the handle function again once the current thread
|
||||
// is scheduled by GenMC the next time.
|
||||
if (std::holds_alternative<Reset>(load_ret))
|
||||
return MutexLockResultExt::reset();
|
||||
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result.");
|
||||
ERROR_ON(
|
||||
*ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
|
||||
"Mutex read value was neither 0 nor 1"
|
||||
);
|
||||
const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
|
||||
if (is_lock_acquired) {
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
|
||||
nullptr,
|
||||
inc_pos(thread_id),
|
||||
old_val,
|
||||
address,
|
||||
size,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
// We don't update Miri's memory for this operation so we don't need to know if the store
|
||||
// was the co-maximal store, but we still check that we at least get a boolean as the result
|
||||
// of the store.
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: store part of mutex try_lock returned unexpected result."
|
||||
);
|
||||
} else {
|
||||
// We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
|
||||
// it. GenMC determines this based on the annotation we pass with the load further up in
|
||||
// this function, namely when that load will read a value other than `MUTEX_LOCKED`.
|
||||
this->handle_assume_block(thread_id, AssumeType::Spinloop);
|
||||
}
|
||||
return MutexLockResultExt::ok(is_lock_acquired);
|
||||
}
|
||||
|
||||
auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> MutexLockResult {
|
||||
auto& currPos = threads_action_[thread_id].event;
|
||||
// As usual, we need to tell GenMC which value was stored at this location before this atomic
|
||||
// access, if there previously was a non-atomic initializing access. We set the initial state of
|
||||
// a mutex to be "unlocked".
|
||||
const auto old_val = MUTEX_UNLOCKED;
|
||||
const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
|
||||
nullptr,
|
||||
++currPos,
|
||||
old_val,
|
||||
SAddr(address),
|
||||
ASize(size)
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
if (nullptr == ret_val) {
|
||||
ERROR("Unimplemented: mutex trylock load returned unexpected result.");
|
||||
}
|
||||
|
||||
ERROR_ON(
|
||||
*ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
|
||||
"Mutex read value was neither 0 nor 1"
|
||||
);
|
||||
const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
|
||||
if (!is_lock_acquired) {
|
||||
return MutexLockResultExt::ok(false); /* Lock already held. */
|
||||
}
|
||||
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
|
||||
nullptr,
|
||||
++currPos,
|
||||
old_val,
|
||||
SAddr(address),
|
||||
ASize(size)
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
// We don't update Miri's memory for this operation so we don't need to know if the store was
|
||||
// co-maximal, but we still check that we get a boolean result.
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: store part of mutex try_lock returned unexpected result."
|
||||
);
|
||||
return MutexLockResultExt::ok(true);
|
||||
}
|
||||
|
||||
auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> StoreResult {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
|
||||
nullptr,
|
||||
pos,
|
||||
// As usual, we need to tell GenMC which value was stored at this location before this
|
||||
// atomic access, if there previously was a non-atomic initializing access. We set the
|
||||
// initial state of a mutex to be "unlocked".
|
||||
/* old_val */ MUTEX_UNLOCKED,
|
||||
MemOrdering::Release,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Signed,
|
||||
/* store_value */ MUTEX_UNLOCKED,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret))
|
||||
return StoreResultExt::from_error(format_error(*err));
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: store part of mutex unlock returned unexpected result."
|
||||
);
|
||||
return StoreResultExt::ok(*is_coherence_order_maximal_write);
|
||||
}
|
||||
|
||||
/** Thread creation/joining */
|
||||
|
||||
void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) {
|
||||
// NOTE: The threadCreate event happens in the parent:
|
||||
const auto pos = inc_pos(parent_id);
|
||||
// FIXME(genmc): for supporting symmetry reduction, these will need to be properly set:
|
||||
const unsigned fun_id = 0;
|
||||
const SVal arg = SVal(0);
|
||||
const ThreadInfo child_info =
|
||||
ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" };
|
||||
|
||||
// NOTE: Default memory ordering (`Release`) used here.
|
||||
const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps());
|
||||
// Sanity check the thread id, which is the index in the `threads_action_` array.
|
||||
BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size());
|
||||
threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0)));
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
|
||||
// The thread join event happens in the parent.
|
||||
const auto pos = inc_pos(thread_id);
|
||||
|
||||
// NOTE: Default memory ordering (`Acquire`) used here.
|
||||
const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
|
||||
// If the join failed, decrease the event index again:
|
||||
if (!std::holds_alternative<SVal>(ret)) {
|
||||
dec_pos(thread_id);
|
||||
}
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values.
|
||||
|
||||
// NOTE: Thread return value is ignored, since Miri doesn't need it.
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
// NOTE: Default memory ordering (`Release`) used here.
|
||||
GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val));
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
GenMCDriver::handleThreadKill(nullptr, pos);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,163 +0,0 @@
|
|||
/** This file contains functionality related to handling mutexes. */
|
||||
|
||||
#include "MiriInterface.hpp"
|
||||
|
||||
// GenMC headers:
|
||||
#include "Static/ModuleID.hpp"
|
||||
|
||||
// CXX.rs generated headers:
|
||||
#include "genmc-sys/src/lib.rs.h"
|
||||
|
||||
#define MUTEX_UNLOCKED SVal(0)
|
||||
#define MUTEX_LOCKED SVal(1)
|
||||
|
||||
auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> MutexLockResult {
|
||||
// This annotation informs GenMC about the condition required to make this lock call succeed.
|
||||
// It stands for `value_read_by_load != MUTEX_LOCKED`.
|
||||
const auto size_bits = size * 8;
|
||||
const auto annot = std::move(Annotation(
|
||||
AssumeType::Spinloop,
|
||||
Annotation::ExprVP(
|
||||
NeExpr<ModuleID::ID>::create(
|
||||
// `RegisterExpr` marks the value of the current expression, i.e., the loaded value.
|
||||
// The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute
|
||||
// other variables from previous expressions that may be used here.
|
||||
RegisterExpr<ModuleID::ID>::create(size_bits, /* id */ 0),
|
||||
ConcreteExpr<ModuleID::ID>::create(size_bits, MUTEX_LOCKED)
|
||||
)
|
||||
.release()
|
||||
)
|
||||
));
|
||||
|
||||
// As usual, we need to tell GenMC which value was stored at this location before this atomic
|
||||
// access, if there previously was a non-atomic initializing access. We set the initial state of
|
||||
// a mutex to be "unlocked".
|
||||
const auto old_val = MUTEX_UNLOCKED;
|
||||
const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::LockCasRead>(
|
||||
thread_id,
|
||||
old_val,
|
||||
address,
|
||||
size,
|
||||
annot,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
// If we get a `Reset`, GenMC decided that this lock operation should not yet run, since it
|
||||
// would not acquire the mutex. Like the handling of the case further down where we read a `1`
|
||||
// ("Mutex already locked"), Miri should call the handle function again once the current thread
|
||||
// is scheduled by GenMC the next time.
|
||||
if (std::holds_alternative<Reset>(load_ret))
|
||||
return MutexLockResultExt::reset();
|
||||
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result.");
|
||||
ERROR_ON(
|
||||
*ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
|
||||
"Mutex read value was neither 0 nor 1"
|
||||
);
|
||||
const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
|
||||
if (is_lock_acquired) {
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
|
||||
nullptr,
|
||||
inc_pos(thread_id),
|
||||
old_val,
|
||||
address,
|
||||
size,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
// We don't update Miri's memory for this operation so we don't need to know if the store
|
||||
// was the co-maximal store, but we still check that we at least get a boolean as the result
|
||||
// of the store.
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: store part of mutex try_lock returned unexpected result."
|
||||
);
|
||||
} else {
|
||||
// We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
|
||||
// it. GenMC determines this based on the annotation we pass with the load further up in
|
||||
// this function, namely when that load will read a value other than `MUTEX_LOCKED`.
|
||||
this->handle_assume_block(thread_id, AssumeType::Spinloop);
|
||||
}
|
||||
return MutexLockResultExt::ok(is_lock_acquired);
|
||||
}
|
||||
|
||||
auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> MutexLockResult {
|
||||
auto& currPos = threads_action_[thread_id].event;
|
||||
// As usual, we need to tell GenMC which value was stored at this location before this atomic
|
||||
// access, if there previously was a non-atomic initializing access. We set the initial state of
|
||||
// a mutex to be "unlocked".
|
||||
const auto old_val = MUTEX_UNLOCKED;
|
||||
const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
|
||||
nullptr,
|
||||
++currPos,
|
||||
old_val,
|
||||
SAddr(address),
|
||||
ASize(size)
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&load_ret))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
const auto* ret_val = std::get_if<SVal>(&load_ret);
|
||||
if (nullptr == ret_val) {
|
||||
ERROR("Unimplemented: mutex trylock load returned unexpected result.");
|
||||
}
|
||||
|
||||
ERROR_ON(
|
||||
*ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
|
||||
"Mutex read value was neither 0 nor 1"
|
||||
);
|
||||
const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
|
||||
if (!is_lock_acquired) {
|
||||
return MutexLockResultExt::ok(false); /* Lock already held. */
|
||||
}
|
||||
|
||||
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
|
||||
nullptr,
|
||||
++currPos,
|
||||
old_val,
|
||||
SAddr(address),
|
||||
ASize(size)
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&store_ret))
|
||||
return MutexLockResultExt::from_error(format_error(*err));
|
||||
// We don't update Miri's memory for this operation so we don't need to know if the store was
|
||||
// co-maximal, but we still check that we get a boolean result.
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: store part of mutex try_lock returned unexpected result."
|
||||
);
|
||||
return MutexLockResultExt::ok(true);
|
||||
}
|
||||
|
||||
auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size)
|
||||
-> StoreResult {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
|
||||
nullptr,
|
||||
pos,
|
||||
// As usual, we need to tell GenMC which value was stored at this location before this
|
||||
// atomic access, if there previously was a non-atomic initializing access. We set the
|
||||
// initial state of a mutex to be "unlocked".
|
||||
/* old_val */ MUTEX_UNLOCKED,
|
||||
MemOrdering::Release,
|
||||
SAddr(address),
|
||||
ASize(size),
|
||||
AType::Signed,
|
||||
/* store_value */ MUTEX_UNLOCKED,
|
||||
EventDeps()
|
||||
);
|
||||
if (const auto* err = std::get_if<VerificationError>(&ret))
|
||||
return StoreResultExt::from_error(format_error(*err));
|
||||
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
|
||||
ERROR_ON(
|
||||
nullptr == is_coherence_order_maximal_write,
|
||||
"Unimplemented: store part of mutex unlock returned unexpected result."
|
||||
);
|
||||
return StoreResultExt::ok(*is_coherence_order_maximal_write);
|
||||
}
|
||||
|
|
@ -1,56 +0,0 @@
|
|||
|
||||
/** This file contains functionality related thread management (creation, finishing, join, etc.) */
|
||||
|
||||
#include "MiriInterface.hpp"
|
||||
|
||||
// CXX.rs generated headers:
|
||||
#include "genmc-sys/src/lib.rs.h"
|
||||
|
||||
// GenMC headers:
|
||||
#include "Support/Error.hpp"
|
||||
#include "Support/Verbosity.hpp"
|
||||
|
||||
// C++ headers:
|
||||
#include <cstdint>
|
||||
|
||||
void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) {
|
||||
// NOTE: The threadCreate event happens in the parent:
|
||||
const auto pos = inc_pos(parent_id);
|
||||
// FIXME(genmc): for supporting symmetry reduction, these will need to be properly set:
|
||||
const unsigned fun_id = 0;
|
||||
const SVal arg = SVal(0);
|
||||
const ThreadInfo child_info =
|
||||
ThreadInfo { thread_id, parent_id, fun_id, arg, "unknown thread" };
|
||||
|
||||
// NOTE: Default memory ordering (`Release`) used here.
|
||||
const auto child_tid = GenMCDriver::handleThreadCreate(nullptr, pos, child_info, EventDeps());
|
||||
// Sanity check the thread id, which is the index in the `threads_action_` array.
|
||||
BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size());
|
||||
threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0)));
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
|
||||
// The thread join event happens in the parent.
|
||||
const auto pos = inc_pos(thread_id);
|
||||
|
||||
// NOTE: Default memory ordering (`Acquire`) used here.
|
||||
const auto ret = GenMCDriver::handleThreadJoin(nullptr, pos, child_id, EventDeps());
|
||||
// If the join failed, decrease the event index again:
|
||||
if (!std::holds_alternative<SVal>(ret)) {
|
||||
dec_pos(thread_id);
|
||||
}
|
||||
// FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values.
|
||||
|
||||
// NOTE: Thread return value is ignored, since Miri doesn't need it.
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
// NOTE: Default memory ordering (`Release`) used here.
|
||||
GenMCDriver::handleThreadFinish(nullptr, pos, SVal(ret_val));
|
||||
}
|
||||
|
||||
void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
|
||||
const auto pos = inc_pos(thread_id);
|
||||
GenMCDriver::handleThreadKill(nullptr, pos);
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue