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

Merge pull request #4611 from Patrick-6/miri-genmc-temporal-mixing

Browse source 
Add support for temporal mixing of atomic and non-atomic accesses in GenMC mode
This commit is contained in:
Ralf Jung 2025-10-01 12:02:45 +00:00 • committed by GitHub
commit 1c16821db8
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
52 changed files with 978 additions and 191 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tools/miri/genmc-sys/build.rs
View file

@ -28,7 +28,7 @@ mod downloading {
/// The GenMC repository the we get our commit from.
pub(crate) const GENMC_GITHUB_URL: &str = "https://gitlab.inf.ethz.ch/public-plf/genmc.git";
/// The GenMC commit we depend on. It must be available on the specified GenMC repository.
pub(crate) const GENMC_COMMIT: &str = "cd01c12032bdd71df742b41c7817f99acc72e7ab";
pub(crate) const GENMC_COMMIT: &str = "ce775ccd7866db820fa12ffca66463087a11dd96";
/// Ensure that a local GenMC repo is present and set to the correct commit.
/// Return the path of the GenMC repo and whether the checked out commit was changed.

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

@ -214,9 +214,10 @@ struct MiriGenmcShim : private GenMCDriver {
* Automatically calls `inc_pos` and `dec_pos` where needed for the given thread.
*/
template <EventLabel::EventLabelKind k, typename... Ts>
auto handle_load_reset_if_none(ThreadId tid, Ts&&... params) -> HandleResult<SVal> {
auto handle_load_reset_if_none(ThreadId tid, std::optional<SVal> old_val, Ts&&... params)
-> HandleResult<SVal> {
const auto pos = inc_pos(tid);
const auto ret = GenMCDriver::handleLoad<k>(pos, std::forward<Ts>(params)...);
const auto ret = GenMCDriver::handleLoad<k>(pos, old_val, std::forward<Ts>(params)...);
// If we didn't get a value, we have to reset the index of the current thread.
if (!std::holds_alternative<SVal>(ret)) {
dec_pos(tid);
@ -274,6 +275,12 @@ inline SVal to_sval(GenmcScalar scalar) {
ERROR_ON(!scalar.is_init, "Cannot convert an uninitialized `GenmcScalar` into an `SVal`\n");
return SVal(scalar.value, scalar.extra);
}
inline std::optional<SVal> try_to_sval(GenmcScalar scalar) {
if (scalar.is_init)
return { SVal(scalar.value, scalar.extra) };
return std::nullopt;
}
} // namespace GenmcScalarExt
namespace LoadResultExt {

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

@ -49,6 +49,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
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),
@ -74,6 +75,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
const auto pos = inc_pos(thread_id);
const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
pos,
GenmcScalarExt::try_to_sval(old_val),
ord,
SAddr(address),
ASize(size),
@ -84,15 +86,13 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
if (const auto* err = std::get_if<VerificationError>(&ret))
return StoreResultExt::from_error(format_error(*err));
if (!std::holds_alternative<std::monostate>(ret))
ERROR("store returned unexpected result");
// FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once
// available).
const auto& g = getExec().getGraph();
return StoreResultExt::ok(
/* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == pos
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
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) {
@ -117,6 +117,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
// `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),
@ -139,6 +140,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
const auto storePos = inc_pos(thread_id);
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
storePos,
GenmcScalarExt::try_to_sval(old_val),
ordering,
SAddr(address),
ASize(size),
@ -148,16 +150,15 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
if (const auto* err = std::get_if<VerificationError>(&store_ret))
return ReadModifyWriteResultExt::from_error(format_error(*err));
const auto* store_ret_val = std::get_if<std::monostate>(&store_ret);
ERROR_ON(nullptr == store_ret_val, "Unimplemented: RMW store returned unexpected result.");
// FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once
// available).
const auto& g = getExec().getGraph();
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
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 */ g.co_max(SAddr(address))->getPos() == storePos
*is_coherence_order_maximal_write
);
}
@ -183,6 +184,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
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),
@ -203,6 +205,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
const auto storePos = inc_pos(thread_id);
const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::CasWrite>(
storePos,
GenmcScalarExt::try_to_sval(old_val),
success_ordering,
SAddr(address),
ASize(size),
@ -211,19 +214,12 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
);
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);
const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
ERROR_ON(
nullptr == store_ret_val,
nullptr == is_coherence_order_maximal_write,
"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
);
return CompareExchangeResultExt::success(read_old_val, *is_coherence_order_maximal_write);
}
/**** Memory (de)allocation ****/

3
src/tools/miri/tests/genmc/fail/atomics/atomic_ptr_double_free.rs
View file

@ -22,9 +22,6 @@ unsafe fn free(ptr: *mut u64) {
#[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(std::ptr::null_mut(), SeqCst);
unsafe {
let ids = [
spawn_pthread_closure(|| {

3
src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_alloc_race.rs
View file

@ -23,9 +23,6 @@ static X: AtomicPtr<u64> = AtomicPtr::new(std::ptr::null_mut());
#[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(std::ptr::null_mut(), SeqCst);
unsafe {
let ids = [
spawn_pthread_closure(|| {

3
src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_dealloc_write_race.rs
View file

@ -20,9 +20,6 @@ static mut Y: u64 = 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(std::ptr::null_mut(), SeqCst);
unsafe {
let ids = [
spawn_pthread_closure(|| {

3
src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_write_dealloc_race.rs
View file

@ -24,9 +24,6 @@ static Y: AtomicPtr<u64> = AtomicPtr::new(std::ptr::null_mut());
#[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(std::ptr::null_mut(), SeqCst);
unsafe {
let ids = [
spawn_pthread_closure(|| {

3
src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs
View file

@ -42,9 +42,6 @@ impl BuggyInc {
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
unsafe {
static BUGGY_INC: BuggyInc = BuggyInc::new();
// FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
BUGGY_INC.num.store(0, Relaxed);
let ids = [
spawn_pthread_closure(|| {
BUGGY_INC.inc();

27
src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_ops.rs
View file

@ -37,18 +37,22 @@ unsafe fn pointers_equal(a: *mut u64, b: *mut u64) {
unsafe fn test_load_store_exchange() {
let atomic_ptr: AtomicPtr<u64> = AtomicPtr::new(&raw mut X);
// FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
// FIXME(genmc): Add test cases with temporal mixing of atomics/non-atomics.
atomic_ptr.store(&raw mut X, SeqCst);
// Load can read the initial value.
// Atomic load can read the initial value.
pointers_equal(atomic_ptr.load(SeqCst), &raw mut X);
// Store works as expected.
// Atomic store works as expected.
atomic_ptr.store(&raw mut Y, SeqCst);
pointers_equal(atomic_ptr.load(SeqCst), &raw mut Y);
// We can read the value of the atomic store non-atomically.
pointers_equal(*atomic_ptr.as_ptr(), &raw mut Y);
// We can read the value of a non-atomic store atomically.
*atomic_ptr.as_ptr() = &raw mut X;
pointers_equal(atomic_ptr.load(SeqCst), &raw mut X);
// Atomic swap must return the old value and store the new one.
*atomic_ptr.as_ptr() = &raw mut Y; // Test that we can read this non-atomic store using `swap`.
pointers_equal(atomic_ptr.swap(&raw mut X, SeqCst), &raw mut Y);
pointers_equal(*atomic_ptr.as_ptr(), &raw mut X);
pointers_equal(atomic_ptr.load(SeqCst), &raw mut X);
// Failing compare_exchange (wrong expected pointer).
@ -56,11 +60,17 @@ unsafe fn test_load_store_exchange() {
Ok(_ptr) => std::process::abort(),
Err(ptr) => pointers_equal(ptr, &raw mut X),
}
// Non-atomic read value should also be unchanged by a failing compare_exchange.
pointers_equal(*atomic_ptr.as_ptr(), &raw mut X);
// Failing compare_exchange (null).
match atomic_ptr.compare_exchange(std::ptr::null_mut(), std::ptr::null_mut(), SeqCst, SeqCst) {
Ok(_ptr) => std::process::abort(),
Err(ptr) => pointers_equal(ptr, &raw mut X),
}
// Non-atomic read value should also be unchanged by a failing compare_exchange.
pointers_equal(*atomic_ptr.as_ptr(), &raw mut X);
// Successful compare_exchange.
match atomic_ptr.compare_exchange(&raw mut X, &raw mut Y, SeqCst, SeqCst) {
Ok(ptr) => pointers_equal(ptr, &raw mut X),
@ -68,15 +78,13 @@ unsafe fn test_load_store_exchange() {
}
// compare_exchange should update the pointer.
pointers_equal(atomic_ptr.load(SeqCst), &raw mut Y);
pointers_equal(*atomic_ptr.as_ptr(), &raw mut Y);
}
unsafe fn test_add_sub() {
const LEN: usize = 16;
let mut array: [u64; LEN] = std::array::from_fn(|i| i as u64);
let atomic_ptr: AtomicPtr<u64> = AtomicPtr::new(&raw mut array[0]);
// FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
atomic_ptr.store(&raw mut array[0], SeqCst);
// Each element of the array should be reachable using `fetch_ptr_add`.
// All pointers must stay valid.
@ -110,10 +118,7 @@ unsafe fn test_and_or_xor() {
let mut array = AlignedArray(std::array::from_fn(|i| i as u64 * 10));
let array_ptr = &raw mut array.0[0];
let atomic_ptr: AtomicPtr<u64> = AtomicPtr::new(array_ptr);
// FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
atomic_ptr.store(array_ptr, SeqCst);
// Test no-op arguments.
assert_equals(array_ptr, atomic_ptr.fetch_or(0, SeqCst));

3
src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_roundtrip.rs
View file

@ -23,9 +23,6 @@ static mut X: [u8; 16] = [0; 16];
#[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.
PTR.store(std::ptr::null_mut(), SeqCst);
unsafe {
let ids = [
spawn_pthread_closure(|| {

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

@ -26,9 +26,6 @@ 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;

41
src/tools/miri/tests/genmc/pass/atomics/mixed_atomic_non_atomic.rs Normal file
View file

@ -0,0 +1,41 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// Test that we can read the value of a non-atomic store atomically and an of an atomic value non-atomically.
#![no_main]
use std::sync::atomic::Ordering::*;
use std::sync::atomic::{AtomicI8, AtomicU64};
static X: AtomicU64 = AtomicU64::new(1234);
static Y: AtomicI8 = AtomicI8::new(0xB);
fn assert_equals<T: Eq>(a: T, b: T) {
if a != b {
std::process::abort();
}
}
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
// 8 byte unsigned integer:
// Read initial value.
assert_equals(1234, X.load(Relaxed));
// Atomic store, non-atomic load.
X.store(0xFFFF, Relaxed);
assert_equals(0xFFFF, unsafe { *X.as_ptr() });
// Non-atomic store, atomic load.
unsafe { *X.as_ptr() = 0xAAAA };
assert_equals(0xAAAA, X.load(Relaxed));
// 1 byte signed integer:
// Read initial value.
assert_equals(0xB, Y.load(Relaxed));
// Atomic store, non-atomic load.
Y.store(42, Relaxed);
assert_equals(42, unsafe { *Y.as_ptr() });
// Non-atomic store, atomic load.
unsafe { *Y.as_ptr() = -42 };
assert_equals(-42, Y.load(Relaxed));
0
}

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

@ -0,0 +1,2 @@
Running GenMC Verification...
Verification complete with 1 executions. No errors found.

41
src/tools/miri/tests/genmc/pass/atomics/read_initial_value.rs Normal file
View file

@ -0,0 +1,41 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// Test that we can read the initial value of global, heap and stack allocations in GenMC mode.
#![no_main]
use std::sync::atomic::AtomicU64;
use std::sync::atomic::Ordering::*;
static X: AtomicU64 = AtomicU64::new(1234);
#[unsafe(no_mangle)]
fn miri_start(_argc: isize, _argv: *const *const u8) -> isize {
// Read initial value of global allocation.
if 1234 != unsafe { *X.as_ptr() } {
std::process::abort();
}
if 1234 != X.load(SeqCst) {
std::process::abort();
}
// Read initial value of stack allocation.
let a = AtomicU64::new(0xBB);
if 0xBB != unsafe { *a.as_ptr() } {
std::process::abort();
}
if 0xBB != a.load(SeqCst) {
std::process::abort();
}
// Read initial value of heap allocation.
let b = Box::new(AtomicU64::new(0xCCC));
if 0xCCC != unsafe { *b.as_ptr() } {
std::process::abort();
}
if 0xCCC != b.load(SeqCst) {
std::process::abort();
}
0
}

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

@ -0,0 +1,2 @@
Running GenMC Verification...
Verification complete with 1 executions. No errors found.

5
src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs
View file

@ -21,11 +21,8 @@ fn assert_eq<T: Eq>(x: T, y: T) {
macro_rules! test_rmw_edge_cases {
($int:ty, $atomic:ty) => {{
let x = <$atomic>::new(123);
// FIXME(genmc,HACK): remove this initializing write once Miri-GenMC supports mixed atomic-non-atomic accesses.
x.store(123, ORD);
// MAX, ADD
let x = <$atomic>::new(123);
assert_eq(123, x.fetch_max(0, ORD)); // `max` keeps existing value
assert_eq(123, x.fetch_max(<$int>::MAX, ORD)); // `max` stores the new value
assert_eq(<$int>::MAX, x.fetch_add(10, ORD)); // `fetch_add` should be wrapping

8
src/tools/miri/tests/genmc/pass/data-structures/ms_queue_dynamic.rs
View file

@ -70,11 +70,6 @@ impl MyStack {
(*dummy).next = AtomicPtr::new(std::ptr::null_mut());
self.head = AtomicPtr::new(dummy);
self.tail = AtomicPtr::new(dummy);
// FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
(*dummy).next.store(std::ptr::null_mut(), Relaxed);
self.head.store(dummy, Relaxed);
self.tail.store(dummy, Relaxed);
}
pub unsafe fn clear_queue(&mut self, _num_threads: usize) {
@ -93,9 +88,6 @@ impl MyStack {
(*node).value = value;
(*node).next = AtomicPtr::new(std::ptr::null_mut());
// FIXME(genmc,HACK): remove these initializing writes once Miri-GenMC supports mixed atomic-non-atomic accesses.
(*node).next.store(std::ptr::null_mut(), Relaxed);
loop {
tail = self.tail.load(Acquire);
let next = (*tail).next.load(Acquire);

3
src/tools/miri/tests/genmc/pass/data-structures/treiber_stack_dynamic.rs
View file

@ -104,9 +104,6 @@ impl MyStack {
#[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.
unsafe { STACK.top.store(std::ptr::null_mut(), Relaxed) };
// We try multiple different parameters for the number and types of threads:
let (readers, writers) = if cfg!(any(default_R1W3, spinloop_assume_R1W3)) {
(1, 3)

4
src/tools/miri/tests/genmc/pass/intercept/spinloop_assume.rs
View file

@ -58,10 +58,6 @@ fn spin_until(value: u64) {
#[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.
unsafe { X = 0 };
FLAG.store(0, Relaxed);
unsafe {
let t0 = || {
X = 42;

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

@ -17,10 +17,6 @@ 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 = 1234;
let mut b = 1234;

4
src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs
View file

@ -17,10 +17,6 @@ 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 = 1234;
let mut b = 1234;

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

@ -28,10 +28,6 @@ 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 results = [1234; 5];
let ids = [

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

@ -17,10 +17,6 @@ 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 = 1234;
let mut b = 1234;

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

@ -17,10 +17,6 @@ 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 = 1234;
let mut b = 1234;

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

@ -22,10 +22,6 @@ 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);

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

@ -18,10 +18,6 @@ use crate::genmc::*;
#[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 {
spawn_pthread_closure(|| {
X.store(1, Relaxed);

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

@ -18,10 +18,6 @@ use crate::genmc::*;
#[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 {
spawn_pthread_closure(|| {
X.store(1, Relaxed);

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

@ -17,10 +17,6 @@ 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 = 1234;
let mut b = 1234;

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

@ -31,10 +31,6 @@ 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 = 1234;
let mut b = 1234;

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

@ -18,11 +18,6 @@ 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);

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

@ -16,9 +16,6 @@ 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;

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

@ -16,9 +16,6 @@ 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;

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

@ -6,7 +6,6 @@
#[path = "../../../utils/genmc.rs"]
mod genmc;
use std::sync::atomic::AtomicU64;
use std::sync::atomic::Ordering::*;
@ -16,9 +15,6 @@ 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 {
let mut a = 1234;
let mut b = 1234;

3
src/tools/miri/tests/genmc/pass/litmus/corr0.rs
View file

@ -16,9 +16,6 @@ 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 {
let mut a = 1234;
let mut b = 1234;

3
src/tools/miri/tests/genmc/pass/litmus/corr1.rs
View file

@ -16,9 +16,6 @@ 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 {
let mut a = 1234;
let mut b = 1234;

3
src/tools/miri/tests/genmc/pass/litmus/corr2.rs
View file

@ -16,9 +16,6 @@ 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 {
let mut a = 1234;
let mut b = 1234;

3
src/tools/miri/tests/genmc/pass/litmus/corw.rs
View file

@ -16,9 +16,6 @@ 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 {
let mut a = 1234;
let ids = [

5
src/tools/miri/tests/genmc/pass/litmus/cumul-release.rs
View file

@ -18,11 +18,6 @@ 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 {
let mut a = 1234;
let mut b = 1234;

3
src/tools/miri/tests/genmc/pass/litmus/default.rs
View file

@ -16,9 +16,6 @@ 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 {
let mut a = 1234;
let mut b = 1234;

5
src/tools/miri/tests/genmc/pass/litmus/detour.rs
View file

@ -22,11 +22,6 @@ static Z: AtomicI64 = AtomicI64::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 {
// Make these static so we can exit the main thread while the other threads still run.
// If these are `let mut` like the other tests, this will cause a use-after-free bug.

3
src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs
View file

@ -16,9 +16,6 @@ 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 {
let mut result = [1234; 4];
let ids = [

3
src/tools/miri/tests/genmc/pass/litmus/inc2w.rs
View file

@ -16,9 +16,6 @@ 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 {
let ids = [
spawn_pthread_closure(|| {

163
src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr Normal file
View file

@ -0,0 +1,163 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u64>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU64::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::option::Option::<std::thread::ThreadId>::unwrap_or_else::<{closure@std::thread::current::id::get_or_init::{closure#0}}>` at RUSTLIB/core/src/option.rs:LL:CC
= note: inside `std::thread::current::id::get_or_init` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::thread::current::current_id` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::rt::init` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::Arc::<i32>::downgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let weak = Arc::downgrade(&data_clone);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::Arc::<i32>::downgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let weak = Arc::downgrade(&data_clone);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
... |
LL | | });
| |______^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
... |
LL | | });
| |______^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::get_mut` at RUSTLIB/alloc/src/sync.rs:LL:CC
= note: inside `std::thread::JoinInner::<'_, ()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
= note: inside `std::thread::JoinHandle::<()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | handle.join().unwrap();
| ^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU32::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::sync::PLATFORM::futex::Once::call` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::Once::call_once::<{closure@std::rt::cleanup::{closure#0}}>` at RUSTLIB/std/src/sync/poison/once.rs:LL:CC
= note: inside `std::rt::cleanup` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange::<*mut i32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicPtr::<i32>::compare_exchange` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::exit_guard::unique_thread_exit` at RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
Verification complete with 4 executions. No errors found.

49
src/tools/miri/tests/genmc/pass/std/arc.rs Normal file
View file

@ -0,0 +1,49 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
//@revisions: check_count try_upgrade
// Check that various operations on `std::sync::Arc` are handled properly in GenMC mode.
//
// The number of explored executions in the expected output of this test may change if
// the implementation of `Arc` is ever changed, or additional optimizations are added to GenMC mode.
//
// The revision that tries to upgrade the `Weak` should never explore fewer executions compared to the revision that just accesses the `strong_count`,
// since `upgrade` needs to access the `strong_count` internally.
// There should always be more than 1 execution for both, since there is always the possibilility that the `Arc` has already been dropped, or it hasn't.
use std::sync::Arc;
fn main() {
let data = Arc::new(42);
// Clone the Arc, drop the original, check that memory still valid.
let data_clone = Arc::clone(&data);
drop(data);
assert!(*data_clone == 42);
// Create a Weak reference.
let weak = Arc::downgrade(&data_clone);
// Spawn a thread that uses the Arc.
let weak_ = weak.clone();
let handle = std::thread::spawn(move || {
// Try to upgrade weak reference.
// Depending on execution schedule, this may fail or succeed depending on whether this runs before or after the `drop` in the main thread.
#[cfg(check_count)]
let _strong_count = weak_.strong_count();
#[cfg(try_upgrade)]
if let Some(strong) = weak_.upgrade() {
assert_eq!(*strong, 42);
}
});
// Drop the last strong reference to the data.
drop(data_clone);
// Wait for the thread to finish.
handle.join().unwrap();
// The upgrade should fail now (all Arcs dropped).
assert!(weak.upgrade().is_none());
}

191
src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr Normal file
View file

@ -0,0 +1,191 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u64>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU64::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::option::Option::<std::thread::ThreadId>::unwrap_or_else::<{closure@std::thread::current::id::get_or_init::{closure#0}}>` at RUSTLIB/core/src/option.rs:LL:CC
= note: inside `std::thread::current::id::get_or_init` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::thread::current::current_id` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::rt::init` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::Arc::<i32>::downgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let weak = Arc::downgrade(&data_clone);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acquire, Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::Arc::<i32>::downgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let weak = Arc::downgrade(&data_clone);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
... |
LL | | });
| |______^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | let handle = std::thread::spawn(move || {
| __________________^
... |
LL | | });
| |______^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::get_mut` at RUSTLIB/alloc/src/sync.rs:LL:CC
= note: inside `std::thread::JoinInner::<'_, ()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
= note: inside `std::thread::JoinHandle::<()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | handle.join().unwrap();
| ^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU32::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::sync::PLATFORM::futex::Once::call` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::Once::call_once::<{closure@std::rt::cleanup::{closure#0}}>` at RUSTLIB/std/src/sync/poison/once.rs:LL:CC
= note: inside `std::rt::cleanup` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange::<*mut i32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicPtr::<i32>::compare_exchange` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::exit_guard::unique_thread_exit` at RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if self.inner()?.strong.fetch_update(Acquire, Relaxed, checked_increment).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE on thread `unnamed-ID`:
= note: inside `std::sync::Weak::<i32>::upgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
note: inside closure
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | if let Some(strong) = weak_.upgrade() {
| ^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if self.inner()?.strong.fetch_update(Acquire, Relaxed, checked_increment).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE on thread `unnamed-ID`:
= note: inside `std::sync::Weak::<i32>::upgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
note: inside closure
--> tests/genmc/pass/std/arc.rs:LL:CC
|
LL | if let Some(strong) = weak_.upgrade() {
| ^^^^^^^^^^^^^^^
Verification complete with 7 executions. No errors found.

5
src/tools/miri/tests/genmc/pass/std/empty_main.rs Normal file
View file

@ -0,0 +1,5 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// A lot of code runs before main, which we should be able to handle in GenMC mode.
fn main() {}

60
src/tools/miri/tests/genmc/pass/std/empty_main.stderr Normal file
View file

@ -0,0 +1,60 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u64>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU64::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::option::Option::<std::thread::ThreadId>::unwrap_or_else::<{closure@std::thread::current::id::get_or_init::{closure#0}}>` at RUSTLIB/core/src/option.rs:LL:CC
= note: inside `std::thread::current::id::get_or_init` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::thread::current::current_id` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::rt::init` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU32::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::sync::PLATFORM::futex::Once::call` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::Once::call_once::<{closure@std::rt::cleanup::{closure#0}}>` at RUSTLIB/std/src/sync/poison/once.rs:LL:CC
= note: inside `std::rt::cleanup` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange::<*mut i32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicPtr::<i32>::compare_exchange` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::exit_guard::unique_thread_exit` at RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
Verification complete with 1 executions. No errors found.

13
src/tools/miri/tests/genmc/pass/std/spawn_std_threads.rs Normal file
View file

@ -0,0 +1,13 @@
//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
// We should be able to spawn and join standard library threads in GenMC mode.
// Since these threads do nothing, we should only explore 1 program execution.
const N: usize = 2;
fn main() {
let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect();
handles.into_iter().for_each(|handle| handle.join().unwrap());
}
fn thread_func() {}

167
src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr Normal file
View file

@ -0,0 +1,167 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u64>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU64::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::option::Option::<std::thread::ThreadId>::unwrap_or_else::<{closure@std::thread::current::id::get_or_init::{closure#0}}>` at RUSTLIB/core/src/option.rs:LL:CC
= note: inside `std::thread::current::id::get_or_init` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::thread::current::current_id` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::rt::init` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside closure
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= note: inside closure at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC
= note: inside `<std::ops::Range<usize> as std::iter::Iterator>::fold::<(), {closure@std::iter::adapters::map::map_fold<usize, std::thread::JoinHandle<()>, (), {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}, {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::for_each::<{closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `std::vec::Vec::<std::thread::JoinHandle<()>>::extend_trusted::<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_extend::SpecExtend<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::spec_extend` at RUSTLIB/alloc/src/vec/spec_extend.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_from_iter_nested::SpecFromIterNested<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter_nested.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_from_iter::SpecFromIter<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::iter::FromIterator<std::thread::JoinHandle<()>>>::from_iter::<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::collect::<std::vec::Vec<std::thread::JoinHandle<()>>>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside closure
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= note: inside closure at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC
= note: inside `<std::ops::Range<usize> as std::iter::Iterator>::fold::<(), {closure@std::iter::adapters::map::map_fold<usize, std::thread::JoinHandle<()>, (), {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}, {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::for_each::<{closure@std::vec::Vec<std::thread::JoinHandle<()>>::extend_trusted<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>::{closure#0}}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `std::vec::Vec::<std::thread::JoinHandle<()>>::extend_trusted::<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_extend::SpecExtend<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::spec_extend` at RUSTLIB/alloc/src/vec/spec_extend.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_from_iter_nested::SpecFromIterNested<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter_nested.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::vec::spec_from_iter::SpecFromIter<std::thread::JoinHandle<()>, std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>>::from_iter` at RUSTLIB/alloc/src/vec/spec_from_iter.rs:LL:CC
= note: inside `<std::vec::Vec<std::thread::JoinHandle<()>> as std::iter::FromIterator<std::thread::JoinHandle<()>>>::from_iter::<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC
= note: inside `<std::iter::Map<std::ops::Range<usize>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::collect::<std::vec::Vec<std::thread::JoinHandle<()>>>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | let handles: Vec<_> = (0..N).map(|_| std::thread::spawn(thread_func)).collect();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::get_mut` at RUSTLIB/alloc/src/sync.rs:LL:CC
= note: inside `std::thread::JoinInner::<'_, ()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
= note: inside `std::thread::JoinHandle::<()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside closure
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | handles.into_iter().for_each(|handle| handle.join().unwrap());
| ^^^^^^^^^^^^^
= note: inside closure at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside `<std::vec::IntoIter<std::thread::JoinHandle<()>> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>::{closure#0}}>` at RUSTLIB/alloc/src/vec/into_iter.rs:LL:CC
= note: inside `<std::vec::IntoIter<std::thread::JoinHandle<()>> as std::iter::Iterator>::for_each::<{closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/spawn_std_threads.rs:LL:CC
|
LL | handles.into_iter().for_each(|handle| handle.join().unwrap());
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU32::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::sync::PLATFORM::futex::Once::call` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::Once::call_once::<{closure@std::rt::cleanup::{closure#0}}>` at RUSTLIB/std/src/sync/poison/once.rs:LL:CC
= note: inside `std::rt::cleanup` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange::<*mut i32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicPtr::<i32>::compare_exchange` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::exit_guard::unique_thread_exit` at RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
Verification complete with 1 executions. No errors found.

38
src/tools/miri/tests/genmc/pass/thread/thread_locals.rs → src/tools/miri/tests/genmc/pass/std/thread_locals.rs
View file

@ -1,17 +1,10 @@
//@compile-flags: -Zmiri-ignore-leaks -Zmiri-genmc -Zmiri-disable-stacked-borrows
#![no_main]
#[path = "../../../utils/genmc.rs"]
mod genmc;
use std::alloc::{Layout, alloc};
use std::cell::Cell;
use std::sync::atomic::AtomicPtr;
use std::sync::atomic::Ordering::*;
use crate::genmc::*;
static X: AtomicPtr<u64> = AtomicPtr::new(std::ptr::null_mut());
thread_local! {
@ -22,26 +15,21 @@ pub unsafe fn malloc() -> *mut u64 {
alloc(Layout::new::<u64>()) as *mut u64
}
#[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(std::ptr::null_mut(), SeqCst);
unsafe {
spawn_pthread_closure(|| {
R.set(malloc());
fn main() {
let handles = [
std::thread::spawn(|| {
R.set(unsafe { malloc() });
let r_ptr = R.get();
let _ = X.compare_exchange(std::ptr::null_mut(), r_ptr, SeqCst, SeqCst);
});
spawn_pthread_closure(|| {
R.set(malloc());
});
spawn_pthread_closure(|| {
R.set(malloc());
}),
std::thread::spawn(|| {
R.set(unsafe { malloc() });
}),
std::thread::spawn(|| {
R.set(unsafe { malloc() });
let r_ptr = R.get();
let _ = X.compare_exchange(std::ptr::null_mut(), r_ptr, SeqCst, SeqCst);
});
0
}
}),
];
handles.into_iter().for_each(|handle| handle.join().unwrap());
}

184
src/tools/miri/tests/genmc/pass/std/thread_locals.stderr Normal file
View file

@ -0,0 +1,184 @@
Running GenMC Verification...
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u64>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU64::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::option::Option::<std::thread::ThreadId>::unwrap_or_else::<{closure@std::thread::current::id::get_or_init::{closure#0}}>` at RUSTLIB/core/src/option.rs:LL:CC
= note: inside `std::thread::current::id::get_or_init` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::thread::current::current_id` at RUSTLIB/std/src/thread/current.rs:LL:CC
= note: inside `std::rt::init` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | / std::thread::spawn(|| {
LL | | R.set(unsafe { malloc() });
LL | | let r_ptr = R.get();
LL | | let _ = X.compare_exchange(std::ptr::null_mut(), r_ptr, SeqCst, SeqCst);
LL | | }),
| |__________^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
|
LL | || self
| ________________^
LL | | .state
LL | | .compare_exchange_weak(state, state + READ_LOCKED, Acquire, Relaxed)
| |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
= note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
= note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | / std::thread::spawn(|| {
LL | | R.set(unsafe { malloc() });
LL | | let r_ptr = R.get();
LL | | let _ = X.compare_exchange(std::ptr::null_mut(), r_ptr, SeqCst, SeqCst);
LL | | }),
| |__________^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/thread/mod.rs:LL:CC
|
LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | / std::thread::spawn(|| {
LL | | R.set(unsafe { malloc() });
LL | | }),
| |__________^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/std/src/thread/mod.rs:LL:CC
|
LL | match COUNTER.compare_exchange_weak(last, id, Ordering::Relaxed, Ordering::Relaxed) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | / std::thread::spawn(|| {
LL | | R.set(unsafe { malloc() });
LL | | let r_ptr = R.get();
LL | | let _ = X.compare_exchange(std::ptr::null_mut(), r_ptr, SeqCst, SeqCst);
LL | | }),
| |__________^
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/alloc/src/sync.rs:LL:CC
|
LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::get_mut` at RUSTLIB/alloc/src/sync.rs:LL:CC
= note: inside `std::thread::JoinInner::<'_, ()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
= note: inside `std::thread::JoinHandle::<()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
note: inside closure
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | handles.into_iter().for_each(|handle| handle.join().unwrap());
| ^^^^^^^^^^^^^
= note: inside closure at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
= note: inside closure at RUSTLIB/core/src/ops/try_trait.rs:LL:CC
= note: inside closure at RUSTLIB/core/src/array/iter/iter_inner.rs:LL:CC
= note: inside `<std::ops::index_range::IndexRange as std::iter::Iterator>::try_fold::<(), {closure@std::array::iter::iter_inner::PolymorphicIter<[std::mem::MaybeUninit<std::thread::JoinHandle<()>>]>::try_fold<(), {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_2<(), std::thread::JoinHandle<()>, {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>::{closure#0}}>::{closure#0}}, std::ops::try_trait::NeverShortCircuit<()>>::{closure#0}}, std::ops::try_trait::NeverShortCircuit<()>>` at RUSTLIB/core/src/ops/index_range.rs:LL:CC
= note: inside `std::array::iter::iter_inner::PolymorphicIter::<[std::mem::MaybeUninit<std::thread::JoinHandle<()>>]>::try_fold::<(), {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_2<(), std::thread::JoinHandle<()>, {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>::{closure#0}}>::{closure#0}}, std::ops::try_trait::NeverShortCircuit<()>>` at RUSTLIB/core/src/array/iter/iter_inner.rs:LL:CC
= note: inside `std::array::iter::iter_inner::PolymorphicIter::<[std::mem::MaybeUninit<std::thread::JoinHandle<()>>]>::fold::<(), {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>::{closure#0}}>` at RUSTLIB/core/src/array/iter/iter_inner.rs:LL:CC
= note: inside `<std::array::IntoIter<std::thread::JoinHandle<()>, 3> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call<std::thread::JoinHandle<()>, {closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>::{closure#0}}>` at RUSTLIB/core/src/array/iter.rs:LL:CC
= note: inside `<std::array::IntoIter<std::thread::JoinHandle<()>, 3> as std::iter::Iterator>::for_each::<{closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>` at RUSTLIB/core/src/iter/traits/iterator.rs:LL:CC
note: inside `main`
--> tests/genmc/pass/std/thread_locals.rs:LL:CC
|
LL | handles.into_iter().for_each(|handle| handle.join().unwrap());
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
warning: GenMC currently does not model spurious failures of `compare_exchange_weak`. Miri with GenMC might miss bugs related to spurious failures.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Acquire }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicU32::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::sync::PLATFORM::futex::Once::call` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
= note: inside `std::sync::Once::call_once::<{closure@std::rt::cleanup::{closure#0}}>` at RUSTLIB/std/src/sync/poison/once.rs:LL:CC
= note: inside `std::rt::cleanup` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
--> RUSTLIB/core/src/sync/atomic.rs:LL:CC
|
LL | intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxed }>(dst, old, new)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
|
= note: BACKTRACE:
= note: inside `std::sync::atomic::atomic_compare_exchange::<*mut i32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sync::atomic::AtomicPtr::<i32>::compare_exchange` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
= note: inside `std::sys::exit_guard::unique_thread_exit` at RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
= note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
= note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
= note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
= note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
Verification complete with 2 executions. No errors found.

2
src/tools/miri/tests/genmc/pass/thread/thread_locals.stderr
View file

@ -1,2 +0,0 @@
Running GenMC Verification...
Verification complete with 2 executions. No errors found.