Skip to content

Commit

Permalink
disable address reuse in data race tests
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Apr 18, 2024
1 parent c962d88 commit 34c8db6
Show file tree
Hide file tree
Showing 37 changed files with 82 additions and 4 deletions.
2 changes: 2 additions & 0 deletions tests/fail/both_borrows/retag_data_race_write.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
//! Make sure that a retag acts like a write for the data race model.
//@revisions: stack tree
//@compile-flags: -Zmiri-preemption-rate=0
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0
//@[tree]compile-flags: -Zmiri-tree-borrows
#[derive(Copy, Clone)]
struct SendPtr(*mut u8);
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/alloc_read_race.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0
#![feature(new_uninit)]

use std::mem::MaybeUninit;
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/alloc_write_race.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0
#![feature(new_uninit)]

use std::ptr::null_mut;
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/atomic_read_na_write_race1.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicUsize, Ordering};
use std::thread::spawn;
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/atomic_read_na_write_race2.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::AtomicUsize;
use std::sync::atomic::Ordering;
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/atomic_write_na_read_race1.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::AtomicUsize;
use std::sync::atomic::Ordering;
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/atomic_write_na_read_race2.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicUsize, Ordering};
use std::thread::spawn;
Expand Down
4 changes: 4 additions & 0 deletions tests/fail/data_race/atomic_write_na_write_race1.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicUsize, Ordering};
use std::thread::spawn;
Expand All @@ -18,6 +20,8 @@ pub fn main() {
let j1 = spawn(move || {
let c = c; // avoid field capturing
*(c.0 as *mut usize) = 32;
// Make this thread take a bit longer.
for _ in 0..100 {}
});

let j2 = spawn(move || {
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/atomic_write_na_write_race2.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::AtomicUsize;
use std::sync::atomic::Ordering;
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/dangling_thread_async_race.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::mem;
use std::thread::{sleep, spawn};
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/dangling_thread_race.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::mem;
use std::thread::{sleep, spawn};
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/dealloc_read_race1.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::thread::spawn;

Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/dealloc_read_race2.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::thread::spawn;

Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/dealloc_read_race_stack.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::ptr::null_mut;
use std::sync::atomic::{AtomicPtr, Ordering};
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/dealloc_write_race1.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::thread::spawn;

Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/dealloc_write_race2.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::thread::spawn;

Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/dealloc_write_race_stack.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::ptr::null_mut;
use std::sync::atomic::{AtomicPtr, Ordering};
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/enable_after_join_to_main.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::thread::spawn;

Expand Down
3 changes: 3 additions & 0 deletions tests/fail/data_race/fence_after_load.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{fence, AtomicUsize, Ordering};
use std::sync::Arc;
use std::thread;
Expand Down
3 changes: 3 additions & 0 deletions tests/fail/data_race/mixed_size_read.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicU16, AtomicU8, Ordering};
use std::thread;

Expand Down
3 changes: 3 additions & 0 deletions tests/fail/data_race/mixed_size_write.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
//@compile-flags: -Zmiri-preemption-rate=0.0 -Zmiri-disable-weak-memory-emulation
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicU16, AtomicU8, Ordering};
use std::thread;

Expand Down
3 changes: 3 additions & 0 deletions tests/fail/data_race/read_read_race1.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
//@compile-flags: -Zmiri-preemption-rate=0.0
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicU16, Ordering};
use std::thread;

Expand Down
3 changes: 3 additions & 0 deletions tests/fail/data_race/read_read_race2.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
//@compile-flags: -Zmiri-preemption-rate=0.0
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicU16, Ordering};
use std::thread;

Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/read_write_race.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here. Stacked borrows interferes by having its own accesses.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::thread::spawn;

Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/read_write_race_stack.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::ptr::null_mut;
use std::sync::atomic::{AtomicPtr, Ordering};
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/relax_acquire_race.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicUsize, Ordering};
use std::thread::spawn;
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/release_seq_race.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicUsize, Ordering};
use std::thread::{sleep, spawn};
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/release_seq_race_same_thread.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicUsize, Ordering};
use std::thread::spawn;
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/rmw_race.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::sync::atomic::{AtomicUsize, Ordering};
use std::thread::spawn;
Expand Down
3 changes: 3 additions & 0 deletions tests/fail/data_race/stack_pop_race.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::thread;

#[derive(Copy, Clone)]
Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/write_write_race.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
// We want to control preemption here.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::thread::spawn;

Expand Down
2 changes: 2 additions & 0 deletions tests/fail/data_race/write_write_race_stack.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-weak-memory-emulation -Zmiri-preemption-rate=0 -Zmiri-disable-stacked-borrows
// Avoid accidental synchronization via address reuse inside `thread::spawn`.
//@compile-flags: -Zmiri-address-reuse-rate=0

use std::ptr::null_mut;
use std::sync::atomic::{AtomicPtr, Ordering};
Expand Down
3 changes: 2 additions & 1 deletion tests/fail/stacked_borrows/retag_data_race_protected_read.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
//@compile-flags: -Zmiri-preemption-rate=0
// Avoid accidental synchronization via address reuse.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-rate=0
use std::thread;

#[derive(Copy, Clone)]
Expand Down
3 changes: 2 additions & 1 deletion tests/fail/stacked_borrows/retag_data_race_read.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
//! Make sure that a retag acts like a read for the data race model.
//@compile-flags: -Zmiri-preemption-rate=0
// Avoid accidental synchronization via address reuse.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-rate=0
#[derive(Copy, Clone)]
struct SendPtr(*mut u8);

Expand Down
3 changes: 2 additions & 1 deletion tests/fail/weak_memory/racing_mixed_size.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
// We want to control preemption here.
//@compile-flags: -Zmiri-preemption-rate=0
// Avoid accidental synchronization via address reuse.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-rate=0

#![feature(core_intrinsics)]

Expand Down
3 changes: 2 additions & 1 deletion tests/fail/weak_memory/racing_mixed_size_read.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
// We want to control preemption here.
//@compile-flags: -Zmiri-preemption-rate=0
// Avoid accidental synchronization via address reuse.
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-rate=0

use std::sync::atomic::Ordering::*;
use std::sync::atomic::{AtomicU16, AtomicU32};
Expand Down
2 changes: 2 additions & 0 deletions tests/pass/concurrency/disable_data_race_detector.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,6 @@
//@compile-flags: -Zmiri-disable-data-race-detector
// Avoid non-determinism
//@compile-flags: -Zmiri-preemption-rate=0 -Zmiri-address-reuse-rate=0

use std::thread::spawn;

Expand Down

0 comments on commit 34c8db6

Please sign in to comment.