-
Notifications
You must be signed in to change notification settings - Fork 353
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add tests, and fix bug in atomic RMW relaxed stores
- Loading branch information
1 parent
e4a9192
commit 837715a
Showing
16 changed files
with
315 additions
and
11 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
|
||
use std::thread::spawn; | ||
|
||
#[derive(Copy, Clone)] | ||
struct EvilSend<T>(pub T); | ||
|
||
unsafe impl<T> Send for EvilSend<T> {} | ||
unsafe impl<T> Sync for EvilSend<T> {} | ||
|
||
pub fn main() { | ||
let mut a = 0u32; | ||
let b = &mut a as *mut u32; | ||
let c = EvilSend(b); | ||
unsafe { | ||
let j1 = spawn(move || { | ||
*c.0 | ||
}); | ||
|
||
let j2 = spawn(move || { | ||
*c.0 = 64; //~ ERROR Data race | ||
}); | ||
|
||
j1.join().unwrap(); | ||
j2.join().unwrap(); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,42 @@ | ||
|
||
use std::thread::spawn; | ||
use std::sync::atomic::{AtomicUsize, Ordering}; | ||
|
||
#[derive(Copy, Clone)] | ||
struct EvilSend<T>(pub T); | ||
|
||
unsafe impl<T> Send for EvilSend<T> {} | ||
unsafe impl<T> Sync for EvilSend<T> {} | ||
|
||
static SYNC: AtomicUsize = AtomicUsize::new(0); | ||
|
||
pub fn main() { | ||
let mut a = 0u32; | ||
let b = &mut a as *mut u32; | ||
let c = EvilSend(b); | ||
|
||
unsafe { | ||
let j1 = spawn(move || { | ||
*c.0 = 1; | ||
SYNC.store(1, Ordering::Release); | ||
}); | ||
|
||
let j2 = spawn(move || { | ||
if SYNC.load(Ordering::Acquire) == 1 { | ||
SYNC.store(2, Ordering::Relaxed); | ||
} | ||
}); | ||
|
||
let j3 = spawn(move || { | ||
if SYNC.load(Ordering::Acquire) == 2 { | ||
*c.0 //~ ERROR Data race | ||
}else{ | ||
0 | ||
} | ||
}); | ||
|
||
j1.join().unwrap(); | ||
j2.join().unwrap(); | ||
j3.join().unwrap(); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,46 @@ | ||
// compile-flags: -Zmiri-disable-isolation | ||
|
||
use std::thread::{spawn, sleep}; | ||
use std::sync::atomic::{AtomicUsize, Ordering}; | ||
use std::time::Duration; | ||
|
||
#[derive(Copy, Clone)] | ||
struct EvilSend<T>(pub T); | ||
|
||
unsafe impl<T> Send for EvilSend<T> {} | ||
unsafe impl<T> Sync for EvilSend<T> {} | ||
|
||
static SYNC: AtomicUsize = AtomicUsize::new(0); | ||
|
||
pub fn main() { | ||
let mut a = 0u32; | ||
let b = &mut a as *mut u32; | ||
let c = EvilSend(b); | ||
|
||
unsafe { | ||
let j1 = spawn(move || { | ||
*c.0 = 1; | ||
SYNC.store(1, Ordering::Release); | ||
sleep(Duration::from_millis(100)); | ||
SYNC.store(3, Ordering::Relaxed); | ||
}); | ||
|
||
let j2 = spawn(move || { | ||
// Blocks the acquire-release sequence | ||
SYNC.store(2, Ordering::Relaxed); | ||
}); | ||
|
||
let j3 = spawn(move || { | ||
sleep(Duration::from_millis(1000)); | ||
if SYNC.load(Ordering::Acquire) == 3 { | ||
*c.0 //~ ERROR Data race | ||
}else{ | ||
0 | ||
} | ||
}); | ||
|
||
j1.join().unwrap(); | ||
j2.join().unwrap(); | ||
j3.join().unwrap(); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,43 @@ | ||
|
||
use std::thread::spawn; | ||
use std::sync::atomic::{AtomicUsize, Ordering}; | ||
|
||
#[derive(Copy, Clone)] | ||
struct EvilSend<T>(pub T); | ||
|
||
unsafe impl<T> Send for EvilSend<T> {} | ||
unsafe impl<T> Sync for EvilSend<T> {} | ||
|
||
static SYNC: AtomicUsize = AtomicUsize::new(0); | ||
|
||
pub fn main() { | ||
let mut a = 0u32; | ||
let b = &mut a as *mut u32; | ||
let c = EvilSend(b); | ||
|
||
unsafe { | ||
let j1 = spawn(move || { | ||
*c.0 = 1; | ||
SYNC.store(1, Ordering::Release); | ||
}); | ||
|
||
let j2 = spawn(move || { | ||
if SYNC.swap(2, Ordering::Relaxed) == 1 { | ||
// Blocks the acquire-release sequence | ||
SYNC.store(3, Ordering::Relaxed); | ||
} | ||
}); | ||
|
||
let j3 = spawn(move || { | ||
if SYNC.load(Ordering::Acquire) == 3 { | ||
*c.0 //~ ERROR Data race | ||
}else{ | ||
0 | ||
} | ||
}); | ||
|
||
j1.join().unwrap(); | ||
j2.join().unwrap(); | ||
j3.join().unwrap(); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
|
||
use std::thread::spawn; | ||
|
||
#[derive(Copy, Clone)] | ||
struct EvilSend<T>(pub T); | ||
|
||
unsafe impl<T> Send for EvilSend<T> {} | ||
unsafe impl<T> Sync for EvilSend<T> {} | ||
|
||
pub fn main() { | ||
let mut a = 0u32; | ||
let b = &mut a as *mut u32; | ||
let c = EvilSend(b); | ||
unsafe { | ||
let j1 = spawn(move || { | ||
*c.0 = 32; | ||
}); | ||
|
||
let j2 = spawn(move || { | ||
*c.0 = 64; //~ ERROR Data race | ||
}); | ||
|
||
j1.join().unwrap(); | ||
j2.join().unwrap(); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,119 @@ | ||
use std::sync::atomic::{AtomicUsize, fence, Ordering}; | ||
use std::thread::spawn; | ||
|
||
#[derive(Copy, Clone)] | ||
struct EvilSend<T>(pub T); | ||
|
||
unsafe impl<T> Send for EvilSend<T> {} | ||
unsafe impl<T> Sync for EvilSend<T> {} | ||
|
||
static SYNC: AtomicUsize = AtomicUsize::new(0); | ||
|
||
fn test_fence_sync() { | ||
let mut var = 0u32; | ||
let ptr = &mut var as *mut u32; | ||
let evil_ptr = EvilSend(ptr); | ||
|
||
|
||
let j1 = spawn(move || { | ||
unsafe { *evil_ptr.0 = 1; } | ||
fence(Ordering::Release); | ||
SYNC.store(1, Ordering::Relaxed) | ||
}); | ||
|
||
let j2 = spawn(move || { | ||
if SYNC.load(Ordering::Relaxed) == 1 { | ||
fence(Ordering::Acquire); | ||
unsafe { *evil_ptr.0 } | ||
}else{ | ||
0 | ||
} | ||
}); | ||
|
||
j1.join().unwrap(); | ||
j2.join().unwrap(); | ||
} | ||
|
||
|
||
fn test_multiple_reads() { | ||
let mut var = 42u32; | ||
let ptr = &mut var as *mut u32; | ||
let evil_ptr = EvilSend(ptr); | ||
|
||
let j1 = spawn(move || unsafe {*evil_ptr.0}); | ||
let j2 = spawn(move || unsafe {*evil_ptr.0}); | ||
let j3 = spawn(move || unsafe {*evil_ptr.0}); | ||
let j4 = spawn(move || unsafe {*evil_ptr.0}); | ||
|
||
assert_eq!(j1.join().unwrap(), 42); | ||
assert_eq!(j2.join().unwrap(), 42); | ||
assert_eq!(j3.join().unwrap(), 42); | ||
assert_eq!(j4.join().unwrap(), 42); | ||
|
||
var = 10; | ||
assert_eq!(var, 10); | ||
} | ||
|
||
pub fn test_rmw_no_block() { | ||
let mut a = 0u32; | ||
let b = &mut a as *mut u32; | ||
let c = EvilSend(b); | ||
|
||
unsafe { | ||
let j1 = spawn(move || { | ||
*c.0 = 1; | ||
SYNC.store(1, Ordering::Release); | ||
}); | ||
|
||
let j2 = spawn(move || { | ||
if SYNC.swap(2, Ordering::Relaxed) == 1 { | ||
//No op, blocking store removed | ||
} | ||
}); | ||
|
||
let j3 = spawn(move || { | ||
if SYNC.load(Ordering::Acquire) == 2 { | ||
*c.0 | ||
}else{ | ||
0 | ||
} | ||
}); | ||
|
||
j1.join().unwrap(); | ||
j2.join().unwrap(); | ||
let v = j3.join().unwrap(); | ||
assert!(v == 1 || v == 2); | ||
} | ||
} | ||
|
||
pub fn test_release_no_block() { | ||
let mut a = 0u32; | ||
let b = &mut a as *mut u32; | ||
let c = EvilSend(b); | ||
|
||
unsafe { | ||
let j1 = spawn(move || { | ||
*c.0 = 1; | ||
SYNC.store(1, Ordering::Release); | ||
SYNC.store(3, Ordering::Relaxed); | ||
}); | ||
|
||
let j2 = spawn(move || { | ||
if SYNC.load(Ordering::Acquire) == 3 { | ||
*c.0 | ||
}else{ | ||
0 | ||
} | ||
}); | ||
|
||
j1.join().unwrap(); | ||
assert_eq!(j2.join().unwrap(),1); | ||
} | ||
} | ||
|
||
pub fn main() { | ||
test_fence_sync(); | ||
test_multiple_reads(); | ||
test_rmw_no_block(); | ||
test_release_no_block(); | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
warning: thread support is experimental. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
warning: thread support is experimental. For example, Miri does not detect data races yet. | ||
warning: thread support is experimental. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
warning: thread support is experimental. For example, Miri does not detect data races yet. | ||
warning: thread support is experimental. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
warning: thread support is experimental. For example, Miri does not detect data races yet. | ||
warning: thread support is experimental. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
warning: thread support is experimental. For example, Miri does not detect data races yet. | ||
warning: thread support is experimental. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,2 @@ | ||
warning: thread support is experimental. For example, Miri does not detect data races yet. | ||
warning: thread support is experimental. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters