Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Weak memory emulation using store buffers #1963

Merged
merged 46 commits into from
Jun 6, 2022
Merged
Changes from 1 commit
Commits
Show all changes
46 commits
Select commit Hold shift + click to select a range
8d36e8b
Add weak memory config option
cbeuw Dec 25, 2021
16315b1
Add test cases
cbeuw Jan 17, 2022
e7698f4
Implement weak memory emulation
cbeuw Dec 27, 2021
aca3b3a
set_at_index sets the default value (0) if index doesn't exist in the…
cbeuw Apr 15, 2022
cf26658
Comment out and provide context to C++20 test
cbeuw Apr 16, 2022
ecdab5f
Clearer boundries between alloc metadata with multiple buffers and an…
cbeuw May 1, 2022
53f4887
Use a new AllocationMap to store store buffers in the same allocation
cbeuw May 6, 2022
a71b103
Add imperfectly overlapping test
cbeuw May 6, 2022
bf7fe68
Add -Zmiri-disable-weak-memory-emulation to README
cbeuw May 6, 2022
11ca975
Move type definitions together and clarify fetch_store on empty buffer
cbeuw May 7, 2022
32627d5
Disable weak memory emulation on scheduler-dependent data race tests
cbeuw May 7, 2022
f729f28
Move cpp20_rwc_syncs into compile-fail
cbeuw May 7, 2022
89138a6
Add more top-level comments
cbeuw May 10, 2022
62b514e
Update README
cbeuw May 10, 2022
773131b
Improve privacy and comments
cbeuw May 11, 2022
7d874db
Add tests showing weak memory behaviours
cbeuw May 12, 2022
6040c9f
Refactor store buffer search conditions
cbeuw May 12, 2022
13e3465
Reduce the number of runs in consistency tests
cbeuw May 12, 2022
8739e45
Move data_race and weak_memory into a submodule
cbeuw May 13, 2022
335667c
Move buffered functions into their own ext trait
cbeuw May 14, 2022
5a4a1bf
Remove incorrect comment
cbeuw May 15, 2022
6b54c92
Throw UB on imperfectly overlapping access
cbeuw May 16, 2022
577054c
Rename variables in AllocationMap
cbeuw May 16, 2022
9214537
Put the initialisation value into the store buffer
cbeuw May 16, 2022
e2002b4
Amend experimental thread support warnings
cbeuw May 16, 2022
31c0141
Replace yield_now() with spin loop hint
cbeuw May 17, 2022
5ddd4ef
Spelling, punctuation and grammar
cbeuw May 19, 2022
6d27f18
Update src/concurrency/weak_memory.rs
cbeuw May 22, 2022
dafd813
Move transmute into a separate function
cbeuw May 22, 2022
7dcb19e
Add rust-only operation tests
cbeuw May 23, 2022
2321b15
Differentiate between not multithreading and temp disabling race dete…
cbeuw May 24, 2022
226ed41
Destroy store buffers on non-racy non-atomic accesses
cbeuw May 24, 2022
613d60d
Allow non-racy mixed size accesses
cbeuw May 25, 2022
bfa5645
Split extra_cpp tests into sound and unsafe
cbeuw May 25, 2022
6a73ded
Update experimental threading warning
cbeuw May 25, 2022
a7c832b
Wording improvements
cbeuw May 29, 2022
ceb173d
Move logic out of machine.rs
cbeuw May 29, 2022
4a07f78
Forbade all racing mixed size atomic accesses
cbeuw May 29, 2022
8215702
Refer to GitHub issue on overwritten init value
cbeuw May 29, 2022
c731071
Give flag temp disabling race detector a better name
cbeuw May 29, 2022
6d0c76e
Specify only perfectly overlapping accesses can race
cbeuw May 29, 2022
65f39bd
Move tests to new directories
cbeuw Jun 4, 2022
1379036
Simplify known C++20 inconsistency test
cbeuw Jun 5, 2022
6fb7c13
Remove unused lifetimes
cbeuw Jun 5, 2022
bf7a5c4
Add more backgrounds on lazy store buffers
cbeuw Jun 5, 2022
1b32d14
Make racy imperfectly overlapping atomic access unsupported instead o…
cbeuw Jun 5, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Amend experimental thread support warnings
cbeuw committed Jun 6, 2022
commit e2002b4c657b218d3866342078b5fd0ce3118021
2 changes: 1 addition & 1 deletion src/shims/unix/thread.rs
Original file line number Diff line number Diff line change
@@ -14,7 +14,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
let this = self.eval_context_mut();

this.tcx.sess.warn(
"thread support is experimental and incomplete: weak memory effects are not emulated.",
"thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.",
);

// Create the new thread
2 changes: 1 addition & 1 deletion tests/pass/concurrency/channels.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/concurrency/concurrent_caller_location.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/concurrency/data_race.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/concurrency/disable_data_race_detector.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/concurrency/issue1643.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/concurrency/linux-futex.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/concurrency/simple.stderr
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

thread '<unnamed>' panicked at 'Hello!', $DIR/simple.rs:LL:CC
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
2 changes: 1 addition & 1 deletion tests/pass/concurrency/sync.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/concurrency/thread_locals.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/concurrency/tls_lib_drop.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/libc.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/pass/panic/concurrent-panic.stderr
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

Thread 1 starting, will block on mutex
Thread 1 reported it has started
2 changes: 1 addition & 1 deletion tests/pass/threadleak_ignored.stderr
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

Dropping 0
2 changes: 1 addition & 1 deletion tests/run-pass/weak_memory/consistency.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.

2 changes: 1 addition & 1 deletion tests/run-pass/weak_memory/weak.stderr
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
warning: thread support is experimental and incomplete: weak memory effects are not emulated.
warning: thread support is experimental: weak memory effects are not fully compatible with the Rust atomics memory model.