user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Merge pull request #4578 from Patrick-6/miri-genmc-cas

Browse source 
Add compare_exchange support for GenMC mode
This commit is contained in:
Ralf Jung 2025-09-12 16:10:02 +00:00 • committed by GitHub
commit fc7eb3c28d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
27 changed files with 850 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

82
src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
View file

@ -34,6 +34,7 @@ struct SchedulingResult;
struct LoadResult;
struct StoreResult;
struct ReadModifyWriteResult;
struct CompareExchangeResult;
// GenMC uses `int` for its thread IDs.
using ThreadId = int;
@ -100,6 +101,17 @@ struct MiriGenmcShim : private GenMCDriver {
GenmcScalar rhs_value,
GenmcScalar old_val
);
[[nodiscard]] CompareExchangeResult 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
);
[[nodiscard]] StoreResult handle_store(
ThreadId thread_id,
uint64_t address,
@ -231,15 +243,15 @@ constexpr auto get_global_alloc_static_mask() -> uint64_t {
namespace GenmcScalarExt {
inline GenmcScalar uninit() {
return GenmcScalar {
/* value: */ 0,
/* is_init: */ false,
.value = 0,
.is_init = false,
};
}
inline GenmcScalar from_sval(SVal sval) {
return GenmcScalar {
/* value: */ sval.get(),
/* is_init: */ true,
.value = sval.get(),
.is_init = true,
};
}
@ -252,22 +264,22 @@ inline SVal to_sval(GenmcScalar scalar) {
namespace LoadResultExt {
inline LoadResult no_value() {
return LoadResult {
/* error: */ std::unique_ptr<std::string>(nullptr),
/* has_value: */ false,
/* read_value: */ GenmcScalarExt::uninit(),
.error = std::unique_ptr<std::string>(nullptr),
.has_value = false,
.read_value = GenmcScalarExt::uninit(),
};
}
inline LoadResult from_value(SVal read_value) {
return LoadResult { /* error: */ std::unique_ptr<std::string>(nullptr),
/* has_value: */ true,
/* read_value: */ GenmcScalarExt::from_sval(read_value) };
return LoadResult { .error = std::unique_ptr<std::string>(nullptr),
.has_value = true,
.read_value = GenmcScalarExt::from_sval(read_value) };
}
inline LoadResult from_error(std::unique_ptr<std::string> error) {
return LoadResult { /* error: */ std::move(error),
/* has_value: */ false,
/* read_value: */ GenmcScalarExt::uninit() };
return LoadResult { .error = std::move(error),
.has_value = false,
.read_value = GenmcScalarExt::uninit() };
}
} // namespace LoadResultExt
@ -278,26 +290,50 @@ inline StoreResult ok(bool is_coherence_order_maximal_write) {
}
inline StoreResult from_error(std::unique_ptr<std::string> error) {
return StoreResult { /* error: */ std::move(error),
/* is_coherence_order_maximal_write: */ false };
return StoreResult { .error = std::move(error), .is_coherence_order_maximal_write = false };
}
} // namespace StoreResultExt
namespace ReadModifyWriteResultExt {
inline ReadModifyWriteResult
ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) {
return ReadModifyWriteResult { /* error: */ std::unique_ptr<std::string>(nullptr),
/* old_value: */ GenmcScalarExt::from_sval(old_value),
/* new_value: */ GenmcScalarExt::from_sval(new_value),
is_coherence_order_maximal_write };
return ReadModifyWriteResult { .error = std::unique_ptr<std::string>(nullptr),
.old_value = GenmcScalarExt::from_sval(old_value),
.new_value = GenmcScalarExt::from_sval(new_value),
.is_coherence_order_maximal_write =
is_coherence_order_maximal_write };
}
inline ReadModifyWriteResult from_error(std::unique_ptr<std::string> error) {
return ReadModifyWriteResult { /* error: */ std::move(error),
/* old_value: */ GenmcScalarExt::uninit(),
/* new_value: */ GenmcScalarExt::uninit(),
/* is_coherence_order_maximal_write: */ false };
return ReadModifyWriteResult { .error = std::move(error),
.old_value = GenmcScalarExt::uninit(),
.new_value = GenmcScalarExt::uninit(),
.is_coherence_order_maximal_write = false };
}
} // namespace ReadModifyWriteResultExt
namespace CompareExchangeResultExt {
inline CompareExchangeResult success(SVal old_value, bool is_coherence_order_maximal_write) {
return CompareExchangeResult { .error = nullptr,
.old_value = GenmcScalarExt::from_sval(old_value),
.is_success = true,
.is_coherence_order_maximal_write =
is_coherence_order_maximal_write };
}
inline CompareExchangeResult failure(SVal old_value) {
return CompareExchangeResult { .error = nullptr,
.old_value = GenmcScalarExt::from_sval(old_value),
.is_success = false,
.is_coherence_order_maximal_write = false };
}
inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
return CompareExchangeResult { .error = std::move(error),
.old_value = GenmcScalarExt::uninit(),
.is_success = false,
.is_coherence_order_maximal_write = false };
}
} // namespace CompareExchangeResultExt
#endif /* GENMC_MIRI_INTERFACE_HPP */

65
src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
View file

@ -155,6 +155,71 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
);
}
[[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,
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);
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>(
storePos,
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 auto* store_ret_val = std::get_if<std::monostate>(&store_ret);
ERROR_ON(
nullptr == store_ret_val,
"Unimplemented: compare-exchange store returned unexpected result."
);
// FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once
// available).
const auto& g = getExec().getGraph();
return CompareExchangeResultExt::success(
read_old_val,
/* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == storePos
);
}
/**** Memory (de)allocation ****/
auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)

8
src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
View file

@ -152,10 +152,10 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
// Miri already ensures that memory accesses are valid, so this check doesn't matter.
// We check that the address is static, but skip checking if it is part of an actual
// allocation.
/* isStaticallyAllocated: */ [](SAddr addr) { return addr.isStatic(); },
.isStaticallyAllocated = [](SAddr addr) { return addr.isStatic(); },
// FIXME(genmc,error reporting): Once a proper a proper API for passing such information is
// implemented in GenMC, Miri should use it to improve the produced error messages.
/* getStaticName: */ [](SAddr addr) { return "[UNKNOWN STATIC]"; },
.getStaticName = [](SAddr addr) { return "[UNKNOWN STATIC]"; },
// This function is called to get the initial value stored at the given address.
//
// From a Miri perspective, this API doesn't work very well: most memory starts out
@ -177,10 +177,10 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
// FIXME(genmc): implement proper support for uninitialized memory in GenMC. Ideally, the
// initial value getter would return an `optional<SVal>`, since the memory location may be
// uninitialized.
/* initValGetter: */ [](const AAccess& a) { return SVal(0xDEAD); },
.initValGetter = [](const AAccess& a) { return SVal(0xDEAD); },
// Miri serves non-atomic loads from its own memory and these GenMC checks are wrong in
// that case. This should no longer be required with proper mixed-size access support.
/* skipUninitLoadChecks: */ [](MemOrdering ord) { return ord == MemOrdering::NotAtomic; },
.skipUninitLoadChecks = [](MemOrdering ord) { return ord == MemOrdering::NotAtomic; },
};
driver->setInterpCallbacks(std::move(interpreter_callbacks));

25
src/tools/miri/genmc-sys/src/lib.rs
View file

@ -198,6 +198,19 @@ mod ffi {
is_coherence_order_maximal_write: bool,
}
#[must_use]
#[derive(Debug)]
struct CompareExchangeResult {
/// If there was an error, it will be stored in `error`, otherwise it is `None`.
error: UniquePtr<CxxString>,
/// The value that was read by the compare-exchange.
old_value: GenmcScalar,
/// `true` if compare_exchange op was successful.
is_success: bool,
/// `true` if the write should also be reflected in Miri's memory representation.
is_coherence_order_maximal_write: bool,
}
/**** These are GenMC types that we have to copy-paste here since cxx does not support
"importing" externally defined C++ types. ****/
@ -313,6 +326,18 @@ mod ffi {
rhs_value: GenmcScalar,
old_value: GenmcScalar,
) -> ReadModifyWriteResult;
fn handle_compare_exchange(
self: Pin<&mut MiriGenmcShim>,
thread_id: i32,
address: u64,
size: u64,
expected_value: GenmcScalar,
new_value: GenmcScalar,
old_value: GenmcScalar,
success_ordering: MemOrdering,
fail_load_ordering: MemOrdering,
can_fail_spuriously: bool,
) -> CompareExchangeResult;
fn handle_store(
self: Pin<&mut MiriGenmcShim>,
thread_id: i32,

82
src/tools/miri/src/concurrency/genmc/helper.rs
View file

@ -1,20 +1,52 @@
use std::sync::RwLock;
use genmc_sys::{MemOrdering, RMWBinOp};
use rustc_abi::Size;
use rustc_const_eval::interpret::{InterpResult, interp_ok};
use rustc_data_structures::fx::FxHashSet;
use rustc_middle::mir;
use rustc_middle::ty::ScalarInt;
use rustc_span::Span;
use tracing::debug;
use super::GenmcScalar;
use crate::diagnostics::EvalContextExt;
use crate::intrinsics::AtomicRmwOp;
use crate::{
AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MiriInterpCx, Scalar,
throw_unsup_format,
AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, InterpCx, MiriInterpCx,
MiriMachine, NonHaltingDiagnostic, Scalar, throw_unsup_format,
};
/// Maximum size memory access in bytes that GenMC supports.
pub(super) const MAX_ACCESS_SIZE: u64 = 8;
/// Type for storing spans for already emitted warnings.
pub(super) type WarningCache = RwLock<FxHashSet<Span>>;
#[derive(Default)]
pub(super) struct Warnings {
pub(super) compare_exchange_failure_ordering: WarningCache,
pub(super) compare_exchange_weak: WarningCache,
}
/// Emit a warning if it hasn't already been reported for current span.
pub(super) fn emit_warning<'tcx>(
ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
cache: &WarningCache,
diagnostic: impl FnOnce() -> NonHaltingDiagnostic,
) {
let span = ecx.machine.current_span();
if cache.read().unwrap().contains(&span) {
return;
}
// This span has not yet been reported, so we insert it into the cache and report it.
let mut cache = cache.write().unwrap();
if cache.insert(span) {
// Some other thread may have added this span while we didn't hold the lock, so we only emit it if the insertions succeeded.
ecx.emit_diagnostic(diagnostic());
}
}
/// This function is used to split up a large memory access into aligned, non-overlapping chunks of a limited size.
/// Returns an iterator over the chunks, yielding `(base address, size)` of each chunk, ordered by address.
pub fn split_access(address: Size, size: Size) -> impl Iterator<Item = (u64, u64)> {
@ -112,7 +144,53 @@ impl AtomicFenceOrd {
}
}
/// Since GenMC ignores the failure memory ordering and Miri should not detect bugs that don't actually exist, we upgrade the success ordering if required.
/// This means that Miri running in GenMC mode will not explore all possible executions allowed under the RC11 memory model.
/// FIXME(genmc): remove this once GenMC properly supports the failure memory ordering.
pub(super) fn maybe_upgrade_compare_exchange_success_orderings(
success: AtomicRwOrd,
failure: AtomicReadOrd,
) -> AtomicRwOrd {
use AtomicReadOrd::*;
let (success_read, success_write) = success.split_memory_orderings();
let upgraded_success_read = match (success_read, failure) {
(_, SeqCst) | (SeqCst, _) => SeqCst,
(Acquire, _) | (_, Acquire) => Acquire,
(Relaxed, Relaxed) => Relaxed,
};
AtomicRwOrd::from_split_memory_orderings(upgraded_success_read, success_write)
}
impl AtomicRwOrd {
/// Split up an atomic read-write memory ordering into a separate read and write ordering.
pub(super) fn split_memory_orderings(self) -> (AtomicReadOrd, AtomicWriteOrd) {
match self {
AtomicRwOrd::Relaxed => (AtomicReadOrd::Relaxed, AtomicWriteOrd::Relaxed),
AtomicRwOrd::Acquire => (AtomicReadOrd::Acquire, AtomicWriteOrd::Relaxed),
AtomicRwOrd::Release => (AtomicReadOrd::Relaxed, AtomicWriteOrd::Release),
AtomicRwOrd::AcqRel => (AtomicReadOrd::Acquire, AtomicWriteOrd::Release),
AtomicRwOrd::SeqCst => (AtomicReadOrd::SeqCst, AtomicWriteOrd::SeqCst),
}
}
/// Split up an atomic read-write memory ordering into a separate read and write ordering.
fn from_split_memory_orderings(
read_ordering: AtomicReadOrd,
write_ordering: AtomicWriteOrd,
) -> Self {
match (read_ordering, write_ordering) {
(AtomicReadOrd::Relaxed, AtomicWriteOrd::Relaxed) => AtomicRwOrd::Relaxed,
(AtomicReadOrd::Acquire, AtomicWriteOrd::Relaxed) => AtomicRwOrd::Acquire,
(AtomicReadOrd::Relaxed, AtomicWriteOrd::Release) => AtomicRwOrd::Release,
(AtomicReadOrd::Acquire, AtomicWriteOrd::Release) => AtomicRwOrd::AcqRel,
(AtomicReadOrd::SeqCst, AtomicWriteOrd::SeqCst) => AtomicRwOrd::SeqCst,
_ =>
panic!(
"Unsupported memory ordering combination ({read_ordering:?}, {write_ordering:?})"
),
}
}
pub(super) fn to_genmc(self) -> MemOrdering {
match self {
AtomicRwOrd::Relaxed => MemOrdering::Relaxed,

109
src/tools/miri/src/concurrency/genmc/mod.rs
View file

@ -13,15 +13,16 @@ use tracing::{debug, info};
use self::global_allocations::{EvalContextExt as _, GlobalAllocationHandler};
use self::helper::{
MAX_ACCESS_SIZE, genmc_scalar_to_scalar, scalar_to_genmc_scalar, to_genmc_rmw_op,
MAX_ACCESS_SIZE, Warnings, emit_warning, genmc_scalar_to_scalar,
maybe_upgrade_compare_exchange_success_orderings, scalar_to_genmc_scalar, to_genmc_rmw_op,
};
use self::thread_id_map::ThreadIdMap;
use crate::concurrency::genmc::helper::split_access;
use crate::intrinsics::AtomicRmwOp;
use crate::{
AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriConfig,
MiriMachine, MiriMemoryKind, Scalar, TerminationInfo, ThreadId, ThreadManager, VisitProvenance,
VisitWith,
MiriMachine, MiriMemoryKind, NonHaltingDiagnostic, Scalar, TerminationInfo, ThreadId,
ThreadManager, VisitProvenance, VisitWith,
};
mod config;
@ -81,16 +82,22 @@ impl PerExecutionState {
}
}
#[derive(Debug)]
struct GlobalState {
/// Keep track of global allocations, to ensure they keep the same address across different executions, even if the order of allocations changes.
/// The `AllocId` for globals is stable across executions, so we can use it as an identifier.
global_allocations: GlobalAllocationHandler,
/// Cache for which warnings have already been shown to the user.
/// `None` if warnings are disabled.
warning_cache: Option<Warnings>,
}
impl GlobalState {
fn new(target_usize_max: u64) -> Self {
Self { global_allocations: GlobalAllocationHandler::new(target_usize_max) }
fn new(target_usize_max: u64, print_warnings: bool) -> Self {
Self {
global_allocations: GlobalAllocationHandler::new(target_usize_max),
warning_cache: print_warnings.then(Default::default),
}
}
}
@ -348,21 +355,91 @@ impl GenmcCtx {
/// `old_value` is the value that a non-atomic load would read here, or `None` if the memory is uninitalized.
pub(crate) fn atomic_compare_exchange<'tcx>(
&self,
_ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
_address: Size,
_size: Size,
_expected_old_value: Scalar,
_new_value: Scalar,
_success: AtomicRwOrd,
_fail: AtomicReadOrd,
_can_fail_spuriously: bool,
_old_value: Scalar,
ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
address: Size,
size: Size,
expected_old_value: Scalar,
new_value: Scalar,
success: AtomicRwOrd,
fail: AtomicReadOrd,
can_fail_spuriously: bool,
old_value: Scalar,
) -> InterpResult<'tcx, (Scalar, Option<Scalar>, bool)> {
assert!(
!self.get_alloc_data_races(),
"atomic compare-exchange with data race checking disabled."
);
throw_unsup_format!("FIXME(genmc): Add support for atomic compare_exchange.")
assert_ne!(0, size.bytes());
assert!(
size.bytes() <= MAX_ACCESS_SIZE,
"GenMC currently does not support atomic accesses larger than {} bytes (got {} bytes)",
MAX_ACCESS_SIZE,
size.bytes()
);
// Upgrade the success memory ordering to equal the failure ordering, since GenMC currently ignores the failure ordering.
// FIXME(genmc): remove this once GenMC properly supports the failure memory ordering.
let upgraded_success_ordering =
maybe_upgrade_compare_exchange_success_orderings(success, fail);
if let Some(warning_cache) = &self.global_state.warning_cache {
// FIXME(genmc): remove once GenMC supports failure memory ordering in `compare_exchange`.
let (effective_failure_ordering, _) =
upgraded_success_ordering.split_memory_orderings();
// Return a warning if the actual orderings don't match the upgraded ones.
if success != upgraded_success_ordering || effective_failure_ordering != fail {
emit_warning(ecx, &warning_cache.compare_exchange_failure_ordering, || {
NonHaltingDiagnostic::GenmcCompareExchangeOrderingMismatch {
success_ordering: success,
upgraded_success_ordering,
failure_ordering: fail,
effective_failure_ordering,
}
});
}
// FIXME(genmc): remove once GenMC implements spurious failures for `compare_exchange_weak`.
if can_fail_spuriously {
emit_warning(ecx, &warning_cache.compare_exchange_weak, || {
NonHaltingDiagnostic::GenmcCompareExchangeWeak
});
}
}
debug!(
"GenMC: atomic_compare_exchange, address: {address:?}, size: {size:?} (expect: {expected_old_value:?}, new: {new_value:?}, old_value: {old_value:?}, {success:?}, orderings: {fail:?}), can fail spuriously: {can_fail_spuriously}"
);
let thread_infos = self.exec_state.thread_id_manager.borrow();
let genmc_tid = thread_infos.get_genmc_tid(ecx.machine.threads.active_thread());
let cas_result = self.handle.borrow_mut().pin_mut().handle_compare_exchange(
genmc_tid,
address.bytes(),
size.bytes(),
scalar_to_genmc_scalar(ecx, expected_old_value)?,
scalar_to_genmc_scalar(ecx, new_value)?,
scalar_to_genmc_scalar(ecx, old_value)?,
upgraded_success_ordering.to_genmc(),
fail.to_genmc(),
can_fail_spuriously,
);
if let Some(error) = cas_result.error.as_ref() {
// FIXME(genmc): error handling
throw_ub_format!("{}", error.to_string_lossy());
}
let return_scalar = genmc_scalar_to_scalar(ecx, cas_result.old_value, size)?;
debug!(
"GenMC: atomic_compare_exchange: result: {cas_result:?}, returning scalar: {return_scalar:?}"
);
// The write can only be a co-maximal write if the CAS succeeded.
assert!(cas_result.is_success || !cas_result.is_coherence_order_maximal_write);
interp_ok((
return_scalar,
cas_result.is_coherence_order_maximal_write.then_some(new_value),
cas_result.is_success,
))
}
/// Inform GenMC about a non-atomic memory load

4
src/tools/miri/src/concurrency/genmc/run.rs
View file

@ -23,7 +23,9 @@ pub fn run_genmc_mode<'tcx>(
// There exists only one `global_state` per full run in GenMC mode.
// It is shared by all `GenmcCtx` in this run.
// FIXME(genmc): implement multithreading once GenMC supports it.
let global_state = Arc::new(GlobalState::new(tcx.target_usize_max()));
// FIXME(genmc): disable warnings in estimation mode once it is added.
let global_state =
Arc::new(GlobalState::new(tcx.target_usize_max(), /* print_warnings */ true));
let genmc_ctx = Rc::new(GenmcCtx::new(config, global_state));
// `rep` is used to report the progress, Miri will panic on wrap-around.

26
src/tools/miri/src/diagnostics.rs
View file

@ -141,6 +141,13 @@ pub enum NonHaltingDiagnostic {
ptr: Pointer,
},
ExternTypeReborrow,
GenmcCompareExchangeWeak,
GenmcCompareExchangeOrderingMismatch {
success_ordering: AtomicRwOrd,
upgraded_success_ordering: AtomicRwOrd,
failure_ordering: AtomicReadOrd,
effective_failure_ordering: AtomicReadOrd,
},
}
/// Level of Miri specific diagnostics
@ -637,6 +644,8 @@ impl<'tcx> MiriMachine<'tcx> {
("sharing memory with a native function".to_string(), DiagLevel::Warning),
ExternTypeReborrow =>
("reborrow of reference to `extern type`".to_string(), DiagLevel::Warning),
GenmcCompareExchangeWeak | GenmcCompareExchangeOrderingMismatch { .. } =>
("GenMC might miss possible behaviors of this code".to_string(), DiagLevel::Warning),
CreatedPointerTag(..)
| PoppedPointerTag(..)
| CreatedAlloc(..)
@ -675,6 +684,23 @@ impl<'tcx> MiriMachine<'tcx> {
format!("weak memory emulation: outdated value returned from load at {ptr}"),
ExternTypeReborrow =>
format!("reborrow of a reference to `extern type` is not properly supported"),
GenmcCompareExchangeWeak =>
"GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures."
.to_string(),
GenmcCompareExchangeOrderingMismatch {
success_ordering,
upgraded_success_ordering,
failure_ordering,
effective_failure_ordering,
} => {
let was_upgraded_msg = if success_ordering != upgraded_success_ordering {
format!("Success ordering '{success_ordering:?}' was upgraded to '{upgraded_success_ordering:?}' to match failure ordering '{failure_ordering:?}'")
} else {
assert_ne!(failure_ordering, effective_failure_ordering);
format!("Due to success ordering '{success_ordering:?}', the failure ordering '{failure_ordering:?}' is treated like '{effective_failure_ordering:?}'")
};
format!("GenMC currently does not model the failure ordering for `compare_exchange`. {was_upgraded_msg}. Miri with GenMC might miss bugs related to this memory access.")
}
};
let notes = match &e {

45
src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.rs Normal file
View file

@ -0,0 +1,45 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// Translated from GenMC's test `wrong/racy/MPU2+rels+rlx`.
// Test if Miri with GenMC can detect the data race on `X`.
// The data race only occurs if thread 1 finishes, then threads 3 and 4 run, then thread 2.
//
// This data race is hard to detect for Miri without GenMC, requiring -Zmiri-many-seeds=0..1024 at the time this test was created.
// FIXME(genmc): once Miri-GenMC error reporting is improved, ensure that it correctly points to the two spans involved in the data race.
#![no_main]
#[path = "../../../utils/genmc.rs"]
mod genmc;
use std::sync::atomic::AtomicUsize;
use std::sync::atomic::Ordering::*;
use genmc::spawn_pthread_closure;
static mut X: u64 = 0;
static Y: AtomicUsize = AtomicUsize::new(0);
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
unsafe {
let _t1 = spawn_pthread_closure(|| {
X = 1;
Y.store(0, Release);
Y.store(1, Relaxed);
});
let _t2 = spawn_pthread_closure(|| {
if Y.load(Relaxed) > 2 {
X = 2; //~ ERROR: Undefined Behavior: Non-atomic race
}
});
let _t3 = spawn_pthread_closure(|| {
let _ = Y.compare_exchange(2, 3, Relaxed, Relaxed);
});
let _t4 = spawn_pthread_closure(|| {
let _ = Y.compare_exchange(1, 2, Relaxed, Relaxed);
});
}
0
}

19
src/tools/miri/tests/genmc/fail/data_race/mpu2_rels_rlx.stderr Normal file
View file

@ -0,0 +1,19 @@
error: Undefined Behavior: Non-atomic race
--> tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC
|
LL | X = 2;
| ^^^^^ Undefined Behavior occurred here
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE on thread `unnamed-ID`:
= note: inside closure at tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC
= note: inside `<std::boxed::Box<{closure@tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC}> as std::ops::FnOnce<()>>::call_once` at RUSTLIB/alloc/src/boxed.rs:LL:CC
note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/fail/data_race/mpu2_rels_rlx.rs:LL:CC}>`
--> tests/genmc/fail/data_race/../../../utils/genmc.rs:LL:CC
|
LL | f();
| ^^^
error: aborting due to 1 previous error

13
src/tools/miri/tests/genmc/fail/loom/store_buffering.genmc.stderr Normal file
View file

@ -0,0 +1,13 @@
error: abnormal termination: the program aborted execution
--> tests/genmc/fail/loom/store_buffering.rs:LL:CC
|
LL | std::process::abort();
| ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
|
= note: BACKTRACE:
= note: inside `miri_start` at tests/genmc/fail/loom/store_buffering.rs:LL:CC
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
error: aborting due to 1 previous error

13
src/tools/miri/tests/genmc/fail/loom/store_buffering.non_genmc.stderr Normal file
View file

@ -0,0 +1,13 @@
error: abnormal termination: the program aborted execution
--> tests/genmc/fail/loom/store_buffering.rs:LL:CC
|
LL | std::process::abort();
| ^^^^^^^^^^^^^^^^^^^^^ abnormal termination occurred here
|
= note: BACKTRACE:
= note: inside `miri_start` at tests/genmc/fail/loom/store_buffering.rs:LL:CC
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
error: aborting due to 1 previous error

57
src/tools/miri/tests/genmc/fail/loom/store_buffering.rs Normal file
View file

@ -0,0 +1,57 @@
//@ revisions: non_genmc genmc
//@[genmc] compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// SPDX-License-Identifier: MIT
// SPDX-FileCopyrightText: Copyright (c) 2019 Carl Lerche
// This is the test `store_buffering` from `loom/test/litmus.rs`, adapted for Miri-GenMC.
// https://github.com/tokio-rs/loom/blob/dbf32b04bae821c64be44405a0bb72ca08741558/tests/litmus.rs
// This test shows the comparison between running Miri with or without GenMC.
// Without GenMC, Miri requires multiple iterations of the loop to detect the error.
#![no_main]
#[path = "../../../utils/genmc.rs"]
mod genmc;
use std::sync::atomic::AtomicUsize;
use std::sync::atomic::Ordering::*;
use crate::genmc::*;
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
// For normal Miri, we need multiple repetitions, but GenMC should find the bug with only 1.
const REPS: usize = if cfg!(non_genmc) { 128 } else { 1 };
for _ in 0..REPS {
// New atomics every iterations, so they don't influence each other.
let x = AtomicUsize::new(0);
let y = AtomicUsize::new(0);
// FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
x.store(0, Relaxed);
y.store(0, Relaxed);
let mut a: usize = 1234;
let mut b: usize = 1234;
unsafe {
let ids = [
spawn_pthread_closure(|| {
x.store(1, Relaxed);
a = y.load(Relaxed)
}),
spawn_pthread_closure(|| {
y.store(1, Relaxed);
b = x.load(Relaxed)
}),
];
join_pthreads(ids);
}
if (a, b) == (0, 0) {
std::process::abort(); //~ ERROR: abnormal termination
}
}
0
}

70
src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs Normal file
View file

@ -0,0 +1,70 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows -Zmiri-ignore-leaks
// Adapted from: `impl LazyKey`, `fn lazy_init`: rust/library/std/src/sys/thread_local/key/racy.rs
// Two threads race to initialize a key, which is just an index into an array in this test.
// The (Acquire, Release) orderings on the compare_exchange prevent any data races for reading from `VALUES[key]`.
// FIXME(genmc): GenMC does not model the failure ordering of compare_exchange currently.
// Miri thus upgrades the success ordering to prevent showing any false data races in cases like this one.
// Once GenMC supports the failure ordering, this test should work without the upgrading.
#![no_main]
#[path = "../../../utils/genmc.rs"]
mod genmc;
use std::sync::atomic::AtomicUsize;
use std::sync::atomic::Ordering::*;
use crate::genmc::*;
const KEY_SENTVAL: usize = usize::MAX;
static KEY: AtomicUsize = AtomicUsize::new(KEY_SENTVAL);
static mut VALUES: [usize; 2] = [0, 0];
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
// FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
KEY.store(KEY_SENTVAL, Relaxed);
unsafe {
let mut a = 0;
let mut b = 0;
let ids = [
spawn_pthread_closure(|| {
VALUES[0] = 42;
let key = get_or_init(0);
if key > 2 {
std::process::abort();
}
a = VALUES[key];
}),
spawn_pthread_closure(|| {
VALUES[1] = 1234;
let key = get_or_init(1);
if key > 2 {
std::process::abort();
}
b = VALUES[key];
}),
];
join_pthreads(ids);
if a != b {
std::process::abort();
}
}
0
}
fn get_or_init(key: usize) -> usize {
match KEY.compare_exchange(KEY_SENTVAL, key, Release, Acquire) {
// The CAS succeeded, so we've created the actual key.
Ok(_) => key,
// If someone beat us to the punch, use their key instead.
// The `Acquire` failure ordering means we synchronized with the `Release` compare_exchange in the thread that wrote the other key.
// We can thus read from `VALUES[other_key]` without a data race.
Err(other_key) => other_key,
}
}

22
src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.stderr Normal file
View file

@ -0,0 +1,22 @@
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Success ordering 'Release' was upgraded to 'AcqRel' to match failure ordering 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC
|
LL | match KEY.compare_exchange(KEY_SENTVAL, key, Release, Acquire) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE on thread `unnamed-ID`:
= note: inside `get_or_init` at tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC
note: inside closure
--> tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC
|
LL | let key = get_or_init(0);
| ^^^^^^^^^^^^^^
= note: inside `<std::boxed::Box<{closure@tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC}> as std::ops::FnOnce<()>>::call_once` at RUSTLIB/alloc/src/boxed.rs:LL:CC
note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs:LL:CC}>`
--> tests/genmc/pass/atomics/../../../utils/genmc.rs:LL:CC
|
LL | f();
| ^^^
(GenMC) Verification complete. No errors were detected.
Number of complete executions explored: 2

34
src/tools/miri/tests/genmc/pass/atomics/cas_simple.rs Normal file
View file

@ -0,0 +1,34 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// Test the basic functionality of compare_exchange.
#![no_main]
use std::sync::atomic::AtomicUsize;
use std::sync::atomic::Ordering::*;
static VALUE: AtomicUsize = AtomicUsize::new(0);
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
VALUE.store(1, SeqCst);
// Expect success:
if VALUE.compare_exchange(1, 2, SeqCst, SeqCst) != Ok(1) {
std::process::abort();
}
// New value should be written:
if 2 != VALUE.load(SeqCst) {
std::process::abort()
}
// Expect failure:
if VALUE.compare_exchange(1234, 42, SeqCst, SeqCst) != Err(2) {
std::process::abort();
}
// Value should be unchanged:
if 2 != VALUE.load(SeqCst) {
std::process::abort()
}
0
}

2
src/tools/miri/tests/genmc/pass/atomics/cas_simple.stderr Normal file
View file

@ -0,0 +1,2 @@
(GenMC) Verification complete. No errors were detected.
Number of complete executions explored: 1

4
src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs
View file

@ -57,9 +57,7 @@ fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
join_pthreads(ids);
// Print the values to check that we get all of them:
if writeln!(MiriStderr, "{results:?}").is_err() {
std::process::abort();
}
writeln!(MiriStderr, "{results:?}").unwrap_or_else(|_| std::process::abort());
0
}

67
src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs Normal file
View file

@ -0,0 +1,67 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// Translated from GenMC's "litmus/MPU2+rels+acqf" test.
#![no_main]
#[path = "../../../utils/genmc.rs"]
mod genmc;
#[path = "../../../utils/mod.rs"]
mod utils;
use std::fmt::Write;
use std::sync::atomic::AtomicU64;
use std::sync::atomic::Ordering::*;
use crate::genmc::*;
use crate::utils::*;
// Note: the GenMC equivalent of this test (genmc/tests/correct/litmus/MPU2+rels+acqf/mpu2+rels+acqf.c) uses non-atomic accesses for `X` with disabled race detection.
static X: AtomicU64 = AtomicU64::new(0);
static Y: AtomicU64 = AtomicU64::new(0);
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
// FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
X.store(0, Relaxed);
Y.store(0, Relaxed);
unsafe {
let mut a = Ok(1234);
let mut b = Ok(1234);
let mut c = 1234;
let ids = [
spawn_pthread_closure(|| {
X.store(1, Relaxed);
Y.store(0, Release);
Y.store(1, Relaxed);
}),
spawn_pthread_closure(|| {
a = Y.compare_exchange(2, 3, Relaxed, Relaxed);
}),
spawn_pthread_closure(|| {
b = Y.compare_exchange(1, 2, Relaxed, Relaxed);
}),
spawn_pthread_closure(|| {
c = Y.load(Acquire);
if c > 2 {
std::sync::atomic::fence(Acquire);
X.store(2, Relaxed);
}
}),
];
join_pthreads(ids);
// Print the values to check that we get all of them:
writeln!(
MiriStderr,
"X={}, Y={}, a={a:?}, b={b:?}, c={c}",
X.load(Relaxed),
Y.load(Relaxed)
)
.unwrap_or_else(|_| std::process::abort());
0
}
}

38
src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.stderr Normal file
View file

@ -0,0 +1,38 @@
X=1, Y=2, a=Err(1), b=Ok(1), c=2
X=1, Y=2, a=Err(1), b=Ok(1), c=1
X=1, Y=2, a=Err(1), b=Ok(1), c=0
X=1, Y=2, a=Err(1), b=Ok(1), c=0
X=2, Y=3, a=Ok(2), b=Ok(1), c=3
X=1, Y=3, a=Ok(2), b=Ok(1), c=3
X=1, Y=3, a=Ok(2), b=Ok(1), c=2
X=1, Y=3, a=Ok(2), b=Ok(1), c=1
X=1, Y=3, a=Ok(2), b=Ok(1), c=0
X=1, Y=3, a=Ok(2), b=Ok(1), c=0
X=1, Y=1, a=Err(1), b=Err(0), c=1
X=1, Y=1, a=Err(1), b=Err(0), c=0
X=1, Y=1, a=Err(1), b=Err(0), c=0
X=1, Y=1, a=Err(1), b=Err(0), c=1
X=1, Y=1, a=Err(1), b=Err(0), c=0
X=1, Y=1, a=Err(1), b=Err(0), c=0
X=1, Y=2, a=Err(0), b=Ok(1), c=2
X=1, Y=2, a=Err(0), b=Ok(1), c=1
X=1, Y=2, a=Err(0), b=Ok(1), c=0
X=1, Y=2, a=Err(0), b=Ok(1), c=0
X=1, Y=1, a=Err(0), b=Err(0), c=1
X=1, Y=1, a=Err(0), b=Err(0), c=0
X=1, Y=1, a=Err(0), b=Err(0), c=0
X=1, Y=1, a=Err(0), b=Err(0), c=1
X=1, Y=1, a=Err(0), b=Err(0), c=0
X=1, Y=1, a=Err(0), b=Err(0), c=0
X=1, Y=2, a=Err(0), b=Ok(1), c=2
X=1, Y=2, a=Err(0), b=Ok(1), c=1
X=1, Y=2, a=Err(0), b=Ok(1), c=0
X=1, Y=2, a=Err(0), b=Ok(1), c=0
X=1, Y=1, a=Err(0), b=Err(0), c=1
X=1, Y=1, a=Err(0), b=Err(0), c=0
X=1, Y=1, a=Err(0), b=Err(0), c=0
X=1, Y=1, a=Err(0), b=Err(0), c=1
X=1, Y=1, a=Err(0), b=Err(0), c=0
X=1, Y=1, a=Err(0), b=Err(0), c=0
(GenMC) Verification complete. No errors were detected.
Number of complete executions explored: 36

7
src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs
View file

@ -55,11 +55,8 @@ fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
join_pthreads(ids);
// Print the values to check that we get all of them:
if writeln!(MiriStderr, "a={a}, b={b}, X={}, Y={}", X.load(Relaxed), Y.load(Relaxed))
.is_err()
{
std::process::abort();
}
writeln!(MiriStderr, "a={a}, b={b}, X={}, Y={}", X.load(Relaxed), Y.load(Relaxed))
.unwrap_or_else(|_| std::process::abort());
0
}
}

37
src/tools/miri/tests/genmc/pass/litmus/casdep.rs Normal file
View file

@ -0,0 +1,37 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// Translated from GenMC's test "litmus/casdep".
#![no_main]
#[path = "../../../utils/genmc.rs"]
mod genmc;
use std::sync::atomic::AtomicU64;
use std::sync::atomic::Ordering::*;
use crate::genmc::*;
static X: AtomicU64 = AtomicU64::new(0);
static Y: AtomicU64 = AtomicU64::new(0);
static Z: AtomicU64 = AtomicU64::new(0);
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
// FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
X.store(0, Relaxed);
Y.store(0, Relaxed);
Z.store(0, Relaxed);
unsafe {
spawn_pthread_closure(|| {
let a = X.load(Relaxed);
let _b = Y.compare_exchange(a, 1, Relaxed, Relaxed);
Z.store(a, Relaxed);
});
spawn_pthread_closure(|| {
Y.store(2, Relaxed);
});
0
}
}

2
src/tools/miri/tests/genmc/pass/litmus/casdep.stderr Normal file
View file

@ -0,0 +1,2 @@
(GenMC) Verification complete. No errors were detected.
Number of complete executions explored: 2

34
src/tools/miri/tests/genmc/pass/litmus/ccr.rs Normal file
View file

@ -0,0 +1,34 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// Translated from GenMC's test "litmus/ccr".
#![no_main]
#[path = "../../../utils/genmc.rs"]
mod genmc;
use std::sync::atomic::AtomicU64;
use std::sync::atomic::Ordering::*;
use crate::genmc::*;
static X: AtomicU64 = AtomicU64::new(0);
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
// FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
X.store(0, Relaxed);
unsafe {
spawn_pthread_closure(|| {
let expected = 0;
let _ = X.compare_exchange(expected, 42, Relaxed, Relaxed);
});
spawn_pthread_closure(|| {
let expected = 0;
let _ = X.compare_exchange(expected, 17, Relaxed, Relaxed);
X.load(Relaxed);
});
0
}
}

2
src/tools/miri/tests/genmc/pass/litmus/ccr.stderr Normal file
View file

@ -0,0 +1,2 @@
(GenMC) Verification complete. No errors were detected.
Number of complete executions explored: 2

35
src/tools/miri/tests/genmc/pass/litmus/cii.rs Normal file
View file

@ -0,0 +1,35 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// Translated from GenMC's test "litmus/cii".
#![no_main]
#[path = "../../../utils/genmc.rs"]
mod genmc;
use std::sync::atomic::AtomicU64;
use std::sync::atomic::Ordering::*;
use crate::genmc::*;
static X: AtomicU64 = AtomicU64::new(0);
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
// FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
X.store(0, Relaxed);
unsafe {
spawn_pthread_closure(|| {
let expected = 1;
let _ = X.compare_exchange(expected, 2, Relaxed, Relaxed);
});
spawn_pthread_closure(|| {
X.fetch_add(1, Relaxed);
});
spawn_pthread_closure(|| {
X.fetch_add(1, Relaxed);
});
0
}
}

2
src/tools/miri/tests/genmc/pass/litmus/cii.stderr Normal file
View file

@ -0,0 +1,2 @@
(GenMC) Verification complete. No errors were detected.
Number of complete executions explored: 6