diff --git a/src/tools/miri/genmc-sys/build.rs b/src/tools/miri/genmc-sys/build.rs index ef49be151bf0..964382d82408 100644 --- a/src/tools/miri/genmc-sys/build.rs +++ b/src/tools/miri/genmc-sys/build.rs @@ -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. diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp index 5f73e5d3d3d0..c9da718aabd6 100644 --- a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp +++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp @@ -214,9 +214,10 @@ struct MiriGenmcShim : private GenMCDriver { * Automatically calls `inc_pos` and `dec_pos` where needed for the given thread. */ template - auto handle_load_reset_if_none(ThreadId tid, Ts&&... params) -> HandleResult { + auto handle_load_reset_if_none(ThreadId tid, std::optional old_val, Ts&&... params) + -> HandleResult { const auto pos = inc_pos(tid); - const auto ret = GenMCDriver::handleLoad(pos, std::forward(params)...); + const auto ret = GenMCDriver::handleLoad(pos, old_val, std::forward(params)...); // If we didn't get a value, we have to reset the index of the current thread. if (!std::holds_alternative(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 try_to_sval(GenmcScalar scalar) { + if (scalar.is_init) + return { SVal(scalar.value, scalar.extra) }; + return std::nullopt; +} } // namespace GenmcScalarExt namespace LoadResultExt { diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp index c9e7f7a1a8a1..a8f8b9cc24f9 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp @@ -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( 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( 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(&ret)) return StoreResultExt::from_error(format_error(*err)); - if (!std::holds_alternative(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(&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( 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( 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(&store_ret)) return ReadModifyWriteResultExt::from_error(format_error(*err)); - const auto* store_ret_val = std::get_if(&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(&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( 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( 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(&store_ret)) return CompareExchangeResultExt::from_error(format_error(*err)); - const auto* store_ret_val = std::get_if(&store_ret); + const bool* is_coherence_order_maximal_write = std::get_if(&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 ****/ diff --git a/src/tools/miri/tests/genmc/fail/atomics/atomic_ptr_double_free.rs b/src/tools/miri/tests/genmc/fail/atomics/atomic_ptr_double_free.rs index d712822a6d00..c18675931719 100644 --- a/src/tools/miri/tests/genmc/fail/atomics/atomic_ptr_double_free.rs +++ b/src/tools/miri/tests/genmc/fail/atomics/atomic_ptr_double_free.rs @@ -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(|| { diff --git a/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_alloc_race.rs b/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_alloc_race.rs index d82fbf53dac7..e453c16b157d 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_alloc_race.rs +++ b/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_alloc_race.rs @@ -23,9 +23,6 @@ static X: AtomicPtr = 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(|| { diff --git a/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_dealloc_write_race.rs b/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_dealloc_write_race.rs index c9bf1f755925..10e0d8d854c2 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_dealloc_write_race.rs +++ b/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_dealloc_write_race.rs @@ -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(|| { diff --git a/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_write_dealloc_race.rs b/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_write_dealloc_race.rs index 2253bac95de8..e2d3057a5b0d 100644 --- a/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_write_dealloc_race.rs +++ b/src/tools/miri/tests/genmc/fail/data_race/atomic_ptr_write_dealloc_race.rs @@ -24,9 +24,6 @@ static Y: AtomicPtr = 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(|| { diff --git a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs index 508eae756f32..2e614e6a360b 100644 --- a/src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs +++ b/src/tools/miri/tests/genmc/fail/loom/buggy_inc.rs @@ -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(); diff --git a/src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_ops.rs b/src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_ops.rs index 9db58b1f9501..aa40e193dbfd 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_ops.rs +++ b/src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_ops.rs @@ -37,18 +37,22 @@ unsafe fn pointers_equal(a: *mut u64, b: *mut u64) { unsafe fn test_load_store_exchange() { let atomic_ptr: AtomicPtr = 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 = 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 = 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)); diff --git a/src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_roundtrip.rs b/src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_roundtrip.rs index 75ee5ede9c96..d846a55cbc31 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_roundtrip.rs +++ b/src/tools/miri/tests/genmc/pass/atomics/atomic_ptr_roundtrip.rs @@ -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(|| { diff --git a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs index 8a77d54a64f8..e17a988cb373 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs +++ b/src/tools/miri/tests/genmc/pass/atomics/cas_failure_ord_racy_key_init.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/atomics/mixed_atomic_non_atomic.rs b/src/tools/miri/tests/genmc/pass/atomics/mixed_atomic_non_atomic.rs new file mode 100644 index 000000000000..7601b354b1c0 --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/atomics/mixed_atomic_non_atomic.rs @@ -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(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 +} diff --git a/src/tools/miri/tests/genmc/pass/atomics/mixed_atomic_non_atomic.stderr b/src/tools/miri/tests/genmc/pass/atomics/mixed_atomic_non_atomic.stderr new file mode 100644 index 000000000000..7867be2dbe8e --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/atomics/mixed_atomic_non_atomic.stderr @@ -0,0 +1,2 @@ +Running GenMC Verification... +Verification complete with 1 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/atomics/read_initial_value.rs b/src/tools/miri/tests/genmc/pass/atomics/read_initial_value.rs new file mode 100644 index 000000000000..18e039fdd0df --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/atomics/read_initial_value.rs @@ -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 +} diff --git a/src/tools/miri/tests/genmc/pass/atomics/read_initial_value.stderr b/src/tools/miri/tests/genmc/pass/atomics/read_initial_value.stderr new file mode 100644 index 000000000000..7867be2dbe8e --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/atomics/read_initial_value.stderr @@ -0,0 +1,2 @@ +Running GenMC Verification... +Verification complete with 1 executions. No errors found. diff --git a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs index f48466e8ce10..7e6e33c8a7b1 100644 --- a/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs +++ b/src/tools/miri/tests/genmc/pass/atomics/rmw_ops.rs @@ -21,11 +21,8 @@ fn assert_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 diff --git a/src/tools/miri/tests/genmc/pass/data-structures/ms_queue_dynamic.rs b/src/tools/miri/tests/genmc/pass/data-structures/ms_queue_dynamic.rs index fda517ae7d23..934fc977366d 100644 --- a/src/tools/miri/tests/genmc/pass/data-structures/ms_queue_dynamic.rs +++ b/src/tools/miri/tests/genmc/pass/data-structures/ms_queue_dynamic.rs @@ -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); diff --git a/src/tools/miri/tests/genmc/pass/data-structures/treiber_stack_dynamic.rs b/src/tools/miri/tests/genmc/pass/data-structures/treiber_stack_dynamic.rs index 2101f9ae66bb..8bdd2a371f51 100644 --- a/src/tools/miri/tests/genmc/pass/data-structures/treiber_stack_dynamic.rs +++ b/src/tools/miri/tests/genmc/pass/data-structures/treiber_stack_dynamic.rs @@ -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) diff --git a/src/tools/miri/tests/genmc/pass/intercept/spinloop_assume.rs b/src/tools/miri/tests/genmc/pass/intercept/spinloop_assume.rs index 9d7c823b1e48..cf19e9299442 100644 --- a/src/tools/miri/tests/genmc/pass/intercept/spinloop_assume.rs +++ b/src/tools/miri/tests/genmc/pass/intercept/spinloop_assume.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/2cowr.rs b/src/tools/miri/tests/genmc/pass/litmus/2cowr.rs index d3fdb470ed36..d9b582bb4362 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/2cowr.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/2cowr.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs index 1ec62ff21342..6d2dfd4f273e 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/IRIW-acq-sc.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs index fa717b4cf18a..6f1d37962d10 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/IRIWish.rs @@ -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 = [ diff --git a/src/tools/miri/tests/genmc/pass/litmus/LB.rs b/src/tools/miri/tests/genmc/pass/litmus/LB.rs index 1cee3230b127..107121ef4e3c 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/LB.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/LB.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP.rs b/src/tools/miri/tests/genmc/pass/litmus/MP.rs index e245cdd15eef..5f9d1b01c37b 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/MP.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/MP.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs index a1b13e3f3c56..6f812bf8a8ac 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/MPU2_rels_acqf.rs @@ -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); diff --git a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.rs b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.rs index b36c8a288f42..4f20b2cf9def 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/MPU_rels_acq.rs @@ -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); diff --git a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.rs b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.rs index cf9f5f2dbfa3..19065d3308f8 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/MP_rels_acqf.rs @@ -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); diff --git a/src/tools/miri/tests/genmc/pass/litmus/SB.rs b/src/tools/miri/tests/genmc/pass/litmus/SB.rs index e592fe05c4e4..74d45c22a295 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/SB.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/SB.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs index a991ccb0d4e0..cbbaa82d6fb5 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/Z6_U.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/casdep.rs b/src/tools/miri/tests/genmc/pass/litmus/casdep.rs index c376d96b111c..8b8f6e793c1f 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/casdep.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/casdep.rs @@ -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); diff --git a/src/tools/miri/tests/genmc/pass/litmus/ccr.rs b/src/tools/miri/tests/genmc/pass/litmus/ccr.rs index 865895b4dcd9..4537f3d6830c 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/ccr.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/ccr.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/cii.rs b/src/tools/miri/tests/genmc/pass/litmus/cii.rs index 663c806e667c..18f56860f960 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/cii.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/cii.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr.rs b/src/tools/miri/tests/genmc/pass/litmus/corr.rs index d6c95100fc24..b586e2e0fa8a 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corr.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/corr.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr0.rs b/src/tools/miri/tests/genmc/pass/litmus/corr0.rs index f722131fda84..856d566ca8bd 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corr0.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/corr0.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr1.rs b/src/tools/miri/tests/genmc/pass/litmus/corr1.rs index a4e8249bac30..ccd849802911 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corr1.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/corr1.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/corr2.rs b/src/tools/miri/tests/genmc/pass/litmus/corr2.rs index 2f490d363779..36616bf36371 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corr2.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/corr2.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/corw.rs b/src/tools/miri/tests/genmc/pass/litmus/corw.rs index 7acc20822a4f..9216a4f8368f 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/corw.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/corw.rs @@ -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 = [ diff --git a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.rs b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.rs index 2387976a8ca6..4034f7634e87 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/cumul-release.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/cumul-release.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/default.rs b/src/tools/miri/tests/genmc/pass/litmus/default.rs index 55fb1ac34acb..0ab26dce419a 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/default.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/default.rs @@ -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; diff --git a/src/tools/miri/tests/genmc/pass/litmus/detour.rs b/src/tools/miri/tests/genmc/pass/litmus/detour.rs index 7136c029bbb5..85c456d5c54e 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/detour.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/detour.rs @@ -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. diff --git a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs index 796ffbf97f96..c8d3d409cf04 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/fr_w_w_w_reads.rs @@ -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 = [ diff --git a/src/tools/miri/tests/genmc/pass/litmus/inc2w.rs b/src/tools/miri/tests/genmc/pass/litmus/inc2w.rs index fd8574c4f7c7..eb84304a1986 100644 --- a/src/tools/miri/tests/genmc/pass/litmus/inc2w.rs +++ b/src/tools/miri/tests/genmc/pass/litmus/inc2w.rs @@ -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(|| { diff --git a/src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr b/src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr new file mode 100644 index 000000000000..f2c574283cbf --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/std/arc.check_count.stderr @@ -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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::::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::` 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::::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::::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::>` 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::>` 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::>` 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::>` 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::>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC + = note: inside `std::sync::Arc::>::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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::` 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::(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::::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::` 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. diff --git a/src/tools/miri/tests/genmc/pass/std/arc.rs b/src/tools/miri/tests/genmc/pass/std/arc.rs new file mode 100644 index 000000000000..addf6408c006 --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/std/arc.rs @@ -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()); +} diff --git a/src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr b/src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr new file mode 100644 index 000000000000..a7dacdeba4e4 --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/std/arc.try_upgrade.stderr @@ -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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::::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::` 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::::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::::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::>` 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::>` 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::>` 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::>` 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::>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC + = note: inside `std::sync::Arc::>::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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::` 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::(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::::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::` 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::::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::::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. diff --git a/src/tools/miri/tests/genmc/pass/std/empty_main.rs b/src/tools/miri/tests/genmc/pass/std/empty_main.rs new file mode 100644 index 000000000000..2ffc3388fb36 --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/std/empty_main.rs @@ -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() {} diff --git a/src/tools/miri/tests/genmc/pass/std/empty_main.stderr b/src/tools/miri/tests/genmc/pass/std/empty_main.stderr new file mode 100644 index 000000000000..36ba5481f472 --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/std/empty_main.stderr @@ -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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::::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::` 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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::` 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::(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::::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::` 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. diff --git a/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.rs b/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.rs new file mode 100644 index 000000000000..dadbee47b986 --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.rs @@ -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() {} diff --git a/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr b/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr new file mode 100644 index 000000000000..d6195b4e9b21 --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/std/spawn_std_threads.stderr @@ -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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::::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::` 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::>` 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::>` 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 ` as std::iter::Iterator>::fold::<(), {closure@std::iter::adapters::map::map_fold, (), {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}, {closure@std::iter::Iterator::for_each::call, {closure@std::vec::Vec>::extend_trusted, {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 `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call, {closure@std::vec::Vec>::extend_trusted, {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 `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::for_each::<{closure@std::vec::Vec>::extend_trusted, {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::>::extend_trusted::, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC + = note: inside `> as std::vec::spec_extend::SpecExtend, std::iter::Map, {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 `> as std::vec::spec_from_iter_nested::SpecFromIterNested, std::iter::Map, {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 `> as std::vec::spec_from_iter::SpecFromIter, std::iter::Map, {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 `> as std::iter::FromIterator>>::from_iter::, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC + = note: inside `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::collect::>>` 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::>` 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::>` 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 ` as std::iter::Iterator>::fold::<(), {closure@std::iter::adapters::map::map_fold, (), {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}, {closure@std::iter::Iterator::for_each::call, {closure@std::vec::Vec>::extend_trusted, {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 `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call, {closure@std::vec::Vec>::extend_trusted, {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 `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::for_each::<{closure@std::vec::Vec>::extend_trusted, {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::>::extend_trusted::, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC + = note: inside `> as std::vec::spec_extend::SpecExtend, std::iter::Map, {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 `> as std::vec::spec_from_iter_nested::SpecFromIterNested, std::iter::Map, {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 `> as std::vec::spec_from_iter::SpecFromIter, std::iter::Map, {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 `> as std::iter::FromIterator>>::from_iter::, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}>>` at RUSTLIB/alloc/src/vec/mod.rs:LL:CC + = note: inside `, {closure@tests/genmc/pass/std/spawn_std_threads.rs:LL:CC}> as std::iter::Iterator>::collect::>>` 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::>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC + = note: inside `std::sync::Arc::>::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 `> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call, {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 `> 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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::` 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::(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::::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::` 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. diff --git a/src/tools/miri/tests/genmc/pass/thread/thread_locals.rs b/src/tools/miri/tests/genmc/pass/std/thread_locals.rs similarity index 53% rename from src/tools/miri/tests/genmc/pass/thread/thread_locals.rs rename to src/tools/miri/tests/genmc/pass/std/thread_locals.rs index cabc8ec92da1..d76975d2e92c 100644 --- a/src/tools/miri/tests/genmc/pass/thread/thread_locals.rs +++ b/src/tools/miri/tests/genmc/pass/std/thread_locals.rs @@ -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 = AtomicPtr::new(std::ptr::null_mut()); thread_local! { @@ -22,26 +15,21 @@ pub unsafe fn malloc() -> *mut u64 { alloc(Layout::new::()) 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()); } diff --git a/src/tools/miri/tests/genmc/pass/std/thread_locals.stderr b/src/tools/miri/tests/genmc/pass/std/thread_locals.stderr new file mode 100644 index 000000000000..ff971301bc66 --- /dev/null +++ b/src/tools/miri/tests/genmc/pass/std/thread_locals.stderr @@ -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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::::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::` 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::>` 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::>` 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::>` 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::>` 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::>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC + = note: inside `std::sync::Arc::>::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 `::try_fold::<(), {closure@std::array::iter::iter_inner::PolymorphicIter<[std::mem::MaybeUninit>]>::try_fold<(), {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_2<(), std::thread::JoinHandle<()>, {closure@std::iter::Iterator::for_each::call, {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>]>::try_fold::<(), {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_2<(), std::thread::JoinHandle<()>, {closure@std::iter::Iterator::for_each::call, {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>]>::fold::<(), {closure@std::iter::Iterator::for_each::call, {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 `, 3> as std::iter::Iterator>::fold::<(), {closure@std::iter::Iterator::for_each::call, {closure@tests/genmc/pass/std/thread_locals.rs:LL:CC}>::{closure#0}}>` at RUSTLIB/core/src/array/iter.rs:LL:CC + = note: inside `, 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::(dst, old, new) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code + | + = note: BACKTRACE: + = note: inside `std::sync::atomic::atomic_compare_exchange_weak::` 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::` 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::(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::::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::` 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. diff --git a/src/tools/miri/tests/genmc/pass/thread/thread_locals.stderr b/src/tools/miri/tests/genmc/pass/thread/thread_locals.stderr deleted file mode 100644 index bde951866d01..000000000000 --- a/src/tools/miri/tests/genmc/pass/thread/thread_locals.stderr +++ /dev/null @@ -1,2 +0,0 @@ -Running GenMC Verification... -Verification complete with 2 executions. No errors found.