Skip to content

Commit

Permalink
naming in read_retag_no_race
Browse files Browse the repository at this point in the history
consistency within the test itself and with spurious_read
  • Loading branch information
Vanille-N committed Oct 6, 2023
1 parent 5443862 commit 62feb30
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 26 deletions.
44 changes: 22 additions & 22 deletions tests/pass/tree_borrows/read_retag_no_race.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,12 +25,12 @@ unsafe impl Send for SendPtr {}
//
// The interleaving executed here is the one that does not have UB,
// i.e.
// read y
// retag x
// write x
// 1:read x
// 2:retag y
// 2:write y
//
// Tree Borrows considers that the read of `y` cannot be in conflict
// with `x` because `x` did not even exist yet when `y` was accessed.
// Tree Borrows considers that the read of `x` cannot be in conflict
// with `y` because `y` did not even exist yet when `x` was accessed.
//
// As long as we are not emitting any writes for the data race model
// upon retags of mutable references, it should not have any issue with
Expand All @@ -45,9 +45,9 @@ unsafe impl Send for SendPtr {}

// The other interleaving is a subsequence of `tests/fail/tree_borrows/spurious_read.rs`
// which asserts that
// retag x
// read y
// write x
// 2:retag y
// 1:read x
// 2:write y
// is UB.

type IdxBarrier = (usize, Arc<Barrier>);
Expand All @@ -66,28 +66,28 @@ macro_rules! synchronized {
}};
}

fn thread_1(y: SendPtr, barrier: IdxBarrier) {
let y = unsafe { &mut *y.0 };
fn thread_1(x: SendPtr, barrier: IdxBarrier) {
let x = unsafe { &mut *x.0 };
synchronized!(barrier, "spawn");

synchronized!(barrier, "read y || retag x");
synchronized!(barrier, "read x || retag y");
// This is the interleaving without UB: by the time
// the other thread starts retagging, this thread
// has already finished all its work using `y`.
let _v = *y;
synchronized!(barrier, "write x");
let _v = *x;
synchronized!(barrier, "write y");
synchronized!(barrier, "exit");
}

fn thread_2(x: SendPtr, barrier: IdxBarrier) {
let x = unsafe { &mut *x.0 };
fn thread_2(y: SendPtr, barrier: IdxBarrier) {
let y = unsafe { &mut *y.0 };
synchronized!(barrier, "spawn");

fn write(x: &mut u8, v: u8, barrier: &IdxBarrier) {
synchronized!(barrier, "write x");
*x = v;
fn write(y: &mut u8, v: u8, barrier: &IdxBarrier) {
synchronized!(barrier, "write y");
*y = v;
}
synchronized!(barrier, "read y || retag x");
synchronized!(barrier, "read x || retag y");
// We don't use a barrier here so that *if* the retag counted as a write
// for the data race model, then it would be UB.
// We still want to make sure that the other thread goes first as per the
Expand All @@ -96,13 +96,13 @@ fn thread_2(x: SendPtr, barrier: IdxBarrier) {
// not counting as "synchronization" from the point of view of the data
// race model.
thread::yield_now();
write(&mut *x, 42, &barrier);
write(&mut *y, 42, &barrier);
synchronized!(barrier, "exit");
}

fn main() {
let mut x = 0u8;
let p = SendPtr(addr_of_mut!(x));
let mut data = 0u8;
let p = SendPtr(addr_of_mut!(data));
let barrier = Arc::new(Barrier::new(2));
let b1 = (1, Arc::clone(&barrier));
let b2 = (2, Arc::clone(&barrier));
Expand Down
8 changes: 4 additions & 4 deletions tests/pass/tree_borrows/read_retag_no_race.stderr
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
Thread 1 executing: spawn
Thread 2 executing: spawn
Thread 2 executing: read y || retag x
Thread 1 executing: read y || retag x
Thread 1 executing: write x
Thread 2 executing: write x
Thread 2 executing: read x || retag y
Thread 1 executing: read x || retag y
Thread 1 executing: write y
Thread 2 executing: write y
Thread 2 executing: exit
Thread 1 executing: exit

0 comments on commit 62feb30

Please sign in to comment.