miri weak memory emulation: put previous value into initial store buffer #128942
Conversation
rustbot
added
S-waiting-on-review
|
The Miri subtree was changed cc @rust-lang/miri Some changes occurred to the CTFE / Miri engine cc @rust-lang/miri |
| // The program didn't actually do a read, so suppress the memory access hooks. | ||
| // This is also a very special exception where we just ignore an error -- if this read | ||
| // was UB e.g. because the memory is uninitialized, we don't want to know! | ||
| let old_val = this.run_for_validation(|| this.read_scalar(dest)).ok(); |
There was a problem hiding this comment.
Technically we only need to do this read if there wasn't a store buffer here yet. But to actually realize that we'd have to do the buffered_atomic_write before write_scalar, and then give buffered_atomic_write a closure that reads the previous value if needed. I am not sure doing the buffered store before the real store works of if there are some subtle invariants here preventing this...
| // access | ||
| val, | ||
| // access. | ||
| val: Some(val), |
There was a problem hiding this comment.
Is there a reason to represent an uninit store buffer as one containing a store element with None val, instead of just an empty buffer with no elements?
There was a problem hiding this comment.
This is related to the new test I added: if the memory is uninitialized when the atomic object is created, an outdated read hitting that initial state should properly report UB.
There was a problem hiding this comment.
So we can initially have uninitialized memory, but we do not have a mechanism to write uninitialized bytes later?
There was a problem hiding this comment.
Yes, indeed. Currently all atomic intrinsics take iN or *const T types which must be initialized.
If we ever have MaybeUninit atomics, this will become a lot more tricky, since the value could be partially initialized.
…ites; pre-fill with previous value
RalfJung
force-pushed
the
interpret-weak-memory
branch
from
c0c951c to
8b18c6b
Compare
|
@saethlin how should we proceed here? Is there some way I can make reviewing simpler? Should we look for another reviewer? Most of this is in Miri where I'd probably self-approve based on @cbeuw having taken a look, but we do need to make a function in rustc |
|
I'll review this today, that's how we will proceed :p |
|
:-)
|
|
I have a question about the implementation, but it's just idle curiosity. Thanks for the reminder. @bors r+ |
bors
added
S-waiting-on-bors
…saethlin miri weak memory emulation: put previous value into initial store buffer Fixes rust-lang/miri#2164 by doing a read before each atomic write so that we can initialize the store buffer. The read suppresses memory access hooks and UB exceptions, to avoid otherwise influencing the program behavior. If the read fails, we store that as `None` in the store buffer, so that when an atomic read races with the first atomic write to some memory and previously the memory was uninitialized, we can report UB due to reading uninit memory. `@cbeuw` this changes a bit the way we initialize the store buffers. Not sure if you still remember all this code, but if you could have a look to make sure this still makes sense, that would be great. :) r? `@saethlin`
…kingjubilee Rollup of 9 pull requests Successful merges: - rust-lang#126985 (Implement `-Z embed-source` (DWARFv5 source code embedding extension)) - rust-lang#127922 (Add unsafe to extern blocks in style guide) - rust-lang#128731 (simd_shuffle intrinsic: allow argument to be passed as vector) - rust-lang#128935 (More work on `zstd` compression) - rust-lang#128942 (miri weak memory emulation: put previous value into initial store buffer) - rust-lang#129418 (rustc: Simplify getting sysroot library directory) - rust-lang#129490 (Add Trusty OS as tier 3 target) - rust-lang#129559 (float types: document NaN bit pattern guarantees) - rust-lang#129642 (Bump backtrace to rust-lang/backtrace@fc37b22) r? `@ghost` `@rustbot` modify labels: rollup
Rollup of 9 pull requests Successful merges: - rust-lang#126985 (Implement `-Z embed-source` (DWARFv5 source code embedding extension)) - rust-lang#127922 (Add unsafe to extern blocks in style guide) - rust-lang#128731 (simd_shuffle intrinsic: allow argument to be passed as vector) - rust-lang#128935 (More work on `zstd` compression) - rust-lang#128942 (miri weak memory emulation: put previous value into initial store buffer) - rust-lang#129418 (rustc: Simplify getting sysroot library directory) - rust-lang#129490 (Add Trusty OS as tier 3 target) - rust-lang#129536 (Add `f16` and `f128` inline ASM support for `aarch64`) - rust-lang#129559 (float types: document NaN bit pattern guarantees) r? `@ghost` `@rustbot` modify labels: rollup
Rollup merge of rust-lang#128942 - RalfJung:interpret-weak-memory, r=saethlin miri weak memory emulation: put previous value into initial store buffer Fixes rust-lang/miri#2164 by doing a read before each atomic write so that we can initialize the store buffer. The read suppresses memory access hooks and UB exceptions, to avoid otherwise influencing the program behavior. If the read fails, we store that as `None` in the store buffer, so that when an atomic read races with the first atomic write to some memory and previously the memory was uninitialized, we can report UB due to reading uninit memory. ``@cbeuw`` this changes a bit the way we initialize the store buffers. Not sure if you still remember all this code, but if you could have a look to make sure this still makes sense, that would be great. :) r? ``@saethlin``
Fixes rust-lang/miri#2164 by doing a read before each atomic write so that we can initialize the store buffer. The read suppresses memory access hooks and UB exceptions, to avoid otherwise influencing the program behavior. If the read fails, we store that as
Nonein the store buffer, so that when an atomic read races with the first atomic write to some memory and previously the memory was uninitialized, we can report UB due to reading uninit memory.@cbeuw this changes a bit the way we initialize the store buffers. Not sure if you still remember all this code, but if you could have a look to make sure this still makes sense, that would be great. :)
r? @saethlin